Instances For
Equations
- One or more equations did not get rendered due to their size.
- Lean.expandExplicitBindersAux.loop combinator idents type? 0 acc = pure acc
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Lean.expandBrackedBindersAux.loop combinator binders 0 acc = pure acc
Instances For
Instances For
Instances For
Step-wise reasoning over transitive relations.
calc
a = b := pab
b = c := pbc
...
y = z := pyz
proves a = z
from the given step-wise proofs. =
can be replaced with any
relation implementing the typeclass Trans
. Instead of repeating the right-
hand sides, subsequent left-hand sides can be replaced with _
.
calc
a = b := pab
_ = c := pbc
...
_ = z := pyz
It is also possible to write the first relation as
. This is useful for aligning relation symbols, especially on longer:
identifiers:
calc abc
_ = bce := pabce
_ = cef := pbcef
...
_ = xyz := pwxyz
calc
has term mode and tactic mode variants. This is the term mode variant.
See Theorem Proving in Lean 4 for more information.
Instances For
Step-wise reasoning over transitive relations.
calc
a = b := pab
b = c := pbc
...
y = z := pyz
proves a = z
from the given step-wise proofs. =
can be replaced with any
relation implementing the typeclass Trans
. Instead of repeating the right-
hand sides, subsequent left-hand sides can be replaced with _
.
calc
a = b := pab
_ = c := pbc
...
_ = z := pyz
It is also possible to write the first relation as
. This is useful for aligning relation symbols:
calc abc
_ = bce := pabce
_ = cef := pbcef
...
_ = xyz := pwxyz
calc
has term mode and tactic mode variants. This is the tactic mode variant,
which supports an additional feature: it works even if the goal is a = z'
for some other z'
; in this case it will not close the goal but will instead
leave a subgoal proving z = z'
.
See Theorem Proving in Lean 4 for more information.
Instances For
Apply function extensionality and introduce new hypotheses.
The tactic funext
will keep applying the funext
lemma until the goal target is not reducible to
|- ((fun x => ...) = (fun x => ...))
The variant funext h₁ ... hₙ
applies funext
n
times, and uses the given identifiers to name the new hypotheses.
Patterns can be used like in the intro
tactic. Example, given a goal
|- ((fun x : Nat × Bool => ...) = (fun x => ...))
funext (a, b)
applies funext
once and performs pattern matching on the newly introduced pair.
Instances For
Expands
class abbrev C := D_1, ..., D_n
into
class C extends D_1, ..., D_n
attribute [instance] C.mk
Instances For
· tac
focuses on the main goal and tries to solve it using tac
, or else fails.
Instances For
Similar to first
, but succeeds only if one the given tactics solves the current goal.