def Lean.Meta.casesOnStuckLHS (mvarId : Lean.MVarId) : Lean.MetaM (Array Lean.MVarId)

Helper method for proveCondEqThm. Given a goal of the form C.rec ... xMajor = rhs, apply cases xMajor.

Equations

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

partial def Lean.Meta.casesOnStuckLHS.findFVar? (e : Lean.Expr) : Lean.MetaM (Option Lean.FVarId)

def Lean.Meta.casesOnStuckLHS? (mvarId : Lean.MVarId) : Lean.MetaM (Option (Array Lean.MVarId))

Equations

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

def Lean.Meta.Match.unfoldNamedPattern (e : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

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

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

Similar to forallTelescopeReducing, but

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

2. Equality parameters associated with the h : discr notation are replaced with rfl proofs. Recall that this kind of parameter always occurs after the parameters correspoting to pattern variables. numNonEqParams is the size of the prefix.

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

• Lean.Meta.Match.forallAltTelescope altType altNumParams numDiscrEqs k = Lean.Meta.Match.forallAltTelescope.go altType altNumParams numDiscrEqs k #[] #[] #[] #[] 0 altType

partial def Lean.Meta.Match.forallAltTelescope.go {α : Type} (altType : Lean.Expr) (altNumParams numDiscrEqs : Nat) (k : Array Lean.Expr → Array Lean.Expr → Array Lean.Expr → Array Bool → Lean.Expr → Lean.MetaM α) (ys eqs args : Array Lean.Expr) (mask : Array Bool) (i : Nat) (type : Lean.Expr) : Lean.MetaM α

def Lean.Meta.Match.forallAltTelescope.isNamedPatternProof (type h : Lean.Expr) : Bool

Equations

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

structure Lean.Meta.Match.SimpH.State : Type

State for the equational theorem hypothesis simplifier.

Recall that each equation contains additional hypotheses to ensure the associated case does not taken by previous cases. We have one hypothesis for each previous case.

Each hypothesis is of the form forall xs, eqs → False

We use tactics to minimize code duplication.

• mvarId : Lean.MVarId
• xs : List Lean.FVarId
• eqs : List Lean.FVarId
• eqsNew : List Lean.FVarId

@[reducible, inline]

abbrev Lean.Meta.Match.SimpH.M (α : Type) : Type

Equations

• Lean.Meta.Match.SimpH.M = StateRefT' IO.RealWorld Lean.Meta.Match.SimpH.State Lean.MetaM

partial def Lean.Meta.Match.SimpH.trySubstVarsAndContradiction (mvarId : Lean.MVarId) (forbidden : Lean.FVarIdSet := ∅) : Lean.MetaM Bool

Auxiliary tactic that tries to replace as many variables as possible and then apply contradiction. We use it to discard redundant hypotheses.

partial def Lean.Meta.Match.SimpH.go : Lean.Meta.Match.SimpH.M Bool

def Lean.Meta.Match.proveCondEqThm (matchDeclName : Lean.Name) (type : Lean.Expr) : Lean.MetaM Lean.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.

Equations

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

partial def Lean.Meta.Match.proveCondEqThm.go (matchDeclName : Lean.Name) (mvarId : Lean.MVarId) (depth : Nat) : Lean.MetaM Unit

inductive Lean.Meta.Match.InjectionAnyResult : Type

• solved : Lean.Meta.Match.InjectionAnyResult
• failed : Lean.Meta.Match.InjectionAnyResult
• subgoal (fvarId : Lean.FVarId) (mvarId : Lean.MVarId) : Lean.Meta.Match.InjectionAnyResult

  fvarId refers to the local declaration selected for the application of the injection tactic.

@[export lean_get_match_equations_for]

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

Equations

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