27 lines
767 B
Text
27 lines
767 B
Text
axiom let_in {A B} (x : A) (f : A -> B) : B
|
|
axiom add (x y : Nat) : Nat
|
|
@[simp] axiom addZero (x : Nat) : add x 0 = x
|
|
syntax "bigAdd0Seq! " num term:max : term
|
|
syntax "bigAddSeq! " num term:max : term
|
|
|
|
macro_rules
|
|
| `(bigAdd0Seq! $n $acc) =>
|
|
let n := n.toNat
|
|
if n == 0 then
|
|
`(add $acc (add $acc 0))
|
|
else
|
|
`(let_in (add $acc (add $acc 0)) (fun acc' => bigAdd0Seq! $(Lean.quote (n - 1)) acc'))
|
|
|
|
macro_rules
|
|
| `(bigAddSeq! $n $acc) =>
|
|
let n := n.toNat
|
|
if n == 0 then
|
|
`(add $acc $acc)
|
|
else
|
|
`(let_in (add $acc $acc) (fun acc' => bigAddSeq! $(Lean.quote (n - 1)) acc'))
|
|
|
|
theorem ex1 (x : Nat) : bigAdd0Seq! 150 x = bigAddSeq! 150 x := by
|
|
simp
|
|
|
|
-- theorem ex2 (x : Nat) : bigAddSeq! 5 x = bigAddSeq! 5 x := by
|
|
-- simp
|