| Copyright | (c) Galois Inc, 2015 |
|---|---|
| License | Apache-2 |
| Maintainer | jhendrix@galois.com, lcasburn@galois.com |
| Safe Haskell | Trustworthy |
| Language | Haskell98 |
Language.Lean.Decl
Description
Operations for working with Lean declarations.
- newtype Env = Env (ForeignPtr Env)
- data Decl
- axiom :: Name -> List Name -> Expr -> Decl
- constant :: Name -> List Name -> Expr -> Decl
- definition :: Name -> List Name -> Expr -> Expr -> Word32 -> Bool -> Decl
- definitionWith :: Env -> Name -> List Name -> Expr -> Expr -> Bool -> Decl
- theorem :: Name -> List Name -> Expr -> Expr -> Word32 -> Decl
- theoremWith :: Env -> Name -> List Name -> Expr -> Expr -> Decl
- declName :: Decl -> Name
- declUnivParams :: Decl -> List Name
- declType :: Decl -> Expr
- data DeclView
- declView :: Decl -> DeclView
- data CertDecl
- check :: Env -> Decl -> CertDecl
Documentation
Constructors
Create an axiom.
Create a constant.
Constants and axioms in Lean are essentially the same thing.
Arguments
| :: Name | Name of the definition |
| -> List Name | Universe parameters for defintion |
| -> Expr | Type of definition |
| -> Expr | Value of definition |
| -> Word32 | Definitional height |
| -> Bool | Flag that indicates if definition should be lazily unfolded |
| -> Decl |
Create a definition with an explicit definitional height
Arguments
| :: Env | The environment |
| -> Name | Name of the definition |
| -> List Name | Universe parameters for defintion |
| -> Expr | Type of definition |
| -> Expr | Value of definition |
| -> Bool | Flag that indicates if definition should be lazily unfolded |
| -> Decl |
Create a definition with a definitional height computed from the environment.
The definitional height is computed using information from the environment.
Arguments
| :: Name | Name of the theorem |
| -> List Name | Universe parameters for theorem |
| -> Expr | Type of the theorem |
| -> Expr | Proof of the theorem |
| -> Word32 | Definitional height |
| -> Decl |
Creates a theorem with an explicit definitional height.
Theorems and definitions are essentially the same thing in Lean, except in the way the normalizer treats them. The normalizer will only unfold theroem if there is nothing else to be done when checking whether two terms are definitionally equal or not.
Arguments
| :: Env | The environment |
| -> Name | The name of the theorem |
| -> List Name | Universe parameters for theorem |
| -> Expr | Type of the theorem |
| -> Expr | Proof of the theorem |
| -> Decl |
theoremWith creates a theorem that is relative to an environment.
Theorems and definitions are essentially the same thing in Lean, except in the way the normalizer treats them. The normalizer will only unfold theroem if there is nothing else to be done when checking whether two terms are definitionally equal or not.
The definitional height is computed from environment.
Projections
declUnivParams :: Decl -> List Name Source
The list of universe params for a declaration.
Information about a declaration