The Coq mailing list

[Bernard Hurley <bernard AT marcade.biz>]

Hi All,

I'm fairly new to Coq and I am still trying to figure out how types
work.

If I do:

++++++++++++++++++++
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.

Check eq_ind bool true explain.
+++++++++++++++++++

I get the response:

+++++++++++++++++
eq_ind bool true explain
     : explain true -> forall y : bool, eq bool true y -> explain y
+++++++++++++++++

This suggests to me that at this point it must be possible for objects
of type "explain true" to exist. I am curious to know what such a thing
would look like.

Regards,

Bernard.