The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

I have the following code:

  Let fun_eta (a b : Type) (f : a -> b) : (fun x => f x) = f.

    exact eq_refl.

  Defined.

  Set Printing All.

  Print fun_eta.

  Check fun (a b : Type) (f : a -> b) =>

                       @eq_refl (a -> b) (fun x : a => f x) :

                       forall (a b : Type) (f : a -> b),

                       @eq (a -> b) (fun x : a => f x) f.

  (* Toplevel input, characters 77-229:

Error:

In environment

fun_eta := fun (a b : Type) (f : a -> b) =>

                   @eq_refl (a -> b) (fun x : a => f x)

                : forall (a b : Type) (f : a -> b),

                  @eq (a -> b) (fun x : a => f x) f

a : Type

b : Type

f : a -> b

The term "@eq_refl (a -> b) (fun x : a => f x)" has type

 "@eq (a -> b) (fun x : a => f x) (fun x : a => f x)"

 while it is expected to have type

 "forall (a b : Type) (f : a -> b), @eq (a -> b) (fun x : a => f x) f". *)

When I [Print fun_eta.], I get something that doesn't type-check according to [Check] and [Definition].  Is there a way to define this term without using tactics?  Is this a bug in Coq 8.4?

Thanks.

-Jason