15 lines
233 B
Text
15 lines
233 B
Text
|
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
|