Numeric.Type.Evidence

Construct type-level evidence at runtime

Documentation

data Evidence :: Constraint -> Type where

Bring an instance of certain class or constaint satisfaction evidence into scope.

Constructors

E :: a => Evidence a

withEvidence :: Evidence a -> (a => r) -> r

Pattern match agains evidence to get constraints info

sumEvs :: Evidence a -> Evidence b -> Evidence (a, b)

Combine evidence

(+!+) :: Evidence a -> Evidence b -> Evidence (a, b) infixl 4

Combine evidence

data Evidence' :: (k -> Constraint) -> k -> Type where

Same as Evidence, but allows to separate constraint function from the type it is applied to.

Constructors

E' :: c a => Evidence' c a

toEvidence :: Evidence' c a -> Evidence (c a)

toEvidence' :: Evidence (c a) -> Evidence' c a