--- The unit type.
module Stdlib.Data.Unit;
import Stdlib.Data.Unit.Base open public;
import Stdlib.Data.Bool.Base open;
import Stdlib.Trait.Eq open;
import Stdlib.Trait.Ord open;
import Stdlib.Trait.Show open;
import Stdlib.Trait.Foldable open;
instance
eqUnitI : Eq Unit := mkEq λ {unit unit := true};
instance
ordUnitI : Ord Unit := mkOrd λ {unit unit := EQ};
instance
showUnitI : Show Unit := mkShow λ {unit := "unit"};
instance
foldableUnitI : Foldable Unit Unit :=
mkFoldable@{
rfor {B : Type} (f : B -> Unit -> B) (ini : B) (_ : Unit) : B := f ini unit;
for {B : Type} (f : B -> Unit -> B) (ini : B) (_ : Unit) : B := f ini unit
};