toki/numidr
1
0
Fork 0
Code Issues Pull requests Activity

Add constructors to interfaces

Browse source
This commit is contained in:
Kiana Sheibani 2022-09-19 12:42:07 -04:00
parent 33f64c69d9
commit 09901977c2
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Data/NumIdr/Interfaces.idr
View file

@ -22,6 +22,7 @@ Field a = (Eq a, Neg a, Fractional a)
||| * `0` is a minimum of `abslt`. ||| * `0` is a minimum of `abslt`.
public export public export
interface (Eq a, Neg a, Fractional a) => FieldCmp a where interface (Eq a, Neg a, Fractional a) => FieldCmp a where
constructor MkFieldCmp
||| Compare the absolute values of two inputs. ||| Compare the absolute values of two inputs.
abslt : a -> a -> Bool abslt : a -> a -> Bool
@ -46,6 +47,7 @@ infixr 10 ^
||| * If `x *. (y *. z)` is defined, then `(x *. y) *. z` is defined and equal. ||| * If `x *. (y *. z)` is defined, then `(x *. y) *. z` is defined and equal.
public export public export
interface Mult a b c | a,b where interface Mult a b c | a,b where
constructor MkMult
||| A generalized multiplication/application operator for matrices and ||| A generalized multiplication/application operator for matrices and
||| vector transformations. ||| vector transformations.
(*.) : a -> b -> c (*.) : a -> b -> c
@ -63,6 +65,7 @@ Mult' a = Mult a a a
||| * `identity *. x == x` ||| * `identity *. x == x`
public export public export
interface Mult' a => MultMonoid a where interface Mult' a => MultMonoid a where
constructor MkMultMonoid
||| Construct an identity matrix or transformation. ||| Construct an identity matrix or transformation.
||| |||
||| NOTE: Creating an identity element for an `n`-dimensional transformation ||| NOTE: Creating an identity element for an `n`-dimensional transformation
@ -76,6 +79,7 @@ interface Mult' a => MultMonoid a where
||| * `inverse x *. x == identity` ||| * `inverse x *. x == identity`
public export public export
interface MultMonoid a => MultGroup a where interface MultMonoid a => MultGroup a where
constructor MkMultGroup
||| Calculate the inverse of the matrix or transformation. ||| Calculate the inverse of the matrix or transformation.
||| WARNING: This function will not check if an inverse exists for the given ||| WARNING: This function will not check if an inverse exists for the given
||| input, and will happily return results containing NaN values. To avoid ||| input, and will happily return results containing NaN values. To avoid