How to derive constructors in composition

Stream: new members

[MrQubo]

I have a structure that is a composition of some inductive definition. Is there some way to maybe automatically derive constructors for the composed structure, as in the following example?

inductive Typ
| const : String → Typ
| arr : Typ → Typ → Typ
deriving DecidableEq

inductive Term
| bvar : (bi : Nat) → Term
| app : (func : Term) → (arg : Term) → Term
| lam : (arg_type : Typ) → (body : Term) → Term
deriving DecidableEq

structure TypedTerm where
  term : Term
  type : Typ
deriving DecidableEq

def TypedTerm.bvar (bi : Nat) (type : Typ) : TypedTerm := { term := Term.bvar bi, type }
def TypedTerm.app (func : TypedTerm) (arg : TypedTerm) (type : Typ) : TypedTerm := { term := Term.app func.term arg.term, type }
def TypedTerm.lam (arg_type : Typ) (body : TypedTerm) (type : Typ) : TypedTerm := { term := Term.lam arg_type body.term, type }

[Aaron Liu]

No, I don't think so.