fix(tests/lean/run): adjust tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
3903be34a4
commit
c11fd6b0d2
2 changed files with 3 additions and 3 deletions
|
@ -44,5 +44,5 @@ theorem T3 : aux2 = N2.foo (f a) (f b)
|
|||
|
||||
|
||||
check foo a b
|
||||
theorem T4 : foo a b = N1.foo a b
|
||||
theorem T4 : foo a b = N2.foo a b
|
||||
:= refl _
|
||||
|
|
|
@ -49,8 +49,8 @@ theorem sum_inhabited_right [instance] {A B : Type} (H : inhabited B) : inhabite
|
|||
inhabited_mk (inr A (default B))
|
||||
|
||||
theorem sum_eq_decidable [instance] {A B : Type} (s1 s2 : A + B)
|
||||
(H1 : ∀a1 a2, decidable (inl B a1 = inl B a2))
|
||||
(H2 : ∀b1 b2, decidable (inr A b1 = inr A b2)) : decidable (s1 = s2) :=
|
||||
(H1 : ∀a1 a2 : A, decidable (inl B a1 = inl B a2))
|
||||
(H2 : ∀b1 b2 : B, decidable (inr A b1 = inr A b2)) : decidable (s1 = s2) :=
|
||||
rec_on s1
|
||||
(take a1, show decidable (inl B a1 = s2), from
|
||||
rec_on s2
|
||||
|
|
Loading…
Reference in a new issue