Language.Nominal.Properties.UnifySpec

Documentation

prop_l_l' :: [Name Int] -> [Name Int] -> Property

l is unifiable with l' for any l and l' Should fail, taking e.g. l = [] and l' nonempty

prop_res_res :: [Atom] -> [Atom] -> [Atom] -> Bool

ns > ns' > x is unifiable with ns' > ns > x

prop_res_unres :: Nom [Name Int] -> Bool

x' -> ns x -> res ns x unifies with x'

prop_unify_ren :: [Name ()] -> [Name ()] -> Property

Unifiers correctly calculated

prop_renId :: Atom -> Bool

idRen equals idRen extended with an identity mapping (since equality is on nub).

iprop_fresh_ren :: (UnifyPerm a, Support a, Swappable a, Eq a) => a -> Bool

Permutations and freshening renamings coincide

prop_fresh_ren_atmlistlist :: [[Atom]] -> Bool

prop_fresh_ren_absatmlist :: Abs () [Atom] -> Bool