builtin types

Stream: new members

[Nasos Evangelou-Oost]

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]

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

[Nasos Evangelou-Oost]

@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]

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

[Yury G. Kudryashov]

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

[Nasos Evangelou-Oost]

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

[Nasos Evangelou-Oost]

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

[Yury G. Kudryashov]

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]

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

[Nasos Evangelou-Oost]

@Yury G. Kudryashov thank you, ok