Documentation

Lean.Meta.Match.CaseValues

structure Lean.Meta.CaseValueSubgoal :

Type

mvarId : Lean.MVarId
newH : Lean.FVarId
subst : Lean.Meta.FVarSubst

instance Lean.Meta.instInhabitedCaseValueSubgoal :

Inhabited Lean.Meta.CaseValueSubgoal

Equations

Lean.Meta.instInhabitedCaseValueSubgoal = { default := { mvarId := default, newH := default, subst := default } }

def Lean.Meta.caseValue (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (value : Lean.Expr) :

Lean.MetaM (Lean.Meta.CaseValueSubgoal × Lean.Meta.CaseValueSubgoal)

Equations

Lean.Meta.caseValue mvarId fvarId value = do let s ← Lean.Meta.caseValueAux mvarId fvarId value `h { map := ∅ } Lean.Meta.appendTagSuffix s.fst.mvarId `thenBranch Lean.Meta.appendTagSuffix s.snd.mvarId `elseBranch pure s

structure Lean.Meta.CaseValuesSubgoal :

Type

instance Lean.Meta.instInhabitedCaseValuesSubgoal :

Inhabited Lean.Meta.CaseValuesSubgoal

Equations

Lean.Meta.instInhabitedCaseValuesSubgoal = { default := { mvarId := default, newHs := default, subst := default } }

def Lean.Meta.caseValues (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (values : Array Lean.Expr) (hNamePrefix : optParam Lean.Name `h) (substNewEqs : optParam Bool false) :

Lean.MetaM (Array Lean.Meta.CaseValuesSubgoal)

Equations

Lean.Meta.caseValues mvarId fvarId values hNamePrefix substNewEqs = (fun loop => loop 1 mvarId (Array.toList values) #[] #[]) (Lean.Meta.caseValues.loop fvarId hNamePrefix substNewEqs)

def Lean.Meta.caseValues.loop (fvarId : Lean.FVarId) (hNamePrefix : optParam Lean.Name `h) (substNewEqs : optParam Bool false) :

Nat → Lean.MVarId → List Lean.Expr → Array Lean.FVarId → Array Lean.Meta.CaseValuesSubgoal → Lean.MetaM (Array Lean.Meta.CaseValuesSubgoal)