The Unit Type
Table of Contents
1 Unit
module Lib.Data.Unit where
This file defines the unit type, i.e., the type that is inhabited by a unique element (often named star). As it is an inductive type, it also comes equiped with an induction principle.
1.1 Definition
data Unit : U = star
1.2 Induction principle
ind-Unit (P : Unit → U) (p : P star) : (x : Unit) → P x = split star → p