Language.Lean.Expr

Operations for Lean expressions.

Documentation

data MacroDef

A Lean macro definition

Instances

Eq MacroDef

Show MacroDef

IsLeanValue MacroDef (Ptr MacroDef)

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)

data BinderKind

Kind of binding used for bound variables.

Constructors

BinderDefault

BinderImplicit

BinderStrictImplicit

BinderInstImplicit

BinderHidden

Instances

Enum BinderKind

Eq BinderKind

Show BinderKind

Constructors

varExpr :: Word32 -> Expr

Create a variable with de-Bruijn index i. This is a bound variable.

sortExpr :: Univ -> Expr

Creates a type for the given universe

constExpr :: Name -> List Univ -> Expr

Create a constant with a given name and universe parameters

appExpr :: Expr -> Expr -> Expr

Create a function application for expressions

lambdaExpr :: BinderKind -> Name -> Expr -> Expr -> Expr

Create a lambda abstraction for expressions

piExpr :: BinderKind -> Name -> Expr -> Expr -> Expr

Create a pi abstraction for expressions

macroExpr :: MacroDef -> List Expr -> Expr

Create a macro application for expressions

localExpr :: Name -> Expr -> Expr

Create a local constant with the given name and type.

localExtExpr

Arguments

:: BinderKind

The binder kind for expression

-> Name

The name of expression

-> Name

The pretty print name

-> Expr

The type of the expression

-> Expr

Create a local constant with additional parameters

metavarExpr :: Name -> Expr -> Expr

Create a metavariable with the given name nm and type tp.

View

data ExprView

Information about the expression.

Constructors

ExprVar Word32

ExprSort Univ

ExprConst Name (List Univ)

ExprLocal BinderKind Name Name Expr

ExprMeta Name Expr

ExprApp Expr Expr

ExprLambda BinderKind Name Expr Expr

ExprPi BinderKind Name Expr Expr

ExprMacro MacroDef (List Expr)

Instances

Eq ExprView

Show ExprView

exprView :: Expr -> ExprView

View information about the structure of an expression.

Operations

exprLt :: Expr -> Expr -> Bool

Return true if first expression is structurally less than other.

exprToString :: Expr -> String

Return the string representation of an expression.