module Stdlib.Data.Bool;

open import Stdlib.Data.Bool.Base public;

import Stdlib.Trait.Eq as Eq;
open Eq using {Eq};

import Stdlib.Trait.Ord as Ord;
open Ord using {Ord};

import Stdlib.Trait.Show as Show;
open Show using {Show};

module BoolTraits;
  
  Eq : Eq Bool;
  Eq :=
    Eq.mkEq
      λ {
        | true true := true
        | false false := true
        | _ _ := false
      };
  
  Ord : Ord Bool;
  Ord :=
    Ord.mkOrd
      λ {
        | false false := Ord.EQ
        | false true := Ord.LT
        | true false := Ord.GT
        | true true := Ord.EQ
      };
  
  Show : Show Bool;
  Show :=
    Show.mkShow
      λ {
        | true := "true"
        | false := "false"
      };

end;