coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Type Casting?

From: Randy Pollack <rpollack AT inf.ed.ac.uk>
To: Coq-Club Club <coq-club AT inria.fr>
Subject: [Coq-Club] Type Casting?
Date: Tue, 28 Apr 2015 12:20:33 +0100

I realize I am unclear about Coq's type casting. Here is one example.

Goal (cons: forall (A:Set), A -> list A -> list A) = cons.
constr_eq (cons: forall (A:Set), A -> list A -> list A) cons.
compute.

[Coq-Club] Type Casting?, Randy Pollack, 04/28/2015