mutual inductives

Stream: general

[Chris Hughes]

What's the "canonical" proof that the Types A and B are empty. I proved it by reference to the auxiliary A._mut_. Is there a nicer way?

mutual inductive A, B
with A : Type
| mk : B → A
with B : Type
| mk : A → B

[Kenny Lau]

mutual inductive A, B
with A : Type
| mk : B → A
with B : Type
| mk : A → B

def A.to_sort (l : Sort*) : A → l
| (A.mk (B.mk x)) := A.to_sort x

[Chris Hughes]

Of course.

[Chris Hughes]

Are there any recursors that look a bit like this?

def AB.reca : Π {Ca : A → Sort*} {Cb : B → Sort*}
  (ha : Π a : A, Ca a → Cb (B.mk a))
  (hb : Π b : B, Cb b → Ca (A.mk b))
  (a : A), Ca a

[Kenny Lau]

you can write one