michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(tests/lean): adjust tests to reflect changes in the standard library

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-01 15:09:00 -07:00
parent 0d66d19ba3
commit bf142f3f18
3 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/print_ax2.lean
View file

@ -1,3 +1,3 @@
import logic.axioms.hilbert logic.axioms.funext
import logic.axioms.hilbert logic.axioms.em
print axioms

4
tests/lean/print_ax2.lean.expected.out
View file

@ -1,2 +1,2 @@
funext : ∀ {A : Type} {B : A → Type} {f g : Π (a : A), B a}, (∀ (a : A), f a = g a) → f = g
strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → { (x : A) | (∃ (y : A), P y) → P x }
em : ∀ (a : Prop), a ∨ ¬a
strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → { (x : A)| (∃ (y : A), P y) → P x}

2
tests/lean/struct_class.lean.expected.out
View file

@ -4,6 +4,7 @@ measurable : Type → Type
nonempty : Type → Prop
point : Type → Type → Type
setoid : Type → Type
subsingleton : Type → Prop
well_founded : Π {A : Type}, (A → A → Prop) → Prop
decidable : Prop → Type₁
inhabited : Type → Type
@ -11,4 +12,5 @@ measurable : Type → Type
nonempty : Type → Prop
point : Type → Type → Type
setoid : Type → Type
subsingleton : Type → Prop
well_founded : Π {A : Type}, (A → A → Prop) → Prop