Agda-2.4.2.3: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.SizedTypes.Tests

Contents

Synopsis

Documentation

Label interpretation

type Relation a = a -> a -> Bool

Generic properties

propCommutative :: Eq b => (a -> a -> b) -> a -> a -> Bool

propAssociative :: Eq a => (a -> a -> a) -> a -> a -> a -> Bool

propIdempotent :: Eq a => (a -> a -> a) -> a -> Bool

propUnit :: Eq a => (a -> a -> a) -> a -> a -> Bool

propZero :: Eq a => (a -> a -> a) -> a -> a -> Bool

propDistL :: Eq b => (a -> b -> b) -> (b -> b -> b) -> a -> b -> b -> Bool

propDistR :: Eq a => (a -> b -> a) -> (a -> a -> a) -> a -> a -> b -> Bool

propDistributive :: Eq a => (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Bool

propSemiLattice :: Eq a => (a -> a -> a) -> a -> a -> a -> Bool

propBoundedSemiLattice :: Eq a => (a -> a -> a) -> a -> a -> a -> a -> Bool

propMonoid :: Eq a => (a -> a -> a) -> a -> a -> a -> a -> Bool

propDioid :: Eq a => (a -> a -> a) -> a -> (a -> a -> a) -> a -> a -> a -> a -> Bool

propDioid_Gen :: Dioid a => a -> a -> a -> Bool

Properties of Dioid class.

prop_Dioid_Weight :: Weight -> Weight -> Weight -> Bool

Weight instance.

prop_SemiLattice_Label :: Label -> Label -> Label -> Bool

Label instance.

All tests

tests :: IO Bool

Runs all tests starting with "prop_" in this file.