chore(tests/lean): fix style and adjust tests
This commit is contained in:
parent
b81d4d50f1
commit
7e8a394caf
3 changed files with 4 additions and 2 deletions
|
@ -104,7 +104,6 @@ struct print_axioms_deps {
|
||||||
if (!m_use_axioms)
|
if (!m_use_axioms)
|
||||||
m_ios << "no axioms" << endl;
|
m_ios << "no axioms" << endl;
|
||||||
}
|
}
|
||||||
|
|
||||||
};
|
};
|
||||||
|
|
||||||
static void print_axioms(parser & p) {
|
static void print_axioms(parser & p) {
|
||||||
|
|
|
@ -1 +1,2 @@
|
||||||
no axioms
|
quot.sound : ∀ {A : Type} [s : setoid A] {a b : A}, setoid.r a b → quot.mk a = quot.mk b
|
||||||
|
propext : ∀ {a b : Prop}, (a ↔ b) → a = b
|
||||||
|
|
|
@ -1,2 +1,4 @@
|
||||||
|
quot.sound : ∀ {A : Type} [s : setoid A] {a b : A}, setoid.r a b → quot.mk a = quot.mk b
|
||||||
em : ∀ (a : Prop), a ∨ ¬a
|
em : ∀ (a : Prop), a ∨ ¬a
|
||||||
|
propext : ∀ {a b : Prop}, (a ↔ b) → a = b
|
||||||
strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → { (x : A)| Exists P → P x}
|
strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → { (x : A)| Exists P → P x}
|
||||||
|
|
Loading…
Reference in a new issue