Language.Lean.Internal.Name

Internal declarations for Lean names together with typeclass instances for Name.

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.

Internal declarations

type NamePtr = Ptr Name

Haskell type for lean_name FFI parameters.

type OutNamePtr = Ptr NamePtr

Haskell type for lean_name* FFI parameters.

withName :: Name -> (Ptr Name -> IO a) -> IO a

Function c2hs uses to pass Name values to Lean

type ListName = List Name

Synonym for List Expr that can be used in c2hs bindings.

type ListNamePtr = Ptr ListName

A list of Lean universe levels.

Haskell type for lean_list_name FFI parameters.

type OutListNamePtr = Ptr ListNamePtr

Haskell type for lean_list_name* FFI parameters.

withListName :: ListName -> (Ptr ListName -> IO a) -> IO a

Function c2hs uses to pass ListName values to Lean