The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Have you read the chapters of Certified Programming with Dependent Types <http://adam.chlipala.net/cpdt/> about programming with dependent types?  I have a feeling that you'll find all or most of your answers there.

On 06/21/2016 08:50 AM, Mwyann wrote:

Dear Michael,
Thanks a lot for your fast and complete answer. Indeed, I think I’m still confused with types and values. What I’m really looking after is to match the type of a value, for example we would like to make this work as you would imagine:
Inductive some_type := A | B | C.
Definition type (t:Type): nat := match t with | bool => 0 | nat => 1 (* error: redundant *) | some_type => 2 | _ => 99 (* any other type *) end.
Compute type 1. (* would return “1” as “nat” *)
I don’t know what mechanism we can use to determine the type of a term (apart from the internal Coq’s type checking).
Do you know if any lectures on the subject exists somewhere? (especially courses that contains examples, which help learning efficiently).
Best regards,

Yann

2016-06-21 10:48 GMT+02:00 Soegtrop, Michael <michael.soegtrop AT intel.com>:

Dear Yann,

 

 [...]