| Copyright | (c) Galois Inc, 2015 |
|---|---|
| License | Apache-2 |
| Maintainer | jhendrix@galois.com, lcasburn@galois.com |
| Safe Haskell | Trustworthy |
| Language | Haskell98 |
Language.Lean.Internal.Expr
Description
Internal declarations for Lean expressions and typeclass instances for Expr.
- data MacroDef
- type MacroDefPtr = Ptr MacroDef
- type OutMacroDefPtr = Ptr MacroDefPtr
- withMacroDef :: MacroDef -> (Ptr MacroDef -> IO a) -> IO a
- data Expr
- type ExprPtr = Ptr Expr
- type OutExprPtr = Ptr ExprPtr
- withExpr :: Expr -> (Ptr Expr -> IO a) -> IO a
- exprLt :: Expr -> Expr -> Bool
- exprToString :: Expr -> String
- data BinderKind
- type ListExpr = List Expr
- type ListExprPtr = Ptr ListExpr
- type OutListExprPtr = Ptr ListExprPtr
- withListExpr :: List Expr -> (Ptr (List Expr) -> IO a) -> IO a
Macro definitions
A Lean macro definition
type MacroDefPtr = Ptr MacroDef Source
Haskell type for lean_macro_def FFI parameters.
type OutMacroDefPtr = Ptr MacroDefPtr Source
Haskell type for lean_macro_def* FFI parameters.
withMacroDef :: MacroDef -> (Ptr MacroDef -> IO a) -> IO a Source
Function c2hs uses to pass MacroDef values to Lean
Expressions
A Lean expression
Instances
| Eq Expr Source | |
| Ord Expr Source | |
| Show Expr Source | |
| IsLeanValue Expr (Ptr Expr) Source | |
| IsList (List Expr) Source | |
| Eq (List Expr) Source | |
| Show (List Expr) Source | |
| IsListIso (List Expr) Source | |
| IsLeanValue (List Expr) (Ptr (List Expr)) Source | |
| type Item ListExpr = Expr Source | |
| data List Expr = ListExpr (ForeignPtr (List Expr)) Source | A list of expressions (constructor not actually exported) |
type OutExprPtr = Ptr ExprPtr Source
Haskell type for lean_expr* FFI parameters.
exprLt :: Expr -> Expr -> Bool Source
Return true if first expression is structurally less than other.
exprToString :: Expr -> String Source
Return the string representation of an expression.
List of expressions
type ListExprPtr = Ptr ListExpr Source
Haskell type for lean_list_expr FFI parameters.
type OutListExprPtr = Ptr ListExprPtr Source
Haskell type for lean_list_expr* FFI parameters.