From c121bcf26304dc39db1fcad495fced6e6d812f5d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 4 Sep 2018 16:59:09 -0700 Subject: [PATCH] chore(tests/lean/smart_unfolding): remove test since it depends on `#reduce` --- tests/lean/smart_unfolding.lean | 5 ----- tests/lean/smart_unfolding.lean.expected.out | 8 -------- 2 files changed, 13 deletions(-) delete mode 100644 tests/lean/smart_unfolding.lean delete mode 100644 tests/lean/smart_unfolding.lean.expected.out diff --git a/tests/lean/smart_unfolding.lean b/tests/lean/smart_unfolding.lean deleted file mode 100644 index 58ab4ef7b6..0000000000 --- a/tests/lean/smart_unfolding.lean +++ /dev/null @@ -1,5 +0,0 @@ -constant n : nat -#reduce n + (nat.succ n) - -set_option type_context.smart_unfolding false -#reduce n + (nat.succ n) diff --git a/tests/lean/smart_unfolding.lean.expected.out b/tests/lean/smart_unfolding.lean.expected.out deleted file mode 100644 index f1243c7056..0000000000 --- a/tests/lean/smart_unfolding.lean.expected.out +++ /dev/null @@ -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)