The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 02/04/2013 09:25 AM, Jason Gross wrote:
> 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:

Looks like a shallow bug with pretty-printing and parsing not being 
inverses.  (There are some much more interesting bugs of this kind. :])  
The above works with two extra parens:

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.