| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Language.Nominal.Properties.NomSpec
Synopsis
- prop_x_neq_x :: Nom [Name Int] -> Property
- prop_split_scope :: Name String -> Bool
- prop_fresh_neq :: Name () -> Bool
- prop_fresh_neq' :: Bool
- prop_fresh_neq'' :: Bool
- prop_fresh_eq :: Bool
- prop_freshFor1 :: Name () -> Name () -> Bool
- prop_freshFor2 :: Name () -> Bool
- prop_transposeNomMaybe :: Nom (Maybe [Name Int]) -> Bool
- prop_transposeMaybeNom :: Maybe (Nom [Name Int]) -> Bool
- prop_new' :: [Name Int] -> Bool
- prop_not_new' :: [Name Int] -> Name Int -> Property
- prop_new :: Int -> Int -> [Name Int] -> Bool
- prop_freshFor_notElem :: Name () -> [Name ()] -> Bool
- iprop_support_nom :: forall a. (Support a, Swappable a) => [Atom] -> a -> Bool
- prop_support_nom_atmlist :: [Atom] -> [Atom] -> Bool
- prop_support_nom_nomatmlist :: [Atom] -> Nom [Atom] -> Bool
- iprop_freshen_apart :: (Support a, Swappable a) => a -> Bool
- prop_freshen_apart_atmlist :: [Atom] -> Bool
- prop_freshen_apart_nom_atmlist :: Nom [Atom] -> Bool
- prop_freshen_apart_disjoint :: [Atom] -> Bool
- prop_isTrivial_equal :: Nom [Atom] -> Bool
- prop_isTrivial_sane :: Nom [Atom] -> Property
- prop_isTrivial_sane' :: Nom [Atom] -> Property
- deBruijnAcc :: KNom s a -> (KAtom s -> b) -> b -> (a, KAtom s -> b)
- deBruijn1 :: Functor f => KNom s (f (KAtom s)) -> f Int
- deBruijn2 :: Functor f => KNom s (KNom s (f (KAtom s))) -> f Int
- prop_transposeNomList :: Nom [Atom] -> Property
- prop_transposeNomNom :: Nom (Nom [Atom]) -> Property
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_freshFor2 :: Name () -> Bool Source #
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
prop_freshen_apart_atmlist :: [Atom] -> Bool Source #
prop_freshen_apart_disjoint :: [Atom] -> Bool Source #