mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
32 lines
825 B
Lean4
32 lines
825 B
Lean4
abbrev M := ExceptT String $ StateT Nat Id
|
|
|
|
/- The following instances are not needed, but they speedup the proof -/
|
|
instance : Monad M := inferInstance
|
|
instance : LawfulMonad M := inferInstance
|
|
instance : MonadStateOf Nat M := inferInstance
|
|
instance : Bind M := inferInstance
|
|
instance : Pure M := inferInstance
|
|
|
|
syntax "bigAdd0Seq! " num : term
|
|
|
|
macro_rules
|
|
| `(bigAdd0Seq! $n) =>
|
|
let n := n.toNat
|
|
if n == 0 then
|
|
`(pure ())
|
|
else
|
|
`(get >>= fun n => set (0 + n) >>= fun _ => bigAdd0Seq! $(Lean.quote (n - 1)))
|
|
|
|
@[simp] theorem get_set : (get >>= fun n => set n) = (pure () : M Unit) :=
|
|
rfl
|
|
|
|
set_option maxRecDepth 1000000
|
|
set_option maxHeartbeats 1000000
|
|
|
|
theorem ex : (bigAdd0Seq! 40 : M Unit) = pure () := by
|
|
simp
|
|
|
|
-- set_option pp.explicit true
|
|
-- set_option pp.notation false
|
|
-- #print ex
|