| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Language.Nominal.Properties.Examples.SystemFSpec
Description
Please read the source code to view the tests.
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_untypeable :: Bool
- prop_all_typeable :: Trm -> Property
- prop_typeable_nf :: Trm -> Property
- prop_nf_typeable :: Trm -> Property
- prop_type_soundness :: Trm -> Property
- prop_id_type_unchanged :: Trm -> Property
- prop_app_id :: Trm -> Property
- prop_typeof_zero :: Bool
- prop_church_numerals0 :: NonNegative Int -> Bool
- prop_church_numerals1 :: NonNegative Int -> Bool
- prop_church_numerals_type :: NonNegative Int -> Bool
Substitution
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
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 Source #
n' # y => y[n->n'] = (n' n).y
Typing and reduction
prop_untypeable :: Bool Source #
(id id) has no type (it needs a type argument)
prop_all_typeable :: Trm -> Property Source #
Not all terms are typeable
prop_typeable_nf :: Trm -> Property Source #
prop_nf_typeable :: Trm -> Property Source #
prop_type_soundness :: Trm -> Property Source #
Type soundness If a term is typeable and normalisable then its normal form has the same type as it does.
prop_id_type_unchanged :: Trm -> Property Source #
typeof(id t) = typeof(t)
prop_app_id :: Trm -> Property Source #
If x : t then (id t x) --> x
Church numerals
prop_typeof_zero :: Bool Source #
0 : nat
prop_church_numerals0 :: NonNegative Int -> Bool Source #
i+1 /= 0
prop_church_numerals1 :: NonNegative Int -> Bool Source #
i+1 /= i
prop_church_numerals_type :: NonNegative Int -> Bool Source #
i : nat