Language.Nominal.Properties.Examples.SystemFSpec

Please read the source code to view the tests.

Substitution

iprop_sub_id :: (KSub ntyp x y, Eq y) => (ntyp -> x) -> ntyp -> y -> Bool

y[n-> var n] = y

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

n # y => y[n->x] = y

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

n' # y => y[n->n'] = (n' n).y

prop_sub_perm_typevar' :: NTyp -> NTyp -> Typ -> Property

prop_sub_perm_typevar'' :: NTyp -> NTyp -> Trm -> Property

prop_sub_perm_termvar :: NTrm -> NTrm -> Trm -> Property

Typing and reduction

prop_untypeable :: Bool

(id id) has no type (it needs a type argument)

prop_all_typeable :: Trm -> Property

Not all terms are typeable

prop_typeable_nf :: Trm -> Property

prop_nf_typeable :: Trm -> Property

prop_type_soundness :: Trm -> Property

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

typeof(id t) = typeof(t)

prop_app_id :: Trm -> Property

If x : t then (id t x) --> x

Church numerals

prop_typeof_zero :: Bool

0 : nat

prop_church_numerals0 :: NonNegative Int -> Bool

i+1 /= 0

prop_church_numerals1 :: NonNegative Int -> Bool

i+1 /= i

prop_church_numerals_type :: NonNegative Int -> Bool

i : nat