Local definitions in mutual inductive type block

Stream: new members

[Avi Craimer]

Hi. I am trying to define a mutually inductive type in Lean 4. For convenience I have a generic structure MorphData which is non-inductive. I need to convert my inductively defined Morph type to MorphData to pass into the mutually inductively defined globular Constraint constructor. It all type checks fine except that for an error under mutual saying, invalid mutual block. I'm guessing that you can't have freestanding function definitions inside the mutual block. I can't move getMorphismData outside the mutual block either since it both relies on and is used in the definitions. I guess what I need is a way to define getMorphismData as a local definition under Morph, but I've tried various ways of using the let syntax and can't get it to work.

structure MorphData (α :Type u) where
  name: Name
  input: α
  output: α
  dimension: Nat
deriving Repr

mutual
  inductive Morph : Nat -> Type u :=
    | unitMorph  : Morph 0
    | liftPair (nm:Name) (i: (Morph n)  ) (o:Morph n) (globularityProof: globular (getMorphData i) (getMorphData o)) : Morph (n+1)

 def getMorphData (mSym: Morph n) : MorphData Morph :=
  match mSym with
  | unitSym => MorphData.mk UnitName unitSym unitSym 0
  | liftPair nm (i: Morph n) o _ => MorphData.mk nm i o n+1

  inductive Constraint :  Type u :=
  | globular (input: MorphismData (Morph n) ) (output: MorphismData (Morph n)) (p:(input = output) ∨ (input.input = output.input ∧ input.output = output.output)) : Constraint
end

[Kevin Buzzard]

You might want to ask this question in the Lean 4 stream; most people who read this stream are Lean 3 users.