## Stream: new members

### Topic: mutual recursive induction and def

#### kana (Mar 19 2021 at 22:34):

def f : t -> Type := match ...
inductive t : bool -> Type
| y : t false
| x : forall (a : t) -> f a -> t true


is it possible to define such thing?

#### Mario Carneiro (Mar 19 2021 at 22:36):

can you make a #mwe?

#### Mario Carneiro (Mar 19 2021 at 22:37):

This is an inductive-recursive type, and the answer is no, at least not directly

#### Mario Carneiro (Mar 19 2021 at 22:37):

but it might be possible to refactor the recursive function into an inductive relation, and then you can do it by mutual induction

#### Mario Carneiro (Mar 19 2021 at 22:39):

Your sketch doesn't typecheck, because t is not a type but you wrote forall (a : t)

#### kana (Mar 19 2021 at 22:43):

It is not mwe, because I don't know how to make it workable

inductive type
| u -- u means type of type
| unit
open type

inductive term : type → Type
| type : type → term u -- injection of types into terms
| tt : term unit
| the : ∀(α : term u), term (from_type α) → term (from_type α)
open term

def from_type : term u → type
| (term.type x) := x
| (term.the _ x) := from_type x


#### Mario Carneiro (Mar 19 2021 at 22:53):

You can encode this much using a well-formedness predicate on terms:

inductive type
| u
| unit
open type

inductive term : type → Type
| type : type → term u
| tt : term unit
| the : ∀ (β : type) (α : term u), term β → term u

def from_type : ∀ {α}, term α → option type
| _ (term.type x) := some x
| _ term.tt := none
| _ (term.the β _ _) := some β

def term.wf : ∀ {α}, term α → Prop
| _ (term.the β α x) := from_type x = some β ∧ α.wf ∧ x.wf
| _ (term.type _) := true
| _ term.tt := true

def wfterm (α : type) : Type := { t : term α // t.wf }


#### kana (Mar 19 2021 at 23:13):

Thanks!

Last updated: May 08 2021 at 04:14 UTC