coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] A query about types.

From: Adam Chlipala <adamc AT csail.mit.edu>
To: Bernard Hurley <bernard AT marcade.biz>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] A query about types.
Date: Thu, 19 Apr 2012 06:37:46 -0400

Bernard Hurley wrote:

++++++++++++++++++++
Inductive eq (A:Type) (x:A) : A ->  Prop :=
   refl_equal : eq A x x.

Definition explain (b: bool) :=
   match b with
     | true =>  True
     | false =>  False
   end.
+++++++++++++++++++

[...]it must be possible for objects
of type "explain true" to exist. I am curious to know what such a thing
would look like.

Example et : explain true := I.

[Coq-Club] A query about types., Bernard Hurley
- Re: [Coq-Club] A query about types., Adam Chlipala
  - Re: [Coq-Club] A query about types., Bernard Hurley