coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Agda-like notation for dependent function types

From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Agda-like notation for dependent function types
Date: Mon, 22 Dec 2014 11:18:05 +0100

The following works for me™ (in Coq trunk):

Notation "( x : A ) -> B" := (forall (x : A), B) (at level 99, right
associativity, x at level 0, B at level
200) : type_scope.

Definition foo : ( x : nat ) -> x = x := fun x => eq_refl.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] Agda-like notation for dependent function types, Abhishek Anand, 12/21/2014
- Re: [Coq-Club] Agda-like notation for dependent function types, Pierre-Marie Pédrot, 12/22/2014
  - Re: [Coq-Club] Agda-like notation for dependent function types, Jason Gross, 12/22/2014
    - Re: [Coq-Club] Agda-like notation for dependent function types, Pierre-Marie Pédrot, 12/22/2014