| Copyright | (c) Galois Inc, 2015 |
|---|---|
| License | Apache-2 |
| Maintainer | jhendrix@galois.com, lcasburn@galois.com |
| Safe Haskell | Trustworthy |
| Language | Haskell98 |
Language.Lean.Inductive
Description
Operations for creating inductive types and declarations.
- data InductiveType
- inductiveType :: Name -> Expr -> List Expr -> InductiveType
- inductiveTypeName :: InductiveType -> Name
- inductiveTypeType :: InductiveType -> Expr
- inductiveTypeConstructors :: InductiveType -> List Expr
- recursorName :: Name -> Name
- data InductiveDecl
- inductiveDecl :: List Name -> Word32 -> List InductiveType -> InductiveDecl
- inductiveDeclUnivParams :: InductiveDecl -> List Name
- inductiveDeclNumParams :: InductiveDecl -> Word32
- inductiveDeclTypes :: InductiveDecl -> List InductiveType
- addInductiveDecl :: InductiveDecl -> Env -> Env
- lookupInductiveDecl :: Env -> Name -> Maybe InductiveDecl
- lookupConstructorInductiveTypeName :: Env -> Name -> Maybe Name
- lookupRecursorInductiveTypeName :: Env -> Name -> Maybe Name
- lookupInductiveTypeNumIndices :: Env -> Name -> Maybe Word32
- lookupInductiveTypeNumMinorPremises :: Env -> Name -> Maybe Word32
- inductiveTypeHasDepElim :: Env -> Name -> Bool
Inductive type
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 |
Arguments
| :: Name | Name of the inductive type |
| -> Expr | Type of the inductive type |
| -> List Expr | Constructors (must be a list of local constants) |
| -> InductiveType |
Creates an inductive type
inductiveTypeName :: InductiveType -> Name Source
Get the name of a inductive type.
inductiveTypeType :: InductiveType -> Expr Source
Get the type of a inductive type.
inductiveTypeConstructors :: InductiveType -> List Expr Source
Get the list of constructors associated with the given inductive type.
recursorName :: Name -> Name Source
Get the name of the recursor (aka eliminator) associated with a inductive type with given name.
Inductive declarations
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
Arguments
| :: List Name | Universe parameters |
| -> Word32 | Number of parameters |
| -> List InductiveType | List of inductive types |
| -> InductiveDecl |
A inductive datatype declaration
The remaining inductive datatype arguments are treated as indices.
inductiveDeclUnivParams :: InductiveDecl -> List Name Source
Get the list of universe parameter names for the given inductive declaration.
inductiveDeclNumParams :: InductiveDecl -> Word32 Source
Get the number of parameters for the in the declaration.
inductiveDeclTypes :: InductiveDecl -> List InductiveType Source
Get the list of inductive types in the inductive declaration
Environment operations
addInductiveDecl :: InductiveDecl -> Env -> Env Source
Add the inductive declaration to the given environment.
lookupInductiveDecl :: Env -> Name -> Maybe InductiveDecl Source
Return the inductive declaration that introduced type with the given
name in the environment (or Nothing if no inductive type by that name exists).
lookupConstructorInductiveTypeName :: Env -> Name -> Maybe Name Source
If the given name is a constructor in the envionment, this returns the name of the associated inductive type.
If the name is not a constructor, then this returns Nothing.
lookupRecursorInductiveTypeName :: Env -> Name -> Maybe Name Source
If the given name is a recursor in the given environment, this returns the name of the associated inductive type.
If the name is not a recursor, then this returns Nothing.
lookupInductiveTypeNumIndices :: Env -> Name -> Maybe Word32 Source
Given the name of an inductive type in the environment, this returns the number of indices.
If the name is not an inductive type, then this returns Nothing.
lookupInductiveTypeNumMinorPremises :: Env -> Name -> Maybe Word32 Source
Given the name of an inductive type in the environment, this returns the number of minor premises for the recursor associated to this type.
If the name is not an inductive type, then this returns Nothing.
inductiveTypeHasDepElim :: Env -> Name -> Bool Source
Given a name, this returns true if the name is for a inductive type that supports dependent elimination.