def Lean.Meta.Match.mkAppDiscrEqs (alt : Expr) (heqs : Array Expr) (numDiscrEqs : Nat) : MetaM Expr

Given an application of an matcher arm alt that is expecting the numDiscrEqs, and an array of discr = pattern equalities (one for each discriminant), apply those that are expected by the alternative.

Equations

• Lean.Meta.Match.mkAppDiscrEqs alt heqs numDiscrEqs = do let __do_lift ← Lean.Meta.inferType alt Lean.Meta.Match.mkAppDiscrEqs.go✝ alt heqs numDiscrEqs alt __do_lift 0

def Lean.Meta.Match.proveCondEqThm (matchDeclName : Name) (type : Expr) (heqPos heqNum : Nat := 0) : MetaM Expr

Helper method for proving a conditional equational theorem associated with an alternative of the match-eliminator matchDeclName. type contains the type of the theorem.

The heqPos/heqNum arguments indicate that these hypotheses are Eq/HEq hypotheses to substitute first; this is used for the generalized match equations.

Equations

• One or more equations did not get rendered due to their size.

@[export lean_get_match_equations_for]

def Lean.Meta.Match.getEquationsForImpl (matchDeclName : Name) : MetaM MatchEqns

Equations

• One or more equations did not get rendered due to their size.

opaque Lean.Meta.Match.matchCongrEqnsExt : EnvExtension (PHashMap Name (Array Name))

def Lean.Meta.Match.registerMatchCongrEqns (matchDeclName : Name) (eqnNames : Array Name) : CoreM Unit

Equations

• One or more equations did not get rendered due to their size.

@[export lean_get_congr_match_equations_for]

def Lean.Meta.Match.genMatchCongrEqnsImpl (matchDeclName : Name) : MetaM (Array Name)

Generate the congruence equations for the given match auxiliary declaration. The congruence equations have a completely unrestricted left-hand side (arbitrary discriminants), and take propositional equations relating the discriminants to the patterns as arguments. In this sense they combine a congruence lemma with the regular equation lemma. Since the motive depends on the discriminants, they are HEq equations.

The code duplicates a fair bit of the logic above, and has to repeat the calculation of the notAlts. One could avoid that and generate the generalized equations eagerly above, but they are not always needed, so for now we live with the code duplication.

Equations

• One or more equations did not get rendered due to their size.