Function parse_definition_in 

pub fn parse_definition_in(
    ctx: &Context,
    input: &str,
) -> Result<(Command, usize), ParseError>

parse_definition, with the kernel context the equation compiler needs.

With a context, a Consider block is a real equation set: nested constructor patterns compile to a tree of positional matches, overlapping equations are split top-to-bottom (first match wins, as in Lean), a When _: catch-all fans out over every constructor with no clause of its own, several columns can be matched at once (Consider a and b: with When Zero and _:), and every clause lands in the slot of the constructor it NAMES rather than the slot its position in the source happens to hit.