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

chore(tests/lean): remove tests for command that will be deleted

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-14 08:58:14 -07:00
parent 5a50102e92
commit c64e4267d9
6 changed files with 0 additions and 72 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
tests/lean/abstract_expr1.lean
View file

@ -1,5 +0,0 @@
#abstract_expr 0 @zero
#abstract_expr 0 ℕ
#abstract_expr 0 nat_has_zero
#abstract_expr 0 @zero ℕ
#abstract_expr 0 @zero ℕ nat_has_zero

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

@ -1,5 +0,0 @@
1558663523
3156312089
1320171407
1921459337
1547633539

19
tests/lean/abstract_expr2.lean
View file

@ -1,19 +0,0 @@
universes l1 l2 l3
constants (f : Π (X Y U : Type) (x1 x2 : X) (y1 y2 : Y) (Hx : x1 = x2) (Hy : y1 = y2), U)
constants (X : Type.{l1}) (Y : Type.{l2}) (U : Type.{l3})
constants (x1 x2 : X) (y1 y2 : Y) (Hx1 Hx2 : x1 = x2) (Hy1 Hy2 : y1 = y2)
#abstract_expr 0 f X Y U
#abstract_expr 0 f X Y U x1
#abstract_expr 0 f X Y U x1 x2
#abstract_expr 0 f X Y U x1 x2 y1
#abstract_expr 0 f X Y U x1 x2 y1 y2
#abstract_expr 0 f X Y U x1 x2 y1 y2 Hx1
#abstract_expr 0 f X Y U x1 x2 y1 y2 Hx1 Hy1
#abstract_expr 0 f X Y U x1 x2 y1 y2 Hx2 Hy2
#abstract_expr 1 (f X Y U x1 x2 y1 y2), (f X Y U x1 x2 y1 y2 Hx2 Hy2)
#abstract_expr 1 (f X Y U x1 x2 y1 y2 Hx1 Hy1), (f X Y U x1 x2 y1 y2)
#abstract_expr 1 (f X Y U x1 x2 y1 y2 Hx1), (f X Y U x1 x2 y1 y2 Hx2)
#abstract_expr 1 (f X Y U x1 x2 y1 y2 Hx1 Hy1), (f X Y U x1 x2 y1 y2 Hx2 Hy2)

12
tests/lean/abstract_expr2.lean.expected.out
View file

@ -1,12 +0,0 @@
2197106003
2230813415
735509793
2462481275
3314094375
3314094375
3314094375
3314094375
0
0
1
1

19
tests/lean/abstract_expr3.lean
View file

@ -1,19 +0,0 @@
universes l1 l2
constants (X : Type.{l1}) (P : X → Type.{l2}) (P_ss : ∀ x, subsingleton (P x))
constants (x1 x2 : X) (px1a px1b : P x1) (px2a px2b : P x2)
attribute P_ss [instance]
constants (f : Π (x1 x2 : X), P x1 → P x2 → Prop)
#abstract_expr 0 f
#abstract_expr 0 f x1
#abstract_expr 0 f x1 x2
#abstract_expr 0 f x1 x2 px1a
#abstract_expr 0 f x1 x2 px1b
#abstract_expr 0 f x1 x2 px1a px2a
#abstract_expr 0 f x1 x2 px1a px2b
#abstract_expr 1 f x1 x2, f x2 x1
#abstract_expr 1 f x1 x2, f x1 x2 px1a
#abstract_expr 1 f x1 x2 px1a, f x1 x2 px1b
#abstract_expr 1 f x1 x2 px1a px2a, f x1 x2 px1b
#abstract_expr 1 f x1 x2 px1a px2a, f x1 x2 px1b px2b

12
tests/lean/abstract_expr3.lean.expected.out
View file

@ -1,12 +0,0 @@
3779869529
643001557
4235699031
4235699031
4235699031
4235699031
4235699031
0
0
1
0
1