Zulip Chat Archive
Stream: new members
Topic: Documentation on keywords like `obtain`
Quinn Culver (Feb 13 2023 at 21:05):
Where can I find documentation on keywords like obtain?
Matthew Ballard (Feb 13 2023 at 21:15):
I find the mathlib documentation to be the best resource for this.
Notification Bot (Feb 13 2023 at 21:18):
Quinn Culver has marked this topic as resolved.
Junyan Xu (Feb 14 2023 at 09:19):
(I don't think it's a keyword)
Notification Bot (Feb 17 2023 at 05:03):
Quinn Culver has marked this topic as unresolved.
Quinn Culver (Feb 17 2023 at 05:04):
What about the keyword (if that's what it's called) this? As in instance [this : inhabited P] : inhabited (dual P) := this ? Is that somewhere in the docs? (I've looked.)
Quinn Culver (Feb 17 2023 at 05:05):
It's very difficult to search for a word like "this". :smile:
Kevin Buzzard (Feb 17 2023 at 05:22):
You could replace this with any other name and it would work
Quinn Culver (Feb 17 2023 at 16:50):
Why then is this (in the example I provided, which is from combinatorics.configuration) highlighted syntax in emacs lean mode? I thought that meant it's a keyword (or whatever it's called).
Eric Wieser (Feb 17 2023 at 17:17):
Highlighting in Lean3 is entirely heuristic based
Eric Wieser (Feb 17 2023 at 17:18):
The heuristic for highlighting this is that this is a more common name than most other names, because have := foo means have this := foo.
Last updated: Dec 20 2023 at 11:08 UTC