The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 21/12/2014 23:25, Abhishek Anand wrote:
> Is there some way in Coq to write dependent
> function types in the former way?

Since at least coq trunk, the arrow is a notation defined in the prelude
as follows.

Reserved Notation "x -> y" (at level 99, right associativity, y at level
200).

I believe that using -noinit and tweaking this definition, you may
obtain what you're looking for.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature