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

chore(tests/lean/run): fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-17 15:46:06 -07:00
parent 423319398d
commit 7ac58c0715
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/run/cases_bug.lean
View file

@ -1,2 +1,2 @@
theorem cast_heq₂ : ∀ {A B : Type} (H : A = B) (a : A), cast H a == a
| A A (eq.refl A) a := heq_of_eq $ cast_eq _ _
| A ⌞A⌟ (eq.refl ⌞A⌟) a := heq_of_eq $ cast_eq _ _

6
tests/lean/run/unreachable_cases.lean
View file

@ -7,13 +7,13 @@ inductive ifin : ℕ → Type -- inductively defined fin-type
open ifin
definition foo {N : Type} : Π{n : ℕ}, N → ifin n → (N × ifin n)
| (succ k) n (fz k) := sorry
| (succ k) n (fz ⌞k⌟) := sorry
| (succ k) n (fs x) := sorry
definition bar {N : Type} : Π{n : ℕ}, (N × ifin n) → (N × ifin n)
| (succ k) (n, fz k) := sorry
| (succ k) (n, fz ⌞k⌟) := sorry
| (succ k) (n, fs x) := sorry
definition bar2 {N : Type} : Π{n : ℕ}, (N × ifin n) → (N × ifin n)
| (succ k) (n, fz k) := sorry
| (succ k) (n, fz ⌞k⌟) := sorry
| (succ k) (n, fs x) := sorry