nom-0.1.0.1: Name-binding & alpha-equivalence

Safe HaskellNone
LanguageHaskell2010

Language.Nominal.Properties.NomSpec

Synopsis

Documentation

prop_x_neq_x :: Nom [Name Int] -> Property Source #

Nom creates local binding, which is unpacked separately by equality. Cf. UnifySpec to see how this can be addressed.

prop_split_scope :: Name String -> Bool Source #

Check restriction creates local scope. Should return False.

prop_fresh_neq :: Name () -> Bool Source #

n' # n if n' is chosen fresh, after n

prop_fresh_neq' :: Bool Source #

freshName () /= freshName () Lazy evaluation means distinct fresh names generated.

prop_fresh_neq'' :: Bool Source #

Same thing using let.

prop_fresh_eq :: Bool Source #

But if we unpack a single fresh name monadically, we can compare it for equality.

prop_freshFor1 :: Name () -> Name () -> Bool Source #

~ (n # (n,n'))

prop_transposeNomMaybe :: Nom (Maybe [Name Int]) -> Bool Source #

Nom Maybe -> Maybe Nom -> Nom Maybe = id

prop_transposeMaybeNom :: Maybe (Nom [Name Int]) -> Bool Source #

Maybe Nom -> Nom Maybe -> Nom Maybe = id

iprop_support_nom :: forall a. (Support a, Swappable a) => [Atom] -> a -> Bool Source #

deBruijnAcc :: KNom s a -> (KAtom s -> b) -> b -> (a, KAtom s -> b) Source #

deBruijn1 :: Functor f => KNom s (f (KAtom s)) -> f Int Source #

deBruijn2 :: Functor f => KNom s (KNom s (f (KAtom s))) -> f Int Source #

prop_transposeNomList :: Nom [Atom] -> Property Source #

Commute Nom and List

prop_transposeNomNom :: Nom (Nom [Atom]) -> Property Source #

Commute Nom and Nom (one way)