Unbound.Nominal.Name

XXX write me

Documentation

data Name a

Names are things that get bound. This type is intentionally abstract; to create a Name you can use string2Name or integer2Name. The type parameter is a tag, or sort, which tells us what sorts of things this name may stand for. The sort must be an instance of the Rep type class.

Constructors

Nm (R a) (String, Integer)

Instances

(Rep a[a1Ev], Sat (ctx[a5QL] (R a[a1Ev])), Sat (ctx[a5QL] (String, Integer))) => Rep1 ctx[a5QL] (Name a[a1Ev])

Rep a => Subst b (Name a)

Eq (Name a)

Ord (Name a)

Show (Name a)

Rep a[a1Ev] => Rep (Name a[a1Ev])

Rep a => Alpha (Name a)

data AnyName

A name with a hidden (existentially quantified) sort.

Constructors

forall a . Rep a => AnyName (Name a)

Instances

Eq AnyName

Ord AnyName

Show AnyName

Rep AnyName

Alpha AnyName

Rep1 ctx[a2w3] AnyName

Subst c AnyName

rAnyName1 :: forall ctx[a2w3]. R1 ctx[a2w3] AnyName

rAnyName :: R AnyName

name2 :: Rep a => Name a

name3 :: Rep a => Name a

name4 :: Rep a => Name a

name5 :: Rep a => Name a

name6 :: Rep a => Name a

name7 :: Rep a => Name a

name8 :: Rep a => Name a

name9 :: Rep a => Name a

name10 :: Rep a => Name a

name11 :: Rep a => Name a

name1 :: Rep a => Name a

name2Integer :: Name a -> Integer

Get the integer index of a Name.

name2String :: Name a -> String

Get the string part of a Name.

anyName2Integer :: AnyName -> Integer

Get the integer index of an AnyName.

anyName2String :: AnyName -> String

Get the string part of an AnyName.

toSortedName :: Rep a => AnyName -> Maybe (Name a)

integer2Name :: Rep a => Integer -> Name a

Create a Name from an Integer.

string2Name :: Rep a => String -> Name a

Create a Name from a String.

s2n :: Rep a => String -> Name a

Convenient synonym for string2Name.

makeName :: Rep a => String -> Integer -> Name a

Create a Name from a String and an Integer index.

getR :: Name a -> R a

Determine the sort of a Name.

translate :: Rep b => Name a -> Name b

Change the sort of a name