From bfb8f04eabdc7387838a66ecf2ea2a59ae73b3c3 Mon Sep 17 00:00:00 2001
From: Gregory Malecha
Date: Wed, 27 May 2020 18:08:14 +0200
Subject: [PATCH] notation for forall
---
theories/base.v | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/theories/base.v b/theories/base.v
index 538dd41..ba67b79 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -190,6 +190,11 @@ embedded logics. *)
Notation "'True'" := True (format "True") : type_scope.
Notation "'False'" := False (format "False") : type_scope.
+(** Change [forall] into a notation in order to enable overloading. *)
+Notation "'forall' x .. y , P" := (forall x, .. (forall y, P%type) ..)
+ (at level 200, x binder, y binder, right associativity,
+ only parsing) : type_scope.
+
(** * Equality *)
(** Introduce some Haskell style like notations. *)
--
GitLab