Equations
- Lean.Meta.Simp.throwCongrHypothesisFailed = throw (Lean.Exception.internal Lean.Meta.Simp.congrHypothesisExceptionId)
Helper method for bootstrapping purposes. It disables arith
if support theorems have not been defined yet.
Equations
- One or more equations did not get rendered due to their size.
Return true if e
is of the form ofNat n
where n
is a kernel Nat literal
If e
is a raw Nat literal and OfNat.ofNat
is not in the list of declarations to unfold,
return an OfNat.ofNat
-application.
Equations
- One or more equations did not get rendered due to their size.
Return true if e
is of the form ofScientific n b m
where n
and m
are kernel Nat literals.
Equations
- Lean.Meta.Simp.isOfScientificLit e = (e.isAppOfArity `OfScientific.ofScientific 5 && (e.getArg! 4).isRawNatLit && (e.getArg! 2).isRawNatLit)
Return true if e
is of the form Char.ofNat n
where n
is a kernel Nat literals.
Equations
- Lean.Meta.Simp.isCharLit e = (e.isAppOfArity `Char.ofNat 1 && e.appArg!.isRawNatLit)
Equations
- Lean.Meta.Simp.instInhabitedSimpM = { default := fun (x : Lean.Meta.Simp.MethodsRef) (x : Lean.Meta.Simp.Context) (x : ST.Ref IO.RealWorld Lean.Meta.Simp.State) => default }
Equations
- dep: Lean.Meta.Simp.SimpLetCase
- nondepDepVar: Lean.Meta.Simp.SimpLetCase
- nondep: Lean.Meta.Simp.SimpLetCase
Equations
- One or more equations did not get rendered due to their size.
We use withNewlemmas
whenever updating the local context.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Meta.Simp.simpConst e = do let __do_lift ← Lean.Meta.Simp.reduce e pure { expr := __do_lift, proof? := none, cache := true }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
- Lean.Meta.Simp.simpLet e = panicWithPosWithDecl "Lean.Meta.Tactic.Simp.Main" "Lean.Meta.Simp.simpLet" 391 29 "unreachable code has been reached"
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Process the given congruence theorem hypothesis. Return true if it made "progress".
Equations
- One or more equations did not get rendered due to their size.
Try to rewrite e
children using the given congruence theorem
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
- Lean.Meta.Simp.simpStep (Lean.Expr.mdata m e_2) = do let r ← Lean.Meta.Simp.simp e_2 pure { expr := Lean.mkMData m r.expr, proof? := r.proof?, cache := r.cache }
- Lean.Meta.Simp.simpStep (Lean.Expr.proj typeName idx struct) = Lean.Meta.Simp.simpProj (Lean.Expr.proj typeName idx struct)
- Lean.Meta.Simp.simpStep (fn.app arg) = Lean.Meta.Simp.simpApp (fn.app arg)
- Lean.Meta.Simp.simpStep (Lean.Expr.lam binderName binderType body binderInfo) = Lean.Meta.Simp.simpLambda (Lean.Expr.lam binderName binderType body binderInfo)
- Lean.Meta.Simp.simpStep (Lean.Expr.forallE binderName binderType body binderInfo) = Lean.Meta.Simp.simpForall (Lean.Expr.forallE binderName binderType body binderInfo)
- Lean.Meta.Simp.simpStep (Lean.Expr.letE declName type value body nonDep) = Lean.Meta.Simp.simpLet (Lean.Expr.letE declName type value body nonDep)
- Lean.Meta.Simp.simpStep (Lean.Expr.const declName us) = Lean.Meta.Simp.simpConst (Lean.Expr.const declName us)
- Lean.Meta.Simp.simpStep (Lean.Expr.bvar deBruijnIndex) = panicWithPosWithDecl "Lean.Meta.Tactic.Simp.Main" "Lean.Meta.Simp.simpStep" 601 20 "unreachable code has been reached"
- Lean.Meta.Simp.simpStep (Lean.Expr.sort u) = pure { expr := Lean.Expr.sort u, proof? := none, cache := true }
- Lean.Meta.Simp.simpStep (Lean.Expr.lit a) = pure { expr := Lean.Expr.lit a, proof? := none, cache := true }
- Lean.Meta.Simp.simpStep (Lean.Expr.mvar mvarId) = do let __do_lift ← Lean.instantiateMVars (Lean.Expr.mvar mvarId) pure { expr := __do_lift, proof? := none, cache := true }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
See simpTarget
. This method assumes mvarId
is not assigned, and we are already using mvarId
s local context.
Equations
- One or more equations did not get rendered due to their size.
Simplify the given goal target (aka type). Return none
if the goal was closed. Return some mvarId'
otherwise,
where mvarId'
is the simplified new goal.
Equations
- One or more equations did not get rendered due to their size.
Apply the result r
for prop
(which is inhabited by proof
). Return none
if the goal was closed. Return some (proof', prop')
otherwise, where proof' : prop'
and prop'
is the simplified prop
.
This method assumes mvarId
is not assigned, and we are already using mvarId
s local context.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Meta.applySimpResultToFVarId mvarId fvarId r mayCloseGoal = do let localDecl ← fvarId.getDecl Lean.Meta.applySimpResultToProp mvarId (Lean.mkFVar fvarId) localDecl.type r mayCloseGoal
Simplify prop
(which is inhabited by proof
). Return none
if the goal was closed. Return some (proof', prop')
otherwise, where proof' : prop'
and prop'
is the simplified prop
.
This method assumes mvarId
is not assigned, and we are already using mvarId
s local context.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
- Lean.Meta.applySimpResultToLocalDeclCore mvarId fvarId none = pure none
Simplify simp
result to the given local declaration. Return none
if the goal was closed.
This method assumes mvarId
is not assigned, and we are already using mvarId
s local context.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.