The Coq mailing list

[Michael Nahas <mike.nahas AT gmail.com>]

I have a type "nat_mod".  So, "nat_mod 3" are the natural numbers modulo 3.  Obviously, "nat_mod 3 1" will be equal to "nat_mod 3 4".

I feel like Coq, in a given context, should be able to coerce a "nat" into a "nat_modulo <N>".  

The code looks something like: 

(* This will change... *)

Definition nat_mod (n:nat) : Type 

  := {x | x < n}.

Theorem nat_mod_from_nat {n:nat} (x : nat) : nat_mod n.

Admitted.

(* This fails: *) 

Coercion nat_mod_from_nat : nat >-> nat_mod.

Check (10 : nat_mod 5).

Basically, the problem seems to be that I can't pick up the modulo value from the context.  (It can't figure out the implicit parameter "n" of "nat_mod_from_nat".)

Coq accepts if I do:

Coercion nat_mod_from_nat : nat >-> Funclass.

But I don't know what "Funclass" means.

Can Coq do what I want?

Mike