nom-0.1.0.1: Name-binding & alpha-equivalence

Safe Haskell	None
Language	Haskell2010

Language.Nominal.Properties.AbsSpec

Synopsis

prop_fuse :: Name () -> [Name ()] -> [Name ()] -> Bool
prop_Abs_Conc :: Name () -> Abs () [Name ()] -> Property
prop_Abs_alpha :: Name () -> Name () -> [Name ()] -> Property
prop_Conc_Abs :: Name () -> [Name ()] -> Property
prop_Conc_Abs_swap :: Name () -> Name () -> [Name ()] -> Property
prop_fuse_unfuse_Abs :: Abs () ([Name ()], [Name ()]) -> Property
prop_unfuse_fuse_Abs :: (Abs () [Name ()], Abs () [Name ()]) -> Property
prop_unfuse_fuse_Abs' :: (Abs Int [Name Int], Abs Int [Name Int]) -> Property
prop_abs_to_nom :: Abs Int [Name Int] -> Bool
prop_nom_to_abs :: Nom (Name Int, [Name Int]) -> Bool

Documentation

prop_fuse :: Name () -> [Name ()] -> [Name ()] -> Bool Source #

fuse a.x a.x' = a.(x,x')

prop_Abs_Conc :: Name () -> Abs () [Name ()] -> Property Source #

n # x => [n](x n) = x@

prop_Abs_alpha :: Name () -> Name () -> [Name ()] -> Property Source #

n' # x => [n]x = [n'](n' n).x

prop_Conc_Abs :: Name () -> [Name ()] -> Property Source #

(n.x) @ n = x

prop_Conc_Abs_swap :: Name () -> Name () -> [Name ()] -> Property Source #

(n.x) @ n' = (n' n).x

prop_fuse_unfuse_Abs :: Abs () ([Name ()], [Name ()]) -> Property Source #

Atm.(X x Y) iso Atm.X x Atm.Y, left-to-right-to-left

prop_unfuse_fuse_Abs :: (Abs () [Name ()], Abs () [Name ()]) -> Property Source #

Atm.(X x Y) iso Atm.X x Atm.Y, right-to-left-to-right

prop_unfuse_fuse_Abs' :: (Abs Int [Name Int], Abs Int [Name Int]) -> Property Source #

Iso fails if atoms labelled, since one label lost Atm.X x Atm.Y -> Atm.(X x Y), and one label invented if list empty

prop_abs_to_nom :: Abs Int [Name Int] -> Bool Source #

Atm.X iso Nom (Atm x X)

prop_nom_to_abs :: Nom (Name Int, [Name Int]) -> Bool Source #

Nom (Atm x X) iso Atm.X.

Note: We have to use unifiability because of local scope.