| Copyright | (c) Murdoch J. Gabbay 2020 |
|---|---|
| License | GPL-3 |
| Maintainer | murdoch.gabbay@gmail.com |
| Stability | experimental |
| Portability | POSIX |
| Safe Haskell | None |
| Language | Haskell2010 |
Language.Nominal.Properties.SubSpec
Description
Duplicating some tests from Language.Nominal.Properties.Examples.SystemFSpec, which has good inductive datatypes to substitute on.
Synopsis
- iprop_sub_id :: (KSub ntyp x y, Eq y) => (ntyp -> x) -> ntyp -> y -> Bool
- prop_sub_id_typevar' :: NTyp -> Typ -> Bool
- prop_sub_id_termvar :: NTrm -> Trm -> Bool
- prop_sub_id_typevar :: NTyp -> Trm -> Bool
- iprop_sub_fresh :: (Typeable s, Swappable y, Swappable n, KSub (KName s n) x y, Eq y, Show y) => KName s n -> x -> y -> Property
- prop_sub_fresh_typevar' :: NTyp -> Typ -> Typ -> Property
- prop_sub_fresh_typevar :: NTyp -> Typ -> Trm -> Property
- prop_sub_fresh_termvar :: NTrm -> Trm -> Trm -> Property
- iprop_sub_perm :: (Typeable s, Swappable y, Swappable n, KSub (KName s n) x y, Eq y, Show y) => (KName s n -> x) -> KName s n -> KName s n -> y -> Property
- prop_sub_perm_typevar' :: NTyp -> NTyp -> Typ -> Property
- prop_sub_perm_typevar'' :: NTyp -> NTyp -> Trm -> Property
- prop_sub_perm_termvar :: NTrm -> NTrm -> Trm -> Property
- prop_sub_singleton1 :: Name Int -> Name Int -> Bool
- prop_sub_singleton2 :: Name Int -> Name Int -> Bool
- prop_sub_abs_1 :: Name () -> Name () -> Name () -> [Name ()] -> Property
- prop_sub_abs_1' :: Name () -> Name () -> Name () -> [Name ()] -> Property
- prop_sub_abs_3 :: Name () -> Name () -> [Name ()] -> Bool
Documentation
iprop_sub_fresh :: (Typeable s, Swappable y, Swappable n, KSub (KName s n) x y, Eq y, Show y) => KName s n -> x -> y -> Property Source #
n # y => y[n->x] = y