Thm* ![]()
Unit
Thm* a:Unit. a =
There happen already to be other single element types. Propositions expressing equality and membership propositions are often represented as types that have a member iff they are true, and when they are true, the sole member is
See
Def Unit == 0 ![]()
Def == *
Thm* a:(0
![]()
). a = *
About:
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |