From cfe88ee172aea77e456c47a33375c5aa60387815 Mon Sep 17 00:00:00 2001 From: Jerome Hugues Date: Wed, 18 Sep 2024 08:44:03 -0400 Subject: [PATCH] =?UTF-8?q?Update=20notation=20definition=20for=20?= =?UTF-8?q?=E2=88=80=20,=20=E2=88=83,=20and=20=CE=BB=20to=20avoid=20errors?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Lib/Foundation.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Lib/Foundation.v b/Lib/Foundation.v index 06bb42c4..b5604894 100644 --- a/Lib/Foundation.v +++ b/Lib/Foundation.v @@ -31,7 +31,7 @@ Arguments Basics.arrow _ _ /. Arguments Datatypes.id {_} _ /. Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) - (at level 200, x binder, y binder, right associativity) : + (at level 10, x binder, y binder, P at level 200, right associativity) : category_theory_scope. Notation "'exists' x .. y , p" := (sigT (fun x => .. (sigT (fun y => p)) ..)) @@ -40,7 +40,7 @@ Notation "'exists' x .. y , p" := (sigT (fun x => .. (sigT (fun y => p)) ..)) category_theory_scope. Notation "∃ x .. y , P" := (exists x, .. (exists y, P) ..) - (at level 200, x binder, y binder, right associativity) : + (at level 10, x binder, y binder, P at level 200, right associativity) : category_theory_scope. Notation "x → y" := (x -> y) @@ -55,5 +55,5 @@ Infix "∧" := prod (at level 80, right associativity) : category_theory_scope. Infix "∨" := sum (at level 85, right associativity) : category_theory_scope. Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..) - (at level 200, x binder, y binder, right associativity) : + (at level 10, x binder, y binder, t at level 200, right associativity) : category_theory_scope.