You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Lib/Foundation.v defines notations for ∀ , ∃, and λ
If user code imports both Category.Lib and Utf8 from the Coq standard library, we get the following error message
Error: Notation "∀ _ .. _ , _" is already defined at level 200 with arguments
binder, constr at level 200 while it is now required to be at level 10
with arguments binder, constr at level 200.
The following patch seems enough to work around this issue: I confirmed category-theory compiles and so does my code.
Before proposing a pull request, I am curious about your feedback on this. I must admit my patch is pretty arbitrary, it ressembles the notation definition from the Coq standard library to avoid conflicts.
diff --git a/Lib/Foundation.v b/Lib/Foundation.v
index 82f7455..560a8c2 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.
Thanks,
The text was updated successfully, but these errors were encountered:
Lib/Foundation.v
defines notations for ∀ , ∃, and λIf user code imports both
Category.Lib
andUtf8
from the Coq standard library, we get the following error messageThe following patch seems enough to work around this issue: I confirmed
category-theory
compiles and so does my code.Before proposing a pull request, I am curious about your feedback on this. I must admit my patch is pretty arbitrary, it ressembles the notation definition from the Coq standard library to avoid conflicts.
Thanks,
The text was updated successfully, but these errors were encountered: