Commit 1990147f authored by Nicola Botta's avatar Nicola Botta
Browse files

Initial.

parent 375cf7c6
module NonNegDouble.BasicOperations
import DoubleExtensions.Predicates
import NonNegDouble.NonNegDouble
import Sigma.Sigma
import Sigma.Operations
|||
public export
mkNonNegDouble : (x : Double) -> {auto prf : 0.0 `LTE` x} -> NonNegDouble
mkNonNegDouble x {prf} = MkSigma x prf
|||
public export
cast : (x : Double) -> {auto prf : 0.0 `LTE` x} -> NonNegDouble
cast x {prf} = mkNonNegDouble x {prf}
|||
toDouble : NonNegDouble -> Double
toDouble = outl
|||
fromDouble : (x : Double) -> NonNegative x -> NonNegDouble
fromDouble = MkSigma
{-
---}
module NonNegDouble.Operations
-- import Data.So
import NonNegDouble.NonNegDouble
import Sigma.Sigma
-- import Double.Predicates
-- import Double.Postulates
-- import Double.Properties
-- import NonNegDouble.NonNegDouble
-- import NonNegDouble.Predicates
-- import NonNegDouble.Constants
-- import NonNegDouble.BasicOperations
-- import Pairs.Operations
||| Addition of positive double precision floating point numbers
public export
plus : NonNegDouble -> NonNegDouble -> NonNegDouble
plus (MkSigma x nnx) (MkSigma y nny) = MkSigma (x + y) (plusPreservesNonNegativity nnx nny)
{-
> ||| Subtraction of positive double precision floating point numbers
> minus : (x : NonNegDouble) -> (y : NonNegDouble) -> {auto prf : y `LTE` x} -> NonNegDouble
> minus (Element x nnx) (Element y nny) {prf} = Element (x - y) (minusPreservesNonNegativity nnx nny prf)
> (-) : (x : NonNegDouble) -> (y : NonNegDouble) -> {auto prf : y `LTE` x} -> NonNegDouble
> (-) = minus
> ||| Multiplication of positive double precision floating point numbers
> mult : NonNegDouble -> NonNegDouble -> NonNegDouble
> mult (Element x nnx) (Element y nny) = Element (x * y) (multPreservesNonNegativity nnx nny)
> ||| Division of positive double precision floating point numbers
> div : NonNegDouble -> NonNegDouble -> NonNegDouble
> div (Element x nnx) (Element y nny) = Element (x / y) (divPreservesNonNegativity nnx nny)
> |||
> fromNat : (n : Nat) -> NonNegDouble
> fromNat Z = zero
> fromNat (S m) = one `plus` (fromNat m)
---}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment