| abbrev M := ExceptT String $ StateT Nat Id | |
| def add (n : Nat) : M Unit := | |
| modify (ยท + 0) | |
| @[simp] theorem addZero : add (natLit! 0) = pure () := | |
| rfl | |
| syntax "bigAdd0Seq! " num : term | |
| macro_rules | |
| | `(bigAdd0Seq! $n) => | |
| let n := n.toNat | |
| if n == 0 then | |
| `(pure ()) | |
| else | |
| `(add (natLit! 0) >>= fun _ => bigAdd0Seq! $(Lean.quote (n - 1))) | |
| set_option maxRecDepth 10000 | |
| theorem ex : bigAdd0Seq! 10 = pure () := by | |
| simp | |
| -- set_option pp.explicit true | |
| -- set_option pp.notation false | |
| -- #print ex |