Skip to main content

pattern_binder_types

logicaffeine_cli::interface::match_compile

Function pattern_binder_types 

Source 
pub fn pattern_binder_types(
    ctx: &Context,
    disc_ty: &Term,
    pattern: &Pattern,
) -> Result<Vec<(String, Term)>, KernelError>
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.