Zulip Chat Archive

Stream: new members

Topic: Local definitions in mutual inductive type block

Avi Craimer (Sep 12 2022 at 09:37):

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

  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

Kevin Buzzard (Sep 12 2022 at 12:32):

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

Last updated: Dec 20 2023 at 11:08 UTC