Hello, I am having hard time trying to understand what is the second line doing here:
Definition id (X:Type) (x:X) := x. Definition id' := id Set nat.
Specifically what is the keyword
Set is the type of nat
oh! no it makes sense, the syntax highlight threw me off!
Set felt like infex operation
grammatically it is a keyword
I think you mean: "lexically it is a keyword"?
(at least from last time I looked at the lexer)
It is probably colored oddly because of
Set Option value, in which
Set is a different thing.
Last updated: Oct 03 2023 at 04:02 UTC