219f8214d3
This PR modifies `let` and `have` term syntaxes to be consistent with each other. Adds configuration options; for example, `have` is equivalent to `let +nondep`, for *nondependent* lets. Other options include `+usedOnly` (for `let_tmp`), `+zeta` (for `letI`/`haveI`), and `+postponeValue` (for `let_delayed)`. There is also `let (eq := h) x := v; b` for introducing `h : x = v` when elaborating `b`. The `eq` option works for pattern matching as well, for example `let (eq := h) (x, y) := p; b`. Future PRs will add these options to tactic syntax, once a stage0 update has been done.
75 lines
1.5 KiB
Text
75 lines
1.5 KiB
Text
/-! Incremental reuse in combinator -/
|
||
|
||
def case (h : a ∨ b ∨ c) : True := by
|
||
cases h
|
||
case inr h =>
|
||
cases h
|
||
case inl =>
|
||
dbg_trace "c 0"
|
||
dbg_trace "c 1"
|
||
dbg_trace "c 2"
|
||
--^ sync
|
||
--^ insert: ".5"
|
||
|
||
/-!
|
||
`case` with multiple tags should *not* be accidentally incremental, leading to e.g. kernel errors.
|
||
-/
|
||
|
||
-- RESET
|
||
def case2 (h : a ∨ b ∨ c) : True := by
|
||
cases h
|
||
case inl | inr =>
|
||
skip
|
||
sorry
|
||
--^ sync
|
||
--^ insert: " "
|
||
--^ collectDiagnostics
|
||
|
||
-- RESET
|
||
def cdot (h : a ∨ b) : True := by
|
||
cases h
|
||
. dbg_trace "d 0"
|
||
dbg_trace "d 1"
|
||
dbg_trace "d 2"
|
||
--^ sync
|
||
--^ insert: ".5"
|
||
dbg_trace "d 3"
|
||
|
||
-- RESET
|
||
def have : True := by
|
||
dbg_trace "h 0"
|
||
have : True := by
|
||
dbg_trace "h 1"
|
||
dbg_trace "h 2"
|
||
--^ sync
|
||
--^ insert: ".5"
|
||
dbg_trace "h 3"
|
||
-- TODO(kmill) make sure extra h 1 is no longer in output
|
||
/-!
|
||
Updating the `have` header should update the unsolved goals position (and currently re-run the body)
|
||
-/
|
||
-- RESET
|
||
def spaceHave : True := by
|
||
have : True := by
|
||
--^ collectDiagnostics
|
||
--^ insert: " "
|
||
--^ collectDiagnostics
|
||
dbg_trace "sh"
|
||
|
||
-- RESET
|
||
def next : True := by
|
||
next =>
|
||
dbg_trace "n 0"
|
||
dbg_trace "n 1"
|
||
--^ sync
|
||
--^ insert: ".5"
|
||
|
||
-- RESET
|
||
def if : True := by
|
||
if h : True then
|
||
dbg_trace "i 0"
|
||
dbg_trace "i 1"
|
||
--^ sync
|
||
--^ insert: ".5"
|
||
else
|
||
skip
|