The Coq mailing list

[Randy Pollack <rpollack AT inf.ed.ac.uk>]

I am unclear about Coq's type casting.

Consider

Check (cons: forall (A:Set), A -> list A -> list A).
(fun A : Set => cons (A:=A)):forall A : Set, A -> list A -> list A
     : forall A : Set, A -> list A -> list A

It looks like the cast [ (cons: forall (A:Set), A -> list A -> list A).] is
a meta-notation for the eta-expansion.  Then why is the cast still in the 
term?

Now consider

Goal (cons: forall (A:Set), A -> list A -> list A) =
       (cons: forall (A:Set), A -> list A -> list A).
cbv beta.

Goal is:

   (fun A : Set => cons (A:=A)) = (fun A : Set => cons (A:=A))

The cast was removed even though no beta steps were taken.  What is
the official story about when casts are removed in Coq?

Finally consider

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

The Goal is

((fun A : Set => cons (A:=A)):forall A : Set, A -> list A -> list A) =
(fun A : Set => cons (A:=A))

Why was the RHS eta expanded in this way?  This is not the goal I
entered; this goal is true (solved by reflexivity), but the tactic

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

fails.

Best,
Randy
--