This module has telescope functions for matcher alts. They are primarily used in Match.MatchEqs, but also in MatcherApp.Transform, hence the separate module.

def Lean.Meta.Match.forallAltVarsTelescope {α : Type} (altType : Expr) (altInfo : AltParamInfo) (k : Array Expr → Array Expr → Array Bool → Expr → MetaM α) : MetaM α

Similar to forallTelescopeReducing, but

1. Eliminates arguments for named parameters and the associated equation proofs.

2. Instantiate the Unit parameter of an otherwise argumentless alternative.

It does not handle the equality parameters associated with the h : discr notation.

The continuation k takes four arguments ys args mask type.

• ys are variables for the hypotheses that have not been eliminated.
• args are the arguments for the alternative alt that has type altType. ys.size <= args.size
• mask[i] is true if the hypotheses has not been eliminated. mask.size == args.size.
• type is the resulting type for altType.

We use the mask to build the splitter proof. See mkSplitterProof.

This can be used to use the alternative of a match expression in its splitter.

Equations

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

def Lean.Meta.Match.forallAltTelescope {α : Type} (altType : Expr) (altInfo : AltParamInfo) (numDiscrEqs : Nat) (k : Array Expr → Array Expr → Array Expr → Array Bool → Expr → MetaM α) : MetaM α

Extension of forallAltTelescope that continues further:

Equality parameters associated with the h : discr notation are replaced with rfl proofs. Recall that this kind of parameter always occurs after the parameters corresponding to pattern variables.

The continuation k takes four arguments ys args mask type.

• ys are variables for the hypotheses that have not been eliminated.
• eqs are variables for equality hypotheses associated with discriminants annotated with h : discr.
• args are the arguments for the alternative alt that has type altType. ys.size <= args.size
• mask[i] is true if the hypotheses has not been eliminated. mask.size == args.size.
• type is the resulting type for altType.

We use the mask to build the splitter proof. See mkSplitterProof.

This can be used to use the alternative of a match expression in its splitter.

Equations

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