单元类型是只有一个元素的规范类型，名为 unit，并由空元组 () 表示。
它仅描述一个值，该值由不应用于任何参数的所述构造函数组成。
Unit 类似于源自 C 的语言中的 void：尽管 void 没有可命名的元素，但它表示从没有附加信息的函数返回控制流。
在函数式编程中，Unit 是“不返回任何内容”的返回类型。
从数学上讲，这由一个完全无信息的值表示，而不是像 Empty 这样表示无法访问的代码的空类型。
当使用 monads 进行编程时，Unit 特别有用。
对于任何类型 α，m α 表示具有副作用并返回 α 类型的值的操作。
m Unit 类型表示具有一些副作用但不返回值的操作。
单位类型有两种变体：
在幕后，Unit 实际上被定义为 PUnit.{1}。
如果可能，Unit 应优先于 PUnit，以避免不必要的 Universe 参数。
如果有疑问，请使用 Unit 直到出现 Universe 错误。
The canonical type with one element. This element is written ().
Unit has a number of uses:
It can be used to model control flow that returns from a function call without providing other information.
Monadic actions that return Unit have side effects without computing values.
In polymorphic types, it can be used to indicate that no data is to be stored in a particular field.
The only element of the unit type.
It can be written as an empty tuple: ().
The canonical universe-polymorphic type with just one element.
It should be used in contexts that require a type to be universe polymorphic, thus disallowing
Unit.
PUnit.unit.{u} : PUnit
The only element of the universe-polymorphic unit type.
Unit-like types 是具有单个构造函数的归纳类型，该构造函数不采用非证明参数。
PUnit 就是此类类型之一。
类似单元类型的所有元素都是 定义上等于所有其他元素。
Unit
CustomUnit 和 AlsoUnit 都是类似单元的类型，具有不带参数的单个构造函数。
任一类型的每对术语在定义上都是相等的。
inductive CustomUnit where
| customUnit
example (e1 e2 : CustomUnit) : e1 = e2 := rfl
structure AlsoUnit where
example (e1 e2 : AlsoUnit) : e1 = e2 := rfl
带参数的类型（例如 WithParam）如果具有不带参数的单个构造函数，那么它们也是类似单元的。
inductive WithParam (n : Nat) where
| mk
example (x y : WithParam 3) : x = y := rfl
具有非证明参数的构造函数不是类单元的，即使参数都是类单元类型。
inductive NotUnitLike where
| mk (u : Unit)
example (e1 e2 : NotUnitLike) : e1 = e2 := rfl
类单元类型的构造函数可以采用作为证明的参数。
inductive ProofUnitLike where
| mk : 2 = 2 → ProofUnitLike
example (e1 e2 : ProofUnitLike) : e1 = e2 := rfl