Zulip Chat Archive

Stream: new members

Topic: builtin types


Nasos Evangelou-Oost (Feb 02 2021 at 03:54):

Hi, i've just installed lean 4 and read the docs. i wondered if there was a built-in Set type, and also is there a built-in Void type? thanks

Yury G. Kudryashov (Feb 02 2021 at 04:04):

Do you mean "built-in" = "in prelude"?

Nasos Evangelou-Oost (Feb 02 2021 at 04:09):

@Yury G. Kudryashov i'm not sure what i mean... i know nothing about lean beyond what is in the docs. there is a section called "Builtin Types" (https://leanprover.github.io/lean4/doc/builtintypes.html), but this list is apparently not exhaustive since Unit appears to be a builtin type but is not listed. I did not find a Void type or a Set type though.

Nasos Evangelou-Oost (Feb 02 2021 at 04:10):

If not in the prelude, is there something i need to import?

Yury G. Kudryashov (Feb 02 2021 at 04:11):

https://github.com/leanprover/lean4/blob/master/src/Init/Prelude.lean#L60 defines False and Empty

Nasos Evangelou-Oost (Feb 02 2021 at 04:13):

@Yury G. Kudryashov thank you. What about for a Set type?

Nasos Evangelou-Oost (Feb 02 2021 at 04:16):

I mean a homogeneous, finite Set, aka a List but unordered

Yury G. Kudryashov (Feb 02 2021 at 04:19):

In lean3, docs#set is an alias for α → Prop, and a finite set is docs#finset. I don't think that Lean 4 prelude has finsets.

Yury G. Kudryashov (Feb 02 2021 at 04:20):

BTW, we have a stream for questions about Lean 4: #lean4

Nasos Evangelou-Oost (Feb 02 2021 at 04:20):

@Yury G. Kudryashov thank you, ok


Last updated: Dec 20 2023 at 11:08 UTC