| Copyright | (c) Galois Inc, 2015 |
|---|---|
| License | Apache-2 |
| Maintainer | jhendrix@galois.com, lcasburn@galois.com |
| Safe Haskell | Trustworthy |
| Language | Haskell98 |
Language.Lean.Typechecker
Description
Interface to Lean typechecker
- data Typechecker
- data ConstraintSeq
- typechecker :: Env -> Typechecker
- inferType :: Typechecker -> Expr -> (Expr, ConstraintSeq)
- checkType :: Typechecker -> Expr -> (Expr, ConstraintSeq)
- whnf :: Typechecker -> Expr -> (Expr, ConstraintSeq)
- isDefEq :: Typechecker -> Expr -> Expr -> (Bool, ConstraintSeq)
Documentation
typechecker :: Env -> Typechecker Source
Create a type checker object for the given environment.
inferType :: Typechecker -> Expr -> (Expr, ConstraintSeq) Source
inferType t e infers the type of e using t.
This returns the type and any constraints generated.
The expression e must not contain any free variables (subexpressions with
type ExprVar).
checkType :: Typechecker -> Expr -> (Expr, ConstraintSeq) Source
inferType t e checks and infers the type of e using t.
This returns the type and any constraints generated.
The expression e must not contain any free variables (subexpressions with
type ExprVar).
whnf :: Typechecker -> Expr -> (Expr, ConstraintSeq) Source
whnf t e computes the weak-head-normal-form of e using t, returning the
form and any generated constraints.
The expression e must not contain any free variables (subexpressions with
type ExprVar).
isDefEq :: Typechecker -> Expr -> Expr -> (Bool, ConstraintSeq) Source
is_def_eq t e1 e2 returns True iff e1 and e2 are definitionally equal along
with any generated constraints.
The expressions e1 and e2 must not contain any free variables
(subexpressions with type ExprVar).