| Copyright | (c) Galois Inc, 2015 |
|---|---|
| License | Apache-2 |
| Maintainer | jhendrix@galois.com, lcasburn@galois.com |
| Safe Haskell | Trustworthy |
| Language | Haskell98 |
Language.Lean.Internal.Inductive
Description
Internal declarations for inductive types and declarations.
- data InductiveType
- type InductiveTypePtr = Ptr InductiveType
- type OutInductiveTypePtr = Ptr InductiveTypePtr
- withInductiveType :: InductiveType -> (Ptr InductiveType -> IO a) -> IO a
- type ListInductiveType = List InductiveType
- type ListInductiveTypePtr = Ptr ListInductiveType
- type OutListInductiveTypePtr = Ptr ListInductiveTypePtr
- withListInductiveType :: List InductiveType -> (Ptr (List InductiveType) -> IO a) -> IO a
- data InductiveDecl
- type InductiveDeclPtr = Ptr InductiveDecl
- type OutInductiveDeclPtr = Ptr InductiveDeclPtr
- withInductiveDecl :: InductiveDecl -> (Ptr InductiveDecl -> IO a) -> IO a
Documentation
data InductiveType Source
An inductive type
Instances
| IsLeanValue InductiveType (Ptr InductiveType) Source | |
| IsList (List InductiveType) Source | |
| Eq (List InductiveType) Source | |
| IsListIso (List InductiveType) Source | |
| IsLeanValue (List InductiveType) (Ptr (List InductiveType)) Source | |
| data List InductiveType = ListInductiveType (ForeignPtr (List InductiveType)) Source | A list of inductive types (constructor not actually exported) |
| type Item (List InductiveType) = InductiveType Source |
type InductiveTypePtr = Ptr InductiveType Source
Haskell type for lean_inductive_type FFI parameters.
type OutInductiveTypePtr = Ptr InductiveTypePtr Source
Haskell type for lean_inductive_type* FFI parameters.
withInductiveType :: InductiveType -> (Ptr InductiveType -> IO a) -> IO a Source
Access raw lean_inductive_type within IO action.
type ListInductiveType = List InductiveType Source
Synonym for List InductiveType
type ListInductiveTypePtr = Ptr ListInductiveType Source
Haskell type for lean_list_inductive_type FFI parameters.
type OutListInductiveTypePtr = Ptr ListInductiveTypePtr Source
Haskell type for lean_list_inductive_type* FFI parameters.
withListInductiveType :: List InductiveType -> (Ptr (List InductiveType) -> IO a) -> IO a Source
Access raw lean_list_inductive_type within IO action.
data InductiveDecl Source
An inductive declaration
A single inductive declaration may define one or more Lean inductive types. The inductive types must have the same parameters.
Instances
type InductiveDeclPtr = Ptr InductiveDecl Source
Haskell type for lean_inductive_decl FFI parameters.
type OutInductiveDeclPtr = Ptr InductiveDeclPtr Source
Haskell type for lean_inductive_decl* FFI parameters.
withInductiveDecl :: InductiveDecl -> (Ptr InductiveDecl -> IO a) -> IO a Source
Access raw lean_inductive_decl within IO action.