e6f44eeeec
This PR adds regression tests for `do`-notation issues that the new elaborator fixes: * `tests/elab/doNotation7.lean` collects reproducers for #2663, #2676, #3126, #5607, #6426, and #8119. * `tests/elab/12229.lean` covers the `logInfo` and `Std.TreeMap` reproducers from #12229.
46 lines
1.1 KiB
Text
46 lines
1.1 KiB
Text
import Lean
|
||
import Std
|
||
|
||
set_option backward.do.legacy false
|
||
|
||
open Lean Meta
|
||
|
||
structure Foo (n : Nat) where
|
||
(l : List Nat)
|
||
(h : n = n)
|
||
|
||
-- same as `foo` in #11337, except replacing `trace` by `logInfo`
|
||
def foo' (n : Nat) : MetaM Unit := do
|
||
let mut result : Foo n := ⟨[7], rfl⟩
|
||
logInfo m!"Initial value of result: {result.l}"
|
||
result := ⟨List.range n, rfl⟩
|
||
logInfo m!"We have a new value of result {result.l}"
|
||
match n with
|
||
| _ => logInfo m!"Now we keep the new value {result.l}"
|
||
|
||
/--
|
||
info: Initial value of result: [7]
|
||
---
|
||
info: We have a new value of result [0, 1, 2, 3, 4]
|
||
---
|
||
info: Now we keep the new value [0, 1, 2, 3, 4]
|
||
-/
|
||
#guard_msgs in
|
||
run_meta do
|
||
foo' 5
|
||
|
||
local instance {α β cmp} [Append β] : Append (Std.TreeMap α β cmp) :=
|
||
⟨.mergeWith (fun _ ↦ (· ++ ·))⟩
|
||
|
||
def bar (hyp? : Option Unit) (a : α) : IO (Std.TreeMap Nat (Array α)) := do
|
||
let mut tree := {}
|
||
if true then
|
||
pure ()
|
||
tree := tree ++ (.insert {} 0 #[a])
|
||
if let some _ := hyp? then
|
||
tree := tree
|
||
return tree
|
||
|
||
/-- info: Std.TreeMap.ofList [(0, #[3])] -/
|
||
#guard_msgs in
|
||
#eval bar none 3
|