Commit 781afc3c authored by Nicola Botta's avatar Nicola Botta
Browse files


parent 84d1b7b4
module NonNegDouble.NonNegDouble
import DoubleExtensions.Predicates
import Sigma.Sigma
||| Non negative double precision floating point numbers as sigma types
public export
NonNegDouble : Type
NonNegDouble = Sigma Double (\ x => 0.0 `LTE` 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