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.Integral open public;
import Stdlib.Trait.Numeric open public;
instance
eqFieldI : Eq Field := mkEq (Field.==);
instance
showFieldI : Show Field :=
mkShow@{
show (f : Field) : String := Show.show (Field.toNat f)
};
instance
naturalFieldI : Natural Field :=
mkNatural@{
+ := (Field.+);
* := (Field.*);
fromNat := Field.fromNat
};
instance
integralFieldI : Integral Field :=
mkIntegral@{
naturalI := naturalFieldI;
- := (Field.-);
fromInt := Field.fromInt
};
instance
numericFieldI : Numeric Field :=
mkNumeric@{
integralI := integralFieldI;
/ := (Field./)
};
Last modified on 2024-04-19 16:39 UTC