Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix binding of type_scope to Sortclass #2038

Merged
merged 3 commits into from
Aug 1, 2024

Conversation

Alizter
Copy link
Collaborator

@Alizter Alizter commented Jul 31, 2024

We fix the order in which we bind type_scope to Sortclass allowing targets of function types to automatically be interpreted as types. This allows us to remove %type annotations throughout the library.

One obvious benefit from this is that when working with nat or mathclasses, Coq will no longer find it ambiguous to have A -> B + C as a type.

Alizter added 2 commits July 31, 2024 12:19
We fix the order in which we bind type_scope to Sortclass allowing
targets of function types to automatically be interpreted as types. This
allows us to remove %type annotations throughout the library.

Signed-off-by: Ali Caglayan <[email protected]>

<!-- ps-id: fad8ec7e-76b2-4ed7-93b6-b7ac64ca8201 -->
@Alizter Alizter requested a review from jdchristensen July 31, 2024 12:56
(** [type_scope] must be declared and bound early on so that later reserved notations register correctly. *)
Declare Scope type_scope.
Bind Scope type_scope with Sortclass.

(** To reserve this notation, we must first bootstrap, and preserve the underlying [forall] notation *)
Notation "'forall' x .. y , P" := (forall x , .. (forall y, P) ..) (at level 200, x binder, y binder, right associativity).
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Previously, this notation was declared before the bind which meant when -> was defined in Overture.v it registered the parser before the binding. By switching the order, we can get the correct binding behaviour.

Copy link
Collaborator

@jdchristensen jdchristensen left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice catch! I used my coqcreplace.py script and noticed that some %type annotations can also be removed in the Categories part of the library. I think they are independent of your changes, but I could push them to this PR if you think that's ok.

@Alizter
Copy link
Collaborator Author

Alizter commented Jul 31, 2024

@jdchristensen That's fine!

@Alizter Alizter merged commit 1d16652 into HoTT:master Aug 1, 2024
22 of 24 checks passed
@Alizter Alizter deleted the fix-scope-binding-for-type branch August 1, 2024 00:13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants