Agda: Generalized variables should be highlighted as bound variables

Created on 5 Jun 2018 · 3Comments · Source: agda/agda

Currently they are highlighted as defined names.

generalize highlighting not-in-changelog bug enhancement

Source

UlfNorell

Most helpful comment

Maybe we could have a separate highlighting for generalized variables? This would be useful for e.g. the LaTeX mode where you may want to make clear syntactically which variables are generalized.

jespercockx on 5 Jun 2018

👍3

All 3 comments

Maybe we could have a separate highlighting for generalized variables? This would be useful for e.g. the LaTeX mode where you may want to make clear syntactically which variables are generalized.

jespercockx on 5 Jun 2018

👍3

I vote for separate.

Currently the highlighting is broken, as some of us discovered today. Consider the following code:

variable
  A : Set

f : A → A
f x = x

When I load this code in Emacs, with non-interactive highlighting, then all occurrences of A get treated as bound variables and postulates. This is a bug.

If I instead use interactive highlighting, then the first occurrence of A gets treated as a bound variable and a postulate, and the other occurrences as bound variables. This is also incorrect.

In either case, if the file is later reloaded, then every occurrence gets treated as a bound variable.