nom-0.1.0.1: Name-binding & alpha-equivalence

Safe Haskell	None
Language	Haskell2010

Language.Nominal.Properties.NameSpec

Synopsis

prop_namelabel :: Name String -> String -> Bool
prop_twonames :: Name () -> Name () -> Property
prop_singleswap :: Name String -> Name String -> [Name String] -> Property
prop_freshswap :: Name String -> Name String -> (Name String, Name String, Name String) -> Property
prop_doubleswap :: Name String -> Name String -> [Name String] -> Bool
prop_doubleswap_fresh' :: Name String -> Name String -> Name String -> Name String -> Property
prop_doubleswap_fresh :: Name String -> Name String -> Name String -> [Name String] -> Property
prop_swap_symm :: Name String -> Name String -> [Name String] -> Bool

Documentation

>>> :set -XScopedTypeVariables
>>> import Test.QuickCheck
>>> import Language.Nominal.Properties.SpecUtilities

prop_namelabel :: Name String -> String -> Bool Source #

withLabel does indeed overwrite the label.

\(n :: Name String) t -> nameLabel (n `withLabel` t) == t

prop_twonames :: Name () -> Name () -> Property Source #

Not all names are equal (even with trivial labels)

prop_singleswap :: Name String -> Name String -> [Name String] -> Property Source #

(n' n).x = x (we expect this to fail)

prop_freshswap :: Name String -> Name String -> (Name String, Name String, Name String) -> Property Source #

n',n#x => (n' n).x = x. Test on x a tuple.

prop_doubleswap :: Name String -> Name String -> [Name String] -> Bool Source #

(n' n).(n' n).x = x

prop_doubleswap_fresh' :: Name String -> Name String -> Name String -> Name String -> Property Source #

n'',n'#x => (n'' n').(n' n).m = (n'' n).m

prop_doubleswap_fresh :: Name String -> Name String -> Name String -> [Name String] -> Property Source #

n'#x => (n'' n').(n' n).x = (n'' n).x

prop_swap_symm :: Name String -> Name String -> [Name String] -> Bool Source #

(n' n).x = (n n').x