structure Lean.Elab.Eqns.EqnInfoCore : Type

• declName : Lake.Name
• levelParams : List Lake.Name
• type : Lean.Expr
• value : Lean.Expr

instance Lean.Elab.Eqns.instInhabitedEqnInfoCore : Inhabited Lean.Elab.Eqns.EqnInfoCore

Equations

• Lean.Elab.Eqns.instInhabitedEqnInfoCore = { default := { declName := default, levelParams := default, type := default, value := default } }

partial def Lean.Elab.Eqns.expand (progress : Bool) (e : Lean.Expr) : Bool × Lean.Expr

Zeta reduces let and let_fun while consuming metadata. Returns true if progress is made.

def Lean.Elab.Eqns.expandRHS? (mvarId : Lean.MVarId) : Lean.MetaM (Option Lean.MVarId)

Equations

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

def Lean.Elab.Eqns.funext? (mvarId : Lean.MVarId) : Lean.MetaM (Option Lean.MVarId)

Equations

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

def Lean.Elab.Eqns.simpMatch? (mvarId : Lean.MVarId) : Lean.MetaM (Option Lean.MVarId)

Equations

• Lean.Elab.Eqns.simpMatch? mvarId = do let mvarId' ← Lean.Meta.Split.simpMatchTarget mvarId if (mvarId != mvarId') = true then pure (some mvarId') else pure none

def Lean.Elab.Eqns.simpIf? (mvarId : Lean.MVarId) : Lean.MetaM (Option Lean.MVarId)

Equations

• Lean.Elab.Eqns.simpIf? mvarId = do let mvarId' ← Lean.Meta.simpIfTarget mvarId true if (mvarId != mvarId') = true then pure (some mvarId') else pure none

def Lean.Elab.Eqns.splitMatch? (mvarId : Lean.MVarId) (declNames : Array Lake.Name) : Lean.MetaM (Option (List Lean.MVarId))

Equations

• Lean.Elab.Eqns.splitMatch? mvarId declNames = Lean.commitWhenSome? do let target ← mvarId.getType' Lean.Elab.Eqns.splitMatch?.go mvarId declNames target ∅

partial def Lean.Elab.Eqns.splitMatch?.go (mvarId : Lean.MVarId) (declNames : Array Lake.Name) (target : Lean.Expr) (badCases : Lean.ExprSet) : Lean.MetaM (Option (List Lean.MVarId))

structure Lean.Elab.Eqns.Context : Type

• declNames : Array Lake.Name

def Lean.Elab.Eqns.tryURefl (mvarId : Lean.MVarId) : Lean.MetaM Bool

Try to close goal using rfl with smart unfolding turned off.

Equations

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

def Lean.Elab.Eqns.simpEqnType (eqnType : Lean.Expr) : Lean.MetaM Lean.Expr

Eliminate namedPatterns from equation, and trivial hypotheses.

Equations

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

def Lean.Elab.Eqns.simpEqnType.collect (e : Lean.Expr) : Lean.FVarIdSet

Equations

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

def Lean.Elab.Eqns.mkEqnTypes (tryRefl : Bool) (declNames : Array Lake.Name) (mvarId : Lean.MVarId) : Lean.MetaM (Array Lean.Expr)

Equations

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

partial def Lean.Elab.Eqns.mkEqnTypes.go (tryRefl : Bool) (declNames : Array Lake.Name) (mvarId : Lean.MVarId) : ReaderT Lean.Elab.Eqns.Context (StateRefT' IO.RealWorld (Array Lean.Expr) Lean.MetaM) Unit

def Lean.Elab.Eqns.removeUnusedEqnHypotheses (declType : Lean.Expr) (declValue : Lean.Expr) : Lean.CoreM (Lean.Expr × Lean.Expr)

Some of the hypotheses added by mkEqnTypes may not be used by the actual proof (i.e., value argument). This method eliminates them.

Alternative solution: improve saveEqn and make sure it never includes unnecessary hypotheses. These hypotheses are leftovers from tactics such as splitMatch? used in mkEqnTypes.

Equations

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

def Lean.Elab.Eqns.removeUnusedEqnHypotheses.go (declType : Lean.Expr) (declValue : Lean.Expr) (type : Lean.Expr) (value : Lean.Expr) (xs : Array Lean.Expr) (lctx : Lean.LocalContext) : Lean.CoreM (Lean.Expr × Lean.Expr)

def Lean.Elab.Eqns.deltaLHS (mvarId : Lean.MVarId) : Lean.MetaM Lean.MVarId

Delta reduce the equation left-hand-side

Equations

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

def Lean.Elab.Eqns.deltaRHS? (mvarId : Lean.MVarId) (declName : Lake.Name) : Lean.MetaM (Option Lean.MVarId)

Equations

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

def Lean.Elab.Eqns.whnfReducibleLHS? (mvarId : Lean.MVarId) : Lean.MetaM (Option Lean.MVarId)

Apply whnfR to lhs, return none if lhs was not modified

Equations

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

def Lean.Elab.Eqns.tryContradiction (mvarId : Lean.MVarId) : Lean.MetaM Bool

Equations

• Lean.Elab.Eqns.tryContradiction mvarId = mvarId.contradictionCore { useDecide := true, emptyType := true, searchFuel := 16, genDiseq := true }

def Lean.Elab.Eqns.mkUnfoldProof (declName : Lake.Name) (mvarId : Lean.MVarId) : Lean.MetaM Unit

Auxiliary method for mkUnfoldEq. The structure is based on mkEqnTypes. mvarId is the goal to be proved. It is a goal of the form

declName x_1 ... x_n = body[x_1, ..., x_n]

The proof is constructed using the automatically generated equational theorems. We basically keep splitting the match and if-then-else expressions in the right hand side until one of the equational theorems is applicable.

Equations

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

partial def Lean.Elab.Eqns.mkUnfoldProof.go (declName : Lake.Name) (tryEqns : Lean.MVarId → Lean.MetaM Bool) (mvarId : Lean.MVarId) : Lean.MetaM Unit

def Lean.Elab.Eqns.mkUnfoldEq (declName : Lake.Name) (info : Lean.Elab.Eqns.EqnInfoCore) : Lean.MetaM Lake.Name

Generate the "unfold" lemma for declName.

Equations

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

def Lean.Elab.Eqns.getUnfoldFor? (declName : Lake.Name) (getInfo? : Unit → Option Lean.Elab.Eqns.EqnInfoCore) : Lean.MetaM (Option Lake.Name)

Equations

• Lean.Elab.Eqns.getUnfoldFor? declName getInfo? = match getInfo? () with | some info => do let __do_lift ← Lean.Elab.Eqns.mkUnfoldEq declName info pure (some __do_lift) | x => pure none