--- 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"};

{-# specialize: true, inline: case #-}
instance
foldableUnitI : Foldable Unit Unit :=
  mkFoldable@{
    {-# inline: true #-}
    rfor {B : Type} (f : B -> Unit -> B) (ini : B) (_ : Unit) : B := f ini unit;
    {-# inline: true #-}
    for {B : Type} (f : B -> Unit -> B) (ini : B) (_ : Unit) : B := f ini unit
  };