Equations
- Lean.Meta.Simp.throwCongrHypothesisFailed = throw (Lean.Exception.internal Lean.Meta.Simp.congrHypothesisExceptionId)
Instances For
Return true if e
is of the form ofNat n
where n
is a kernel Nat literal
Instances For
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.
Instances For
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)
Instances For
Return true if e
is of the form Char.ofNat n
where n
is a kernel Nat literals.
Instances For
Instances For
- dep: Lean.Meta.Simp.SimpLetCase
- nondepDepVar: Lean.Meta.Simp.SimpLetCase
- nondep: Lean.Meta.Simp.SimpLetCase
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
We use withNewlemmas
whenever updating the local context.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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" 380 29 "unreachable code has been reached"
Instances For
Instances For
Instances For
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.
Instances For
Try to rewrite e
children using the given congruence theorem
Equations
- One or more equations did not get rendered due to their size.
Instances For
Returns true
if e
is of the form @letFun _ (fun _ => β) _ _
β
must not contain loose bound variables. Recall that simp
does not have support for let_fun
s
where resulting type depends on the let
-value. Example:
let_fun n := 10;
BitVec.zero n
Instances For
Simplifies a sequence of let_fun
declarations.
It attempts to minimize the quadratic overhead imposed by
the locally nameless discipline.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
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.
Instances For
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.
Instances For
Equations
- Lean.Meta.applySimpResultToFVarId mvarId fvarId r mayCloseGoal = do let localDecl ← fvarId.getDecl Lean.Meta.applySimpResultToProp mvarId (Lean.mkFVar fvarId) localDecl.type r mayCloseGoal
Instances For
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.
Instances For
Instances For
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.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.