Morte

A bare-bones calculus-of-constructions

Types

data Const

Constants

Constructors

Star

Box

Instances

Bounded Const

Enum Const

Eq Const

Show Const

data Expr

Higher-order abstract syntax tree for expressions

Constructors

Const Const

Var Int

Lam Expr (Expr -> Expr)

Pi Expr (Expr -> Expr)

App Expr Expr

Instances

Eq Expr

Show Expr

Functions

typeOf :: Expr -> Either Text Expr

Type-check an expression and return the expression's type

normalize :: Expr -> Expr

Reduce an expression to normal form

pretty :: Expr -> Text

Pretty-print an expression as lazy Text