Hello.

I am reading “Mathematical Components”, 1.3.1

Inductive seq (A : Type) := nil | cons (hd : A) (tl : seq A).

… (seq nat) is the type of sequences of natural numbers, while (seq bool) is the type of sequences of booleans.

Check seq nat.

seq nat

: Set

Check seq bool.

seq bool

: Set

So far so good.

Check seq 5.

Error: The term “5” has type “nat” while it is expected to have type “Type”.

This is expected. But

Check seq true.

seq true

: Set

Is this a feature or a bug?