fix(tests/lean): make sure pretty print and parse test passes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
8f455f5965
commit
35ad156a46
2 changed files with 5 additions and 1 deletions
|
@ -1,5 +1,8 @@
|
|||
variables a b c d : Nat
|
||||
axiom H : a + (b + c) = a + (b + d)
|
||||
|
||||
set_option pp::implicit true
|
||||
|
||||
using Nat
|
||||
check add_succr a
|
||||
|
||||
|
|
|
@ -5,6 +5,7 @@
|
|||
Assumed: c
|
||||
Assumed: d
|
||||
Assumed: H
|
||||
Set: lean::pp::implicit
|
||||
Using: Nat
|
||||
Nat::add_succr a : ∀ b : ℕ, a + (b + 1) = a + b + 1
|
||||
Nat::add_succr a : ∀ b : ℕ, @eq ℕ (a + (b + 1)) (a + b + 1)
|
||||
Proved: mul_zerol2
|
||||
|
|
Loading…
Add table
Reference in a new issue