nom-0.1.0.1: Name-binding & alpha-equivalence

Safe Haskell	None
Language	Haskell2010

Language.Nominal.Properties.UnifySpec

Synopsis

prop_l_l' :: [Name Int] -> [Name Int] -> Property
prop_res_res :: [Atom] -> [Atom] -> [Atom] -> Bool
prop_res_unres :: Nom [Name Int] -> Bool
prop_unify_ren :: [Name ()] -> [Name ()] -> Property
prop_renId :: Atom -> Bool
iprop_fresh_ren :: (UnifyPerm a, Support a, Swappable a, Eq a) => a -> Bool
prop_fresh_ren_atmlistlist :: [[Atom]] -> Bool
prop_fresh_ren_absatmlist :: Abs () [Atom] -> Bool

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

prop_fresh_ren_atmlistlist :: [[Atom]] -> Bool Source #

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