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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.SizedTypes.Tests

Contents

Synopsis

Label interpretation

type Relation a = a -> a -> Bool Source #

class AsWeightRelation b where Source #

Minimal complete definition

eval

Methods

eval :: b -> Relation Weight Source #

Generic properties

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

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

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

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

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

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

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

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

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

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

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

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

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

Properties of Dioid class.

prop_Dioid_Weight :: Weight -> Weight -> Weight -> Bool Source #

Weight instance.

prop_SemiLattice_Label :: Label -> Label -> Label -> Bool Source #

Label instance.

All tests

tests :: IO Bool Source #

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