chore(tests/lean/interactive): remove broken old tests
This commit is contained in:
Leonardo de Moura
parent
e87a27cb4b
commit
a086fb3348
6 changed files with 0 additions and 200 deletions
|
|
@ -1,15 +0,0 @@
|
|||
VISIT alias.lean
|
||||
SET
|
||||
pp.notation false
|
||||
REPLACE 1
|
||||
import data.bool
|
||||
WAIT
|
||||
FINDP 1
|
||||
tt
|
||||
REPLACE 2
|
||||
open bool
|
||||
REPLACE 3
|
||||
check tt
|
||||
WAIT
|
||||
FINDP 3
|
||||
tt
|
||||
|
|
@ -1,46 +0,0 @@
|
|||
-- BEGINSET
|
||||
-- ENDSET
|
||||
-- BEGINWAIT
|
||||
-- ENDWAIT
|
||||
-- BEGINFINDP
|
||||
bool.tt_bxor_tt|eq (bool.bxor bool.tt bool.tt) bool.ff
|
||||
bool.tt_bxor_ff|eq (bool.bxor bool.tt bool.ff) bool.tt
|
||||
bool.bor_tt|∀ a, eq (bool.bor a bool.tt) bool.tt
|
||||
bool.band_tt|∀ a, eq (bool.band a bool.tt) a
|
||||
bool.tt|bool
|
||||
bool.bxor_tt|∀ a, eq (bool.bxor a bool.tt) (bool.bnot a)
|
||||
bool.eq_tt_of_bnot_eq_ff|eq (bool.bnot ?a) bool.ff → eq ?a bool.tt
|
||||
bool.eq_ff_of_bnot_eq_tt|eq (bool.bnot ?a) bool.tt → eq ?a bool.ff
|
||||
bool.ff_bxor_tt|eq (bool.bxor bool.ff bool.tt) bool.tt
|
||||
bool.absurd_of_eq_ff_of_eq_tt|eq ?a bool.ff → eq ?a bool.tt → ?B
|
||||
bool.eq_tt_of_ne_ff|ne ?a bool.ff → eq ?a bool.tt
|
||||
tactic.with_attributes_tac|tactic.expr → tactic.identifier_list → tactic → tactic
|
||||
bool.tt_band|∀ a, eq (bool.band bool.tt a) a
|
||||
bool.cond_tt|∀ t e, eq (bool.cond bool.tt t e) t
|
||||
bool.ff_ne_tt|eq bool.ff bool.tt → false
|
||||
bool.eq_ff_of_ne_tt|ne ?a bool.tt → eq ?a bool.ff
|
||||
bool.tt_bxor|∀ a, eq (bool.bxor bool.tt a) (bool.bnot a)
|
||||
bool.tt_bor|∀ a, eq (bool.bor bool.tt a) bool.tt
|
||||
-- ENDFINDP
|
||||
-- BEGINWAIT
|
||||
-- ENDWAIT
|
||||
-- BEGINFINDP
|
||||
tt|bool
|
||||
tt_bor|∀ a, eq (bor tt a) tt
|
||||
tt_band|∀ a, eq (band tt a) a
|
||||
tt_bxor|∀ a, eq (bxor tt a) (bnot a)
|
||||
tt_bxor_tt|eq (bxor tt tt) ff
|
||||
tt_bxor_ff|eq (bxor tt ff) tt
|
||||
bor_tt|∀ a, eq (bor a tt) tt
|
||||
band_tt|∀ a, eq (band a tt) a
|
||||
bxor_tt|∀ a, eq (bxor a tt) (bnot a)
|
||||
eq_tt_of_bnot_eq_ff|eq (bnot ?a) ff → eq ?a tt
|
||||
eq_ff_of_bnot_eq_tt|eq (bnot ?a) tt → eq ?a ff
|
||||
ff_bxor_tt|eq (bxor ff tt) tt
|
||||
absurd_of_eq_ff_of_eq_tt|eq ?a ff → eq ?a tt → ?B
|
||||
eq_tt_of_ne_ff|ne ?a ff → eq ?a tt
|
||||
tactic.with_attributes_tac|tactic.expr → tactic.identifier_list → tactic → tactic
|
||||
cond_tt|∀ t e, eq (cond tt t e) t
|
||||
ff_ne_tt|eq ff tt → false
|
||||
eq_ff_of_ne_tt|ne ?a tt → eq ?a ff
|
||||
-- ENDFINDP
|
||||
|
|
@ -1,15 +0,0 @@
|
|||
VISIT auto_comp.lean
|
||||
SYNC 8
|
||||
prelude
|
||||
inductive nat := zero : nat | succ : nat → nat
|
||||
inductive bool := ff | tt
|
||||
namespace nat
|
||||
inductive le : nat → nat → Type.{0} := refl : Π a, le a a
|
||||
|
||||
end nat
|
||||
|
||||
WAIT
|
||||
FINDP 6
|
||||
rec_on
|
||||
FINDP 8
|
||||
rec_on
|
||||
|
|
@ -1,12 +0,0 @@
|
|||
-- BEGINWAIT
|
||||
-- ENDWAIT
|
||||
-- BEGINFINDP
|
||||
le.rec_on|le ?a ?a → (Π a, ?C a a) → ?C ?a ?a
|
||||
nat.rec_on|Π n, ?C 0 → (Π a, ?C a → ?C (succ a)) → ?C n
|
||||
bool.rec_on|Π n, ?C bool.ff → ?C bool.tt → ?C n
|
||||
-- ENDFINDP
|
||||
-- BEGINFINDP
|
||||
nat.le.rec_on|nat.le ?a ?a → (Π a, ?C a a) → ?C ?a ?a
|
||||
nat.rec_on|Π n, ?C 0 → (Π a, ?C a → ?C (nat.succ a)) → ?C n
|
||||
bool.rec_on|Π n, ?C bool.ff → ?C bool.tt → ?C n
|
||||
-- ENDFINDP
|
||||
|
|
@ -1,16 +0,0 @@
|
|||
VISIT num2.lean
|
||||
WAIT
|
||||
SET
|
||||
pp.notation false
|
||||
FINDP 39
|
||||
pos_num.si
|
||||
REPLACE 23
|
||||
definition size (a : pos_num) : pos_num :=
|
||||
WAIT
|
||||
REPLACE 39
|
||||
rec (pos pos_num.one) (λp, pos (pos_num.size p)) a
|
||||
WAIT
|
||||
FINDP 39
|
||||
pos_num.si
|
||||
FINDP 26
|
||||
pos_num.si
|
||||
|
|
@ -1,96 +0,0 @@
|
|||
-- BEGINWAIT
|
||||
-- ENDWAIT
|
||||
-- BEGINSET
|
||||
-- ENDSET
|
||||
-- BEGINFINDP
|
||||
pos_num.size|pos_num → pos_num
|
||||
pos_num.bit0|pos_num → pos_num
|
||||
pos_num.is_inhabited|inhabited pos_num
|
||||
pos_num.is_one|pos_num → bool
|
||||
pos_num.inc|pos_num → pos_num
|
||||
pos_num.ibelow|pos_num → Prop
|
||||
pos_num.binduction_on|Π n, (Π n, pos_num.ibelow n → ?C n) → ?C n
|
||||
pos_num.induction_on|Π n, ?C pos_num.one → (Π a, ?C a → ?C (pos_num.bit1 a)) → (Π a, ?C a → ?C (pos_num.bit0 a)) → ?C n
|
||||
pos_num.succ|pos_num → pos_num
|
||||
pos_num.bit1|pos_num → pos_num
|
||||
pos_num.rec|?C pos_num.one → (Π a, ?C a → ?C (pos_num.bit1 a)) → (Π a, ?C a → ?C (pos_num.bit0 a)) → (Π n, ?C n)
|
||||
pos_num.one|pos_num
|
||||
pos_num.below|pos_num → Type
|
||||
pos_num.le|pos_num → pos_num → bool
|
||||
pos_num.cases_on|Π n, ?C pos_num.one → (Π a, ?C (pos_num.bit1 a)) → (Π a, ?C (pos_num.bit0 a)) → ?C n
|
||||
pos_num.pred|pos_num → pos_num
|
||||
pos_num.mul|pos_num → pos_num → pos_num
|
||||
pos_num.no_confusion_type|Type → pos_num → pos_num → Type
|
||||
pos_num.num_bits|pos_num → pos_num
|
||||
pos_num.no_confusion|eq ?v1 ?v2 → pos_num.no_confusion_type ?P ?v1 ?v2
|
||||
pos_num.lt|pos_num → pos_num → bool
|
||||
pos_num.rec_on|Π n, ?C pos_num.one → (Π a, ?C a → ?C (pos_num.bit1 a)) → (Π a, ?C a → ?C (pos_num.bit0 a)) → ?C n
|
||||
pos_num.brec_on|Π n, (Π n, pos_num.below n → ?C n) → ?C n
|
||||
pos_num.add|pos_num → pos_num → pos_num
|
||||
pos_num_has_mul|has_mul pos_num
|
||||
pos_num|Type
|
||||
pos_num_has_one|has_one pos_num
|
||||
pos_num_has_add|has_add pos_num
|
||||
-- ENDFINDP
|
||||
-- BEGINWAIT
|
||||
-- ENDWAIT
|
||||
-- BEGINWAIT
|
||||
-- ENDWAIT
|
||||
-- BEGINFINDP
|
||||
pos_num.size|pos_num → pos_num
|
||||
pos_num.bit0|pos_num → pos_num
|
||||
pos_num.is_inhabited|inhabited pos_num
|
||||
pos_num.is_one|pos_num → bool
|
||||
pos_num.inc|pos_num → pos_num
|
||||
pos_num.ibelow|pos_num → Prop
|
||||
pos_num.binduction_on|Π n, (Π n, pos_num.ibelow n → ?C n) → ?C n
|
||||
pos_num.induction_on|Π n, ?C pos_num.one → (Π a, ?C a → ?C (pos_num.bit1 a)) → (Π a, ?C a → ?C (pos_num.bit0 a)) → ?C n
|
||||
pos_num.succ|pos_num → pos_num
|
||||
pos_num.bit1|pos_num → pos_num
|
||||
pos_num.rec|?C pos_num.one → (Π a, ?C a → ?C (pos_num.bit1 a)) → (Π a, ?C a → ?C (pos_num.bit0 a)) → (Π n, ?C n)
|
||||
pos_num.one|pos_num
|
||||
pos_num.below|pos_num → Type
|
||||
pos_num.le|pos_num → pos_num → bool
|
||||
pos_num.cases_on|Π n, ?C pos_num.one → (Π a, ?C (pos_num.bit1 a)) → (Π a, ?C (pos_num.bit0 a)) → ?C n
|
||||
pos_num.pred|pos_num → pos_num
|
||||
pos_num.mul|pos_num → pos_num → pos_num
|
||||
pos_num.no_confusion_type|Type → pos_num → pos_num → Type
|
||||
pos_num.no_confusion|eq ?v1 ?v2 → pos_num.no_confusion_type ?P ?v1 ?v2
|
||||
pos_num.lt|pos_num → pos_num → bool
|
||||
pos_num.rec_on|Π n, ?C pos_num.one → (Π a, ?C a → ?C (pos_num.bit1 a)) → (Π a, ?C a → ?C (pos_num.bit0 a)) → ?C n
|
||||
pos_num.brec_on|Π n, (Π n, pos_num.below n → ?C n) → ?C n
|
||||
pos_num.add|pos_num → pos_num → pos_num
|
||||
pos_num_has_mul|has_mul pos_num
|
||||
pos_num|Type
|
||||
pos_num_has_one|has_one pos_num
|
||||
pos_num_has_add|has_add pos_num
|
||||
-- ENDFINDP
|
||||
-- BEGINFINDP
|
||||
pos_num.size|pos_num → pos_num
|
||||
pos_num.bit0|pos_num → pos_num
|
||||
pos_num.is_inhabited|inhabited pos_num
|
||||
pos_num.is_one|pos_num → bool
|
||||
pos_num.inc|pos_num → pos_num
|
||||
pos_num.ibelow|pos_num → Prop
|
||||
pos_num.binduction_on|Π n, (Π n, pos_num.ibelow n → ?C n) → ?C n
|
||||
pos_num.induction_on|Π n, ?C pos_num.one → (Π a, ?C a → ?C (pos_num.bit1 a)) → (Π a, ?C a → ?C (pos_num.bit0 a)) → ?C n
|
||||
pos_num.succ|pos_num → pos_num
|
||||
pos_num.bit1|pos_num → pos_num
|
||||
pos_num.rec|?C pos_num.one → (Π a, ?C a → ?C (pos_num.bit1 a)) → (Π a, ?C a → ?C (pos_num.bit0 a)) → (Π n, ?C n)
|
||||
pos_num.one|pos_num
|
||||
pos_num.below|pos_num → Type
|
||||
pos_num.le|pos_num → pos_num → bool
|
||||
pos_num.cases_on|Π n, ?C pos_num.one → (Π a, ?C (pos_num.bit1 a)) → (Π a, ?C (pos_num.bit0 a)) → ?C n
|
||||
pos_num.pred|pos_num → pos_num
|
||||
pos_num.mul|pos_num → pos_num → pos_num
|
||||
pos_num.no_confusion_type|Type → pos_num → pos_num → Type
|
||||
pos_num.no_confusion|eq ?v1 ?v2 → pos_num.no_confusion_type ?P ?v1 ?v2
|
||||
pos_num.lt|pos_num → pos_num → bool
|
||||
pos_num.rec_on|Π n, ?C pos_num.one → (Π a, ?C a → ?C (pos_num.bit1 a)) → (Π a, ?C a → ?C (pos_num.bit0 a)) → ?C n
|
||||
pos_num.brec_on|Π n, (Π n, pos_num.below n → ?C n) → ?C n
|
||||
pos_num.add|pos_num → pos_num → pos_num
|
||||
pos_num_has_mul|has_mul pos_num
|
||||
pos_num|Type
|
||||
pos_num_has_one|has_one pos_num
|
||||
pos_num_has_add|has_add pos_num
|
||||
-- ENDFINDP
|
||||
Loading…
Reference in a new issue