68c006a95b
This PR enables transforming nondependent `let`s into `have`s in a number of contexts: the bodies of nonrecursive definitions, equation lemmas, smart unfolding definitions, and types of theorems. A motivation for this change is that when zeta reduction is disabled, `simp` can only effectively rewrite `have` expressions (e.g. `split` uses `simp` with zeta reduction disabled), and so we cache the nondependence calculations by transforming `let`s to `have`s. The transformation can be disabled using `set_option cleanup.letToHave false`. Uses `Meta.letToHave`, introduced in #8954.
14 lines
795 B
Text
14 lines
795 B
Text
funind_errors.lean:4:7-4:26: error: unknown identifier 'doesNotExist.induct'
|
||
funind_errors.lean:22:7-22:23: error: unknown constant 'takeWhile.induct'
|
||
takeWhile.foo.induct.{u_1} {α : Type u_1} (p : α → Bool) (as : Array α) (motive : Nat → Array α → Prop)
|
||
(case1 :
|
||
∀ (i : Nat) (r : Array α) (h : i < as.size),
|
||
have a := as.get i h;
|
||
p a = true → motive (i + 1) (r.push a) → motive i r)
|
||
(case2 :
|
||
∀ (i : Nat) (r : Array α) (h : i < as.size),
|
||
have a := as.get i h;
|
||
¬p a = true → motive i r)
|
||
(case3 : ∀ (i : Nat) (r : Array α), ¬i < as.size → motive i r) (i : Nat) (r : Array α) : motive i r
|
||
funind_errors.lean:38:7-38:20: error: unknown constant 'idEven.induct'
|
||
funind_errors.lean:45:7-45:19: error: unknown constant 'idAcc.induct'
|