pub fn pattern_binder_types(
ctx: &Context,
disc_ty: &Term,
pattern: &Pattern,
) -> KernelResult<Vec<(String, Term)>>Expand description
The types a pattern’s binders take when it is matched against a value of disc_ty.
This is the same constructor-telescope walk the compiler itself does, exposed so a parser can put the binders in scope with their real types BEFORE it parses the clause body. Two computations of one fact is how a compiler and its surface drift apart; there is one here.