Documentation

Lean.Elab.PreDefinition.Eqns

source
structure Lean.Elab.Eqns.EqnInfoCore:
Type
source
instance Lean.Elab.Eqns.instInhabitedEqnInfoCore:
Inhabited Lean.Elab.Eqns.EqnInfoCore
Equations
source
partial def Lean.Elab.Eqns.expand:
Lean.Expr → Lean.Expr
source
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.
source
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.
source
def Lean.Elab.Eqns.simpMatch? (mvarId : Lean.MVarId) :
Lean.MetaM (Option Lean.MVarId)
Equations
source
def Lean.Elab.Eqns.simpIf? (mvarId : Lean.MVarId) :
Lean.MetaM (Option Lean.MVarId)
Equations
source
def Lean.Elab.Eqns.splitMatch? (mvarId : Lean.MVarId) (declNames : Array Lean.Name) :
Lean.MetaM (Option (List Lean.MVarId))
Equations
source
partial def Lean.Elab.Eqns.splitMatch?.go (mvarId : Lean.MVarId) (declNames : Array Lean.Name) (target : Lean.Expr) (badCases : Lean.ExprSet) :
Lean.MetaM (Option (List Lean.MVarId))
source
structure Lean.Elab.Eqns.Context:
Type
source
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.
source
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.
source
def Lean.Elab.Eqns.simpEqnType.collect (e : Lean.Expr) :
Lean.FVarIdSet
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Eqns.mkEqnTypes (declNames : Array Lean.Name) (mvarId : Lean.MVarId) :
Lean.MetaM (Array Lean.Expr)
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Elab.Eqns.mkEqnTypes.go (declNames : Array Lean.Name) (mvarId : Lean.MVarId) :
ReaderT Lean.Elab.Eqns.Context (StateRefT' IO.RealWorld (Array Lean.Expr) Lean.MetaM) Unit
source
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.
source
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)
source
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.
source
def Lean.Elab.Eqns.deltaRHS? (mvarId : Lean.MVarId) (declName : Lean.Name) :
Lean.MetaM (Option Lean.MVarId)
Equations
  • One or more equations did not get rendered due to their size.
source
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.
source
def Lean.Elab.Eqns.tryContradiction (mvarId : Lean.MVarId) :
Lean.MetaM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
structure Lean.Elab.Eqns.UnfoldEqnExtState:
Type
source
instance Lean.Elab.Eqns.instInhabitedUnfoldEqnExtState:
Inhabited Lean.Elab.Eqns.UnfoldEqnExtState
Equations
source
opaque Lean.Elab.Eqns.unfoldEqnExt:
Lean.EnvExtension Lean.Elab.Eqns.UnfoldEqnExtState
source
def Lean.Elab.Eqns.mkUnfoldProof (declName : Lean.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 constracted 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.
source
partial def Lean.Elab.Eqns.mkUnfoldProof.go (declName : Lean.Name) (tryEqns : Lean.MVarId → Lean.MetaM Bool) (mvarId : Lean.MVarId) :
Lean.MetaM Unit
source
def Lean.Elab.Eqns.mkUnfoldEq (declName : Lean.Name) (info : Lean.Elab.Eqns.EqnInfoCore) :
Lean.MetaM Lean.Name

Generate the "unfold" lemma for declName.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Eqns.getUnfoldFor? (declName : Lean.Name) (getInfo? : Unit → Option Lean.Elab.Eqns.EqnInfoCore) :
Lean.MetaM (Option Lean.Name)
Equations
  • One or more equations did not get rendered due to their size.