latte-kernel.presyntax — latte-kernel 1.0b7-SNAPSHOT

The rich syntax of the lambda-calculus implemented by LaTTe.

+reserved-symbols+ clj/s

arrow-kw? clj/s

(arrow-kw? t)

Arrow type?

exists-kw? clj/s

(exists-kw? t)

Existential?

kind? clj/s

(kind? t)

Is t the sort :kind?

lambda-kw? clj/s

(lambda-kw? t)

Lambda abstraction?

left-binarize clj/s

(left-binarize t)

Binarization (sic!) of an application.

parse clj/s

(parse t)

(parse def-env t)

Parse term t in definitional environment def-env (empty by default).

parse-application-term clj/s

(parse-application-term def-env t bound)

parse-arrow-term clj/s

(parse-arrow-term def-env t bound)

Parse an arrow type.

parse-binder-term clj/s

(parse-binder-term def-env binder t bound)

Parse the binding vector of an abstraction form.

parse-binding clj/s

(parse-binding def-env v bound)

Parse an abstraction binding form.

parse-compound-term clj/s

(parse-compound-term def-env t bound)

Parses t as a compound term.

parse-defined-term clj/s

(parse-defined-term def-env sdef t bound)

Parse a defined term.

parse-lambda-term clj/s

(parse-lambda-term def-env t bound)

Parse a lambda abstraction.

parse-product-term clj/s

(parse-product-term def-env t bound)

Parse a production abstraction.

parse-symbol-term clj/s

(parse-symbol-term def-env sym bound)

parse-term clj/s

(parse-term def-env t)

(parse-term def-env t bound)

Parses the input term t in definitional environment def-env and set of bound variables bound. The function returns a pair with the keyword :ok and the parsed term if the parse was successful, else :ko followed by a parse error.

parse-terms clj/s

(parse-terms def-env ts bound)

Parse a sequence ts of terms.

product-kw? clj/s

(product-kw? t)

Product abstraction?

reserved-symbol? clj/s

(reserved-symbol? s)

Is s a reserved symbol?

type? clj/s

(type? t)

Is t the sort :type?