The Coq mailing list

[<ilmars.cirulis AT gmail.com>]

Definition firstN (n:nat): Type := {m: nat | m<n}.
Definition vector (n:nat) (A:Type): Type := (firstN n) -> A.
Definition matrix (n m:nat) (A:Type): Type := (firstN n) -> (firstN m) -> A.

I just wrote such code and started to think - how can I make functions that
uses any of these Types but doesn't need all parameters each time.

For example, I have function
Definition firstN_to_nat (n: nat) (t: firstN n) := projT1 t.

Can I make something like this (examples with completely imaginary syntax)? Or
I have to use record types (or something else)?
Definition firstN_to_nat t: firstN := projT1 t.
Definition just_example t: firstN := firstN.n + (projT1 t).


Thanks in advance!