inductive definition

Stream: lean4

[Anders Christiansen Sørby]

Why does this work:

inductive Instruction (index : Type) :=
    | Block (body : Instruction index) : Instruction index

But this doesn't

inductive Instruction (index : Type) :=
    | Block (body : Instruction Nat) : Instruction index

And what can I do to fix it? I'm trying to translate a haskell program.

[Kevin Buzzard]

#backticks is a reference for how backticks work for quoting code on Zulip

[Sébastien Michelland]

If you put index in that position, it is fixed for the whole definition. You can make it a parameter an index of the inductive type instead, which allows you to substitute it (but puts your definition in Type 1):

inductive Instruction: (index : Type) → Type 1 :=
    | Block (body : Instruction Nat) : Instruction index

[Anders Christiansen Sørby]

Oh, so this means I need to use universe arguments.

[Jannis Limperg]

Sébastien Michelland said:

You can make it a parameter of the inductive type instead

What you're describing (index after the colon) is an index; Anders' version (index before the colon) is a parameter. Sorry about the nitpicking but it seems necessary here to avoid confusion.

[Sébastien Michelland]

You're right! I should have checked, thanks for raising it.

[Mario Carneiro]

note that in later versions of lean 4 it will make things indices / parameters regardless of which side of the colon they are on, it does an analysis instead to see what changes

[Mario Carneiro]

actually on testing that seems to be only half true: it will turn indices into parameters but not vice versa

[Leonardo de Moura]

The following thread is relevant:
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Simp.20extension/near/276900758