Tree Type Termination Trouble

Stream: lean4

[Jesse Slater]

I've inductively defined TreeType which represents the type of trees where each leaf has type T. The asType function obviously terminates, but I don't know how to prove it. Is it possible to do this safely?

inductive HList {α : Type} (β : α → Type) : List α → Type
  | nil : HList β []
  | cons : β a → HList β as → HList β (a :: as)

inductive TreeType
  | leaf : TreeType
  | nest : List TreeType → TreeType

unsafe def TreeType.asType (T : Type)
  | leaf => T
  | nest l => HList (TreeType.asType T) l

def tree_type : TreeType := .nest [.leaf, .nest []]

unsafe def bool_tree : tree_type.asType Bool := .cons true (.cons .nil .nil)

[Aaron Liu]

this doesn't actually terminate in the sense that Lean wants

[Aaron Liu]

I can give you an alternative definition that works just as well

[Aaron Liu]

Is this acceptable?

inductive TreeType
  | leaf : TreeType
  | nest : List TreeType → TreeType

def TreeType.AsType (T : Type)
  | leaf => T
  | nest l => ListType l
where
  ListType (l : List TreeType) :=
    match l with
    | [] => Unit
    | a :: as => AsType T a × ListType as

def tree_type : TreeType := .nest [.leaf, .nest []]

def bool_tree : tree_type.AsType Bool := (true, (), ())

[Jesse Slater]

Thank you! I think that works for me!