Language.Lean.Name

Operations for working with Lean names.

Documentation

data Name

A Lean name

Instances

Eq Name

Ord Name

Show Name

IsString Name

Monoid Name

IsLeanValue Name (Ptr Name)

IsList (List Name)

Eq (List Name)

Show (List Name)

IsListIso (List Name)

IsLeanValue (List Name) (Ptr (List Name))

type Item ListName = Name

data List Name = ListName (ForeignPtr (List Name))

A list of names (constructor not actually exported)

anonymousName :: Name

The root "anonymous" name

nameAppend :: Name -> String -> Name

Append a string to a name.

nameAppendIndex :: Name -> Word32 -> Name

Append a numeric index to a name.

data NameView

A view of head of a lean name.

Constructors

AnonymousName

The anonymous name.

StringName Name String

A name with a string appended.

IndexName Name Word32

A name with a numeric value appended.

Instances

Show NameView

nameView :: Name -> NameView

View the head of a Lean name.

nameToString :: Name -> String

Return a name as a string with subnames separated by periods.