| Copyright | (c) Galois Inc, 2015 |
|---|---|
| License | Apache-2 |
| Maintainer | jhendrix@galois.com, lcasburn@galois.com |
| Safe Haskell | Trustworthy |
| Language | Haskell98 |
Language.Lean.Internal.Name
Contents
Description
Internal declarations for Lean names
together with typeclass instances for Name.
- data Name
- anonymousName :: Name
- nameAppend :: Name -> String -> Name
- nameAppendIndex :: Name -> Word32 -> Name
- data NameView
- nameView :: Name -> NameView
- nameToString :: Name -> String
- type NamePtr = Ptr Name
- type OutNamePtr = Ptr NamePtr
- withName :: Name -> (Ptr Name -> IO a) -> IO a
- type ListName = List Name
- type ListNamePtr = Ptr ListName
- type OutListNamePtr = Ptr ListNamePtr
- withListName :: ListName -> (Ptr ListName -> IO a) -> IO a
Documentation
A Lean name
Instances
| Eq Name Source | |
| Ord Name Source | |
| Show Name Source | |
| IsString Name Source | |
| Monoid Name Source | |
| IsLeanValue Name (Ptr Name) Source | |
| IsList (List Name) Source | |
| Eq (List Name) Source | |
| Show (List Name) Source | |
| IsListIso (List Name) Source | |
| IsLeanValue (List Name) (Ptr (List Name)) Source | |
| type Item ListName = Name Source | |
| data List Name = ListName (ForeignPtr (List Name)) Source | A list of names (constructor not actually exported) |
The root "anonymous" name
nameAppend :: Name -> String -> Name Source
Append a string to a name.
nameAppendIndex :: Name -> Word32 -> Name Source
Append a numeric index to a name.
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. |
nameToString :: Name -> String Source
Return a name as a string with subnames separated by periods.
Internal declarations
type OutNamePtr = Ptr NamePtr Source
Haskell type for lean_name* FFI parameters.
type ListNamePtr = Ptr ListName Source
A list of Lean universe levels.
Haskell type for lean_list_name FFI parameters.
type OutListNamePtr = Ptr ListNamePtr Source
Haskell type for lean_list_name* FFI parameters.