Stream: Coq users

Topic: What is the keyword Set ?

view this post on Zulip walker (Aug 06 2022 at 09:43):

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

view this post on Zulip Gaëtan Gilbert (Aug 06 2022 at 09:45):

Set is the type of nat
https://coq.github.io/doc/master/refman/language/core/sorts.html

view this post on Zulip walker (Aug 06 2022 at 09:56):

oh! no it makes sense, the syntax highlight threw me off!

view this post on Zulip walker (Aug 06 2022 at 09:56):

Set felt like infex operation

view this post on Zulip Gaëtan Gilbert (Aug 06 2022 at 09:57):

grammatically it is a keyword

view this post on Zulip Karl Palmskog (Aug 06 2022 at 13:55):

I think you mean: "lexically it is a keyword"?

view this post on Zulip Karl Palmskog (Aug 06 2022 at 13:56):

(at least from last time I looked at the lexer)

view this post on Zulip Enrico Tassi (Aug 06 2022 at 14:02):

It is probably colored oddly because of Set Option value, in which Set is a different thing.

Last updated: Oct 13 2024 at 01:02 UTC