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

Anonymous implicit generalization is not recognized #296

Open
Tuplanolla opened this issue May 24, 2022 · 3 comments
Open

Anonymous implicit generalization is not recognized #296

Tuplanolla opened this issue May 24, 2022 · 3 comments

Comments

@Tuplanolla
Copy link

Tuplanolla commented May 24, 2022

Versions

Coq 8.15.0

Coqtail 1.6.2

Vim 8.2

Equations 1.3

Python 3.7.4

Description

Unnamed parameters introduced by implicit generalization are highlighted
as if they were named parameters without explicit type signatures.
Looking at Coq's own theories/Classes/EquivDec.v
demonstrates both sides of this issue.

Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
  match x with
    | left H => @right _ _ H
    | right H => @left _ _ H
  end.
Definition equiv_decb `{EqDec A} (x y : A) : bool :=
  if x == y then true else false.

The implicit parameters of swap_sumbool and equiv_decb
are A B : Type and H : EqDec A respectively.

@whonore
Copy link
Owner

whonore commented May 24, 2022

Are you saying you'd expect the A in EqDec A to be highlighted differently from EqDec and A, B in swap_sumbool? Coqtail's highlighting currently doesn't make much (any?) effort to distinguish between parameters and arguments and just calls them all Identifiers, but I'd welcome any PRs improving the situation. Possibly related: #165.

@Tuplanolla
Copy link
Author

I would expect A, B and H to be Identifiers and
Type and EqDec A to be plain terms,
just like x and y are Identifiers and A is a plain term.

@whonore
Copy link
Owner

whonore commented May 24, 2022

Oh ok, I think I understand. So if there's no explicit :, everything in {} should be treated as if it comes before a : (Identifier), and within <backtick>{} everything should be treated as coming after a : (coqBinderTypeCurly, which has no special highlighting currently).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants