module Stdlib.Data.Bool;

import Stdlib.Data.Bool.Base open public;
import Stdlib.Trait.Eq open;
import Stdlib.Trait.Ord open;
import Stdlib.Trait.Show open;

instance
boolEqI : Eq Bool :=
  mkEq
    λ {
      | true true := true
      | false false := true
      | _ _ := false
    };

instance
boolOrdI : Ord Bool :=
  mkOrd
    λ {
      | false false := EQ
      | false true := LT
      | true false := GT
      | true true := EQ
    };

instance
showBoolI : Show Bool :=
  mkShow
    λ {
      | true := "true"
      | false := "false"
    };
Last modified on 2024-04-29 3:18 UTC