Mutually defined function and type

Stream: new members

[Op From The Start]

I have a minimal recreation of what I need to do:

mutual
inductive Test
| mk: (T: Type) → (m: T→Test) → (h: ∀t: T, f (m t)) → Test

def f: Test → Prop := sorry
end

But I get the error:

invalid mutual block: either all elements of the block must be inductive/structure declarations, or they must all be definitions/theorems/abbrevs

How would I be able to mutually define a recursive type and function at the same time? They really cant be separated, and f is a recursive function so I don't think I could rewrite it inside Test.mk.

[Aaron Liu]

I don't think Lean supports this kind of inductive-recursive definition

[Op From The Start]

Do you know if there is another proof language that would support this?

[Aaron Liu]

Can I ask what exactly you're trying to express?

[Aaron Liu]

you might be able to get away with a subtype

[Op From The Start]

The surreal numbers.
I tried a method by omitting the predicate and then trying to add it back in:

inductive PreNo
 | mk :(L R:Type)→ (L→PreNo)→(R→PreNo)→PreNo

inductive No
 | mk: (n: PreNo) → (∀l: left n, ∀r: right n, ¬ (le (rightm n r) (leftm n l))) → No

But then I don't have left and right sets of No, I have left and right sets of PreNo.

[Aaron Liu]

Maybe you can take a look at how they were defined in the CGT repo:
link

/-- The type of surreal numbers. These are the numeric games quotiented by the antisymmetrization
relation `x ≈ y ↔ x ≤ y ∧ y ≤ x`. In the quotient, the order becomes a total order. -/
def Surreal : Type (u + 1) :=
  Antisymmetrization (Subtype Numeric) (· ≤ ·)