Helper method for bootstrapping purposes. It disables arith
if support theorems have not been defined yet.
Instances For
Instances For
Similar to Result.getProof
, but adds a mkExpectedTypeHint
if proof?
is none
(i.e., result is definitionally equal to input), but we cannot establish that
source
and r.expr
are definitionally when using TransparencyMode.reducible
.
Instances For
Instances For
Instances For
Return true if e
is of the form ofNat n
where n
is a kernel Nat literal
Instances For
Instances For
- dep: Lean.Meta.Simp.SimpLetCase
- nondepDepVar: Lean.Meta.Simp.SimpLetCase
- nondep: Lean.Meta.Simp.SimpLetCase
Instances For
Instances For
Instances For
Instances For
Try to use automatically generated congruence theorems. See mkCongrSimp?
.
Process the given congruence theorem hypothesis. Return true if it made "progress".
Try to rewrite e
children using the given congruence theorem
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Return true if e
is of the form (x : α) → ... → s = t → ... → False
Recall that this kind of proposition is generated by Lean when creating equations for
functions and match-expressions with overlapping cases.
Example: the following match
-expression has overlapping cases.
def f (x y : Nat) :=
match x, y with
| Nat.succ n, Nat.succ m => ...
| _, _ => 0
The second equation is of the form
(x y : Nat) → ((n m : Nat) → x = Nat.succ n → y = Nat.succ m → False) → f x y = 0
The hypothesis (n m : Nat) → x = Nat.succ n → y = Nat.succ m → False
is essentially
saying the first case is not applicable.
Instances For
Instances For
Tries to solve e
using unifyEq?
.
It assumes that isEqnThmHypothesis e
is true
.
Instances For
Instances For
Instances For
Auxiliary method.
Given the current target
of mvarId
, apply r
which is a new target and proof that it is equal to the current one.
Instances For
See simpTarget
. This method assumes mvarId
is not assigned, and we are already using mvarId
s local context.
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.
Instances For
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.
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.