max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(tests/lean/smart_unfolding): remove test since it depends on #reduce

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-04 16:59:09 -07:00
parent d8e7941116
commit c121bcf263
2 changed files with 0 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
tests/lean/smart_unfolding.lean
View file

@ -1,5 +0,0 @@
constant n : nat
#reduce n + (nat.succ n)
set_option type_context.smart_unfolding false
#reduce n + (nat.succ n)

8
tests/lean/smart_unfolding.lean.expected.out
View file

@ -1,8 +0,0 @@
nat.succ (nat.add n n)
nat.succ
((nat.rec ⟨λ (a : ℕ), a, punit.star⟩
(λ (n : ℕ)
(ih : pprod (ℕ → ℕ) (nat.rec punit (λ (n : ℕ) (ih : Type), pprod (pprod (ℕ → ℕ) ih) punit) n)),
⟨λ (a : ℕ), nat.succ (ih.fst a), ⟨ih, punit.star⟩⟩)
n).fst
n)