Agda-2.4.0.2: 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 a => (t -> t -> a) -> t -> t -> 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 a => (t -> a -> a) -> (a -> a -> a) -> t -> a -> a -> Bool

propDistR :: Eq a => (a -> t -> a) -> (a -> a -> a) -> a -> a -> t -> 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.