module Stdlib.Data.Field;

import Stdlib.Data.Field.Base open using {Field} public;
import Stdlib.Data.Field.Base as Field;
import Stdlib.Data.String.Base open;
import Stdlib.Data.Nat;

import Stdlib.Trait.Eq open public;
import Stdlib.Trait.Show open public;
import Stdlib.Trait.Natural open public;
import Stdlib.Trait.FromNatural open;
import Stdlib.Trait.Integral open public;
import Stdlib.Trait.Numeric open public;

{-# specialize: true, inline: case #-}
instance
eqFieldI : Eq Field := mkEq (Field.==);

instance
showFieldI : Show Field :=
  mkShow@{
    show (f : Field) : String := Show.show (Field.toNat f);
  };

{-# specialize: true, inline: case #-}
instance
fromNaturalFieldI : FromNatural Field :=
  mkFromNatural@{
    fromNat := Field.fromNat;
  };

{-# specialize: true, inline: case #-}
instance
naturalFieldI : Natural Field :=
  mkNatural@{
    + := (Field.+);
    * := (Field.*);
  };

{-# specialize: true, inline: case #-}
instance
integralFieldI : Integral Field :=
  mkIntegral@{
    naturalI := naturalFieldI;
    - := (Field.-);
    fromInt := Field.fromInt;
  };

{-# specialize: true, inline: case #-}
instance
numericFieldI : Numeric Field :=
  mkNumeric@{
    integralI := integralFieldI;
    / := (Field./);
  };