The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

I did something what I wanted by record types but then I returned to the first way as it was better.

For example, if I have function 'plus' for vectors or matrices, then parameters n, m guarantees that I can use this function on vectors/matrices of equal size. Or parameters m, n, k allows me multiply only matrices with correct sizes. Etc.

Also there's similar possibilities with Type parameters, too - such restrictions also can be useful sometimes.

If I make it with records then I have to check so many things that it becomes too complicated and complex.

On Thu, Jun 27, 2013 at 7:54 PM, <ilmars.cirulis AT gmail.com> wrote:

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!