The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Guillaume,

> Coq just checks that this is true for all the branches  of the "match"; if 
> so, it assumes that it is also true for the "match" itself.

Sorry, I don't get it. That is what I assumed Coq does until I saw your 
example, but how does Coq check that (in my example below ) the branch term 
"1" has type "bool"?

Definition foo2 (H : nat = bool) : bool :=
  match H in (_ = t) return t with
  | eq_refl => 1
  end.

Best regards,

Michael


Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928