Named type params (`inductive`)

Stream: new members

[Max Nowak]

I would have expected the following two inductive definitions to be identical. The only difference is that I assign ohno as a name to the vector length parameter and simply never use it. Or so I thought. Apparently there is a difference and Lean4 forces me to use ohno. Why is this distinction important? I am hoping this will bring me insights into DTT and Lean4's inner workings :D

inductive Vec (α: Type u) (ohno: Nat) : Type u
  | nil  : Vec α 0 -- inductive datatype parameter mismatch 0 expected ohno
  | cons : α -> Vec α n -> Vec α (n+1)

inductive Vect (α: Type u) : Nat -> Type u
  | nil  : Vect α 0
  | cons : α -> Vect α n -> Vect α (n+1)

[Cameron Torrance]

Lean automatically fills in parameters left of the colon, if you want to use a variable as an index put it to the right.

[Kevin Buzzard]

Is the answer to this simply that the very syntax for inductive types depends on what's on either side of the colon?

[Max Nowak]

Thanks for the answers :).
What do you mean with using a variable as an index?

[Cameron Torrance]

I'm not a computer scientist but I think the distinction is that a parameter only says what kinds of stuff live in your type whereas indices control the structure of the type.
edit: I said this wrong, this should help https://stackoverflow.com/questions/24600256/difference-between-type-parameters-and-indices

[Max Nowak]

Ahhhhh, yeah that makes so much sense now!
The key distinction is then that parameters need to be uniform everywhere, but indices can differ in each constructor, because, well, we can use them to fiddle with which constructors are viable in e.g. pattern matching.

[Max Nowak]

Thank you :)