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.

Sign up for GitHub

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

Jump to bottom

Implicit Types declaration doesn't work for notations involving binders #9764

Open
pi8027 opened this issue Mar 13, 2019 · 2 comments
Open

Implicit Types declaration doesn't work for notations involving binders #9764

pi8027 opened this issue Mar 13, 2019 · 2 comments
Labels
kind: bug An error, flaw, fault or unintended behaviour. part: notations The notation system.

Comments

@pi8027
Copy link
Contributor

pi8027 commented Mar 13, 2019 •
edited

Description of the problem

Notation "[ 'fun' x => F ]" := (fun x => F)
  (at level 0, x ident, only parsing).
               (* or `x pattern` *)

Implicit Types (n : nat).

Fail Definition nat_id := [fun n => n].
(*
The command has indeed failed with message:
         Cannot infer the type of n.
*)

Definition nat_id := (fun n => n).
(*
nat_id is defined
*)

Coq Version

8.9.0 and master
@pi8027 pi8027 mentioned this issue Mar 13, 2019
Merged
@pi8027 pi8027 changed the title Implicit Types declaration doesn't work for binders in notations Implicit Types declaration doesn't work for notations involving binders Mar 14, 2019
@Alizter Alizter added kind: bug An error, flaw, fault or unintended behaviour. needs: triage The validity of this issue needs to be checked, or the issue itself updated. part: notations The notation system. labels Nov 26, 2021
@SkySkimmer
Copy link
Contributor

It fails with x ident but not with x binder.

@SkySkimmer SkySkimmer removed the needs: triage The validity of this issue needs to be checked, or the issue itself updated. label May 6, 2024
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue May 6, 2024
@SkySkimmer
Handle Implicit Type for identonly binders in notations
e7bb878 
Fix coq#9764
@SkySkimmer SkySkimmer mentioned this issue May 6, 2024
Closed
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue May 7, 2024
@SkySkimmer
Handle Implicit Type for identonly binders in notations
aa4dcaa 
Fix coq#9764
@pi8027
Copy link
Contributor Author

pi8027 commented May 13, 2024 •
edited

It fails with x ident but not with x binder.

Thanks. After looking at the reference manual, it seems more appropriate to use x name, but the above example also fails with x name. I didn't check whether #19003 fixes it or not.

By the way, the reference manual does not seem to clearly explain the difference between name and ident. It should be improved (perhaps with the documentation of binder and pattern). Meanwhile, I'm taking a look at #11841.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: bug An error, flaw, fault or unintended behaviour. part: notations The notation system.
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Handle Implicit Type for identonly binders in notations SkySkimmer/coq
3 participants
@pi8027 @SkySkimmer @Alizter