08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
27 lines
1.7 KiB
Text
27 lines
1.7 KiB
Text
recursor foo.rec.{u} : {motive_1 : foo → Sort u} →
|
|
{motive_2 : arrow Nat foo → Sort u} →
|
|
((a : arrow Nat foo) → motive_2 a → motive_1 (foo.mk a)) →
|
|
((a : Nat → foo) → ((a_1 : Nat) → motive_1 (a a_1)) → motive_2 (arrow.mk a)) → (t : foo) → motive_1 t
|
|
number of parameters: 0
|
|
number of indices: 0
|
|
number of motives: 2
|
|
number of minors: 2
|
|
rules:
|
|
for foo.mk (1 fields): fun motive_1 motive_2 mk mk_1 a => mk a (foo.rec_1 mk mk_1 a)
|
|
@[reducible] protected def foo.below.{u} : {motive_1 : (t : foo) → Sort u} →
|
|
{motive_2 : (t : arrow.{0, 0} Nat foo) → Sort u} → (t : foo) → Sort (max 1 u) :=
|
|
fun {motive_1 : (t : foo) → Sort u} {motive_2 : (t : arrow.{0, 0} Nat foo) → Sort u} (t : foo) =>
|
|
@foo.rec.{(max 1 u) + 1} (fun (t : foo) => Sort (max 1 u)) (fun (t : arrow.{0, 0} Nat foo) => Sort (max 1 u))
|
|
(fun (a : arrow.{0, 0} Nat foo) (a_ih : Sort (max 1 u)) => PProd.{u, max 1 u} (motive_2 a) a_ih)
|
|
(fun (a : Nat → foo) (a_ih : Nat → Sort (max 1 u)) =>
|
|
(a_1 : Nat) → PProd.{u, max 1 u} (motive_1 (a a_1)) (a_ih a_1))
|
|
t
|
|
@[reducible] protected def foo2.brecOn.{u} : {motive_1 : (t : foo2) → Sort u} →
|
|
{motive_2 : (t : arrow2) → Sort u} →
|
|
(t : foo2) →
|
|
(F_1 : (t : foo2) → (f : @foo2.below.{u} motive_1 motive_2 t) → motive_1 t) →
|
|
(F_2 : (t : arrow2) → (f : @arrow2.below.{u} motive_1 motive_2 t) → motive_2 t) → motive_1 t :=
|
|
fun {motive_1 : (t : foo2) → Sort u} {motive_2 : (t : arrow2) → Sort u} (t : foo2)
|
|
(F_1 : (t : foo2) → (f : @foo2.below.{u} motive_1 motive_2 t) → motive_1 t)
|
|
(F_2 : (t : arrow2) → (f : @arrow2.below.{u} motive_1 motive_2 t) → motive_2 t) =>
|
|
(@foo2.brecOn.go.{u} motive_1 motive_2 t F_1 F_2).1
|