module Stdlib.Data.Maybe;

import Stdlib.Data.Maybe.Base open public;

import Stdlib.Trait.Eq open;
import Stdlib.Trait.Ord open;
import Stdlib.Trait.Show open;

import Stdlib.Data.Bool.Base open;
import Stdlib.Data.String.Base open;

instance
eqMaybeI {A} {{Eq A}} : Eq (Maybe A) :=
  mkEq
    λ {
      | nothing nothing := true
      | (just a1) (just a2) := Eq.eq a1 a2
      | _ _ := false
    };

instance
showMaybeI {A} {{Show A}} : Show (Maybe A) :=
  mkShow
    λ {
      | nothing := "nothing"
      | (just a) := "just " ++str Show.show a
    };

instance
ordMaybeI {A} {{Ord A}} : Ord (Maybe A) :=
  mkOrd
    λ {
      | nothing nothing := EQ
      | (just a1) (just a2) := Ord.cmp a1 a2
      | nothing (just _) := LT
      | (just _) nothing := GT
    };