Commit 84d1b7b4 authored by Nicola Botta's avatar Nicola Botta
Browse files

Initial.

parent f62ff2a4
module DoubleExtensions.Predicates
import Data.So
|||
public export
data EQ : Double -> Double -> Type where
MkEQ : {x : Double} -> {y : Double} -> So (x == y) -> EQ x y
|||
public export
data LT : Double -> Double -> Type where
MkLT : {x : Double} -> {y : Double} -> So (x < y) -> LT x y
|||
public export
data LTE : Double -> Double -> Type where
MkLTE : {x : Double} -> {y : Double} -> So (x <= y) -> LTE x y
|||
public export
NonNegative : (x : Double) -> Type
NonNegative x = 0.0 `LTE` x
|||
public export
Positive : (x : Double) -> Type
Positive x = 0.0 `LT` x
{-
---}
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