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-07-24 09:59:49 -07:00
parent 066b0fcdf9
commit f7440ff068
3 changed files with 2 additions and 41 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
tests/lean/630.lean.expected.out
View file

@ -1,6 +1,5 @@
inductive pnat.pnat : Type₁
constructors:
pnat.pnat.pos : Π (n : ℕ), nat.gt n (nat.of_num 0) → ℕ+
definition pnat.pnat : Type₁ :=
{ (n : ℕ)| nat.gt n (nat.of_num 0)}
inductive prod : Type → Type → Type
constructors:
prod.mk : Π {A : Type} {B : Type}, A → B → A × B

5
tests/lean/rw_set3.lean
View file

@ -1,5 +0,0 @@
import data.nat
attribute nat.add.comm [simp]
print [simp]

33
tests/lean/rw_set3.lean.expected.out
View file

@ -1,33 +0,0 @@
simplification rules for iff
#1, ?M_1 ↔ false ↦ ¬?M_1
#1, ?M_1 ↔ true ↦ ?M_1
#0, false ↔ true ↦ false
#0, true ↔ false ↦ false
#1, ?M_1 ↔ ¬?M_1 ↦ false
#1, ?M_1 ↔ ?M_1 ↦ true
#1, false ↔ ?M_1 ↦ ¬?M_1
#1, true ↔ ?M_1 ↦ ?M_1
#3 perm, ?M_1 ∧ ?M_2 ∧ ?M_3 ↦ ?M_2 ∧ ?M_1 ∧ ?M_3
#1, ?M_1 ∧ ?M_1 ↦ ?M_1
#1, false ∧ ?M_1 ↦ false
#1, ?M_1 ∧ false ↦ false
#1, true ∧ ?M_1 ↦ ?M_1
#1, ?M_1 ∧ true ↦ ?M_1
#3, (?M_1 ∧ ?M_2) ∧ ?M_3 ↦ ?M_1 ∧ ?M_2 ∧ ?M_3
#2 perm, ?M_1 ∧ ?M_2 ↦ ?M_2 ∧ ?M_1
#2, ?M_2 == ?M_2 ↦ true
#3 perm, ?M_1 ∨ ?M_2 ∨ ?M_3 ↦ ?M_2 ∨ ?M_1 ∨ ?M_3
#1, false ∨ ?M_1 ↦ ?M_1
#1, ?M_1 ∨ false ↦ ?M_1
#1, true ∨ ?M_1 ↦ true
#1, ?M_1 ∨ true ↦ true
#3, (?M_1 ∨ ?M_2) ∨ ?M_3 ↦ ?M_1 ∨ ?M_2 ∨ ?M_3
#2 perm, ?M_1 ∨ ?M_2 ↦ ?M_2 ∨ ?M_1
#2, ?M_2 = ?M_2 ↦ true
#0, ¬false ↦ true
#0, ¬true ↦ false
simplification rules for eq
#2 perm, nat.add ?M_1 ?M_2 ↦ nat.add ?M_2 ?M_1
#3, ite false ?M_2 ?M_3 ↦ ?M_3
#3, ite true ?M_2 ?M_3 ↦ ?M_2
#4, ite ?M_1 ?M_4 ?M_4 ↦ ?M_4