Language.Lean.Internal.Expr

Internal declarations for Lean expressions and typeclass instances for Expr.

Macro definitions

data MacroDef

A Lean macro definition

Instances

Eq MacroDef

Show MacroDef

IsLeanValue MacroDef (Ptr MacroDef)

type MacroDefPtr = Ptr MacroDef

Haskell type for lean_macro_def FFI parameters.

type OutMacroDefPtr = Ptr MacroDefPtr

Haskell type for lean_macro_def* FFI parameters.

withMacroDef :: MacroDef -> (Ptr MacroDef -> IO a) -> IO a

Function c2hs uses to pass MacroDef values to Lean

Expressions

data Expr

A Lean expression

Instances

Eq Expr

Ord Expr

Show Expr

IsLeanValue Expr (Ptr Expr)

IsList (List Expr)

Eq (List Expr)

Show (List Expr)

IsListIso (List Expr)

IsLeanValue (List Expr) (Ptr (List Expr))

type Item ListExpr = Expr

data List Expr = ListExpr (ForeignPtr (List Expr))

A list of expressions (constructor not actually exported)

type ExprPtr = Ptr Expr

Haskell type for lean_expr FFI parameters.

type OutExprPtr = Ptr ExprPtr

Haskell type for lean_expr* FFI parameters.

withExpr :: Expr -> (Ptr Expr -> IO a) -> IO a

Get access to lean_expr within IO action.

exprLt :: Expr -> Expr -> Bool

Return true if first expression is structurally less than other.

exprToString :: Expr -> String

Return the string representation of an expression.

data BinderKind

Kind of binding used for bound variables.

Constructors

BinderDefault

BinderImplicit

BinderStrictImplicit

BinderInstImplicit

BinderHidden

Instances

Enum BinderKind

Eq BinderKind

Show BinderKind

List of expressions

type ListExpr = List Expr

Synonym for List Expr that can be used in c2hs bindings

type ListExprPtr = Ptr ListExpr

Haskell type for lean_list_expr FFI parameters.

type OutListExprPtr = Ptr ListExprPtr

Haskell type for lean_list_expr* FFI parameters.

withListExpr :: List Expr -> (Ptr (List Expr) -> IO a) -> IO a

Function c2hs uses to pass ListExpr values to Lean