Defining Vec as inductive with length as first argument

Stream: lean4

[ohhaimark]

I have Vec defined like this

inductive Vec' (α : Type)  :  Nat → Type :=
  | unit : Vec' α 0
  | cons : α → Vec' α n → Vec' α (n+1)

def Vec := flip Vec'

but I would like to have Vec : Nat -> Type -> Type as an inductive type directly. Is this possible?

[François G. Dorais]

The syntax for inductive types requires all parameters to occur before indices. In your definition α is a parameter and n is an index. If you reverse the order, then α is forced to be an index and that causes a universe bump:

inductive A.Vec : Type _ → Nat → Type _ :=
  | unit : Vec α 0
  | cons : α → Vec α n → Vec α (n+1)

inductive B.Vec :  Nat → Type _ → Type _ :=
  | unit : Vec 0 α
  | cons : α → Vec n α → Vec (n+1) α

#check A.Vec -- Type u_1 → Nat → Type u_1
#check B.Vec -- Nat → Type u_1 → Type (u_1+1)

[Tomas Skrivan]

But that results in an universe bump, which is quite undesirable.

[François G. Dorais]

In ancient times, both A.Vec and B.Vec would have a universe bump since the colon was the division between parameters and indices. The current behavior is already much improved.

[François G. Dorais]

Having mixed parameters and indices would require some deep changes. For example, in the InductiveVal structure, only the number of indices is recorded, which is sufficient since they are necessarily last.

[Tomas Skrivan]

I see, there are probably some deep theoretical reasons for it but for me such universe bumb would be unacceptable.

[Mac]

ohhaimark said:

but I would like to have Vec : Nat -> Type -> Type as an inductive type directly. Is this possible?

Why not just use an abbreviation? That is:

abbrev Vec (n : Nat) (α : Type) := Vec' α n

[Henrik Böving]

That's isomorphic to the flip suggestion they made no?

[Mac]

No, flip is a def not an abbrev (and is not marked @[reducible]) and neither is their def Vec, so their shorthand is not reducible, whereas the abbrev is (which, of course, matters for things like typeclasses).

[ohhaimark]

The only thing is that you don't get the generated definitions. Speaking of which, is there a wildcard export like:

namespace Vec
  export Vec' (*)
end Vec

[Mac]

Sadly, no