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

feat(syntaxes/lean): add highlighting support for binders #268

Merged
merged 2 commits into from May 25, 2021

Conversation

eric-wieser
Copy link
Contributor

@eric-wieser eric-wieser commented May 25, 2021

The following code:

namespace pi
universes u v w
variable {I : Type u}     -- The indexing type
variable {f : I → Type v} -- The family of types already equipped with instances
variables (x y : Π i, f i) (i : I)

#check λ x /-"foo"-/ y, x + y

instance module (α) [semiring α] {m : ∀ i, add_comm_monoid $ f i}
  [∀ i, module α $ f i] :
  @module α (Π i : I, f i) r (@pi.add_comm_monoid I f m) :=
{ add_smul := λ c f g, funext $ λ i, add_smul _ _ _,
  zero_smul := λ f, funext $ λ i, zero_smul α _,
  ..pi.distrib_mul_action _ }

which previously was highlighted as

image

Is now highlighted as:

image

What's new is that vscode now recognizes names within binders.

@@ -2,6 +2,7 @@
"name": "Lean",
"scopeName": "source.lean",
"fileTypes": ["lean"],
"comments": "Lean is full of types; `x < 0` is a type, as are many more complex statements. Highlighting these is probably unhelpful, so we use `meta.type.lean` instead of `entity.name.type.lean` to prevent the type color being used everywhere.",
Copy link
Contributor Author

Choose a reason for hiding this comment

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

Otherwise the result is:

image

Which is a little too green to be useful.

@gebner
Copy link
Member

gebner commented May 25, 2021

This looks wonderful! Thanks!

@gebner gebner merged commit a795855 into leanprover:master May 25, 2021
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.

None yet

2 participants