package alba

You can search for identifiers within the package.

in-package search v0.2.0

Alba compiler

Install

sha256=439b1dce07c86e914d1ebf1712c5581418314b0c8d13594f27a698b1d25fe272

md5=5cf58d4ed4eacbe6f330e9d2378ef5c6

Sourceval is_valid_context : Gamma.t -> bool

is_valid_context gamma

Is the context gamma wellformed?

Sourceval check : Term.t -> Gamma.t -> Term.typ option

check term gamma

Verify if term is welltyped in the valid context gamma. If yes, return its type.

Precondition:

is_valid_context gamma