nom-0.1.0.2: Name-binding & alpha-equivalence

Safe HaskellNone
LanguageHaskell2010

Language.Nominal.Properties.UnifySpec

Synopsis

Documentation

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

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 Source #

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

prop_res_unres :: Nom [Name Int] -> Bool Source #

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

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

Unifiers correctly calculated

prop_renId :: Atom -> Bool Source #

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 Source #

Permutations and freshening renamings coincide