nom-0.1.0.2: Name-binding & alpha-equivalence

Safe HaskellNone
LanguageHaskell2010

Language.Nominal.Properties.Examples.SystemFSpec

Contents

Description

Please read the source code to view the tests.

Synopsis

Substitution

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

y[n-> var n] = y

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_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