package alba

  1. Overview
  2. Docs
package alba
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Problem : sig ... end
type path = int list
val is_valid_context : Gamma.t -> bool

is_valid_context gamma

gamma is wellformed if

  • every type is valid, i.e. it typechecks using only entries of gamma with a smaller level (this is true by contruction, since we are using de bruijn indices)
  • the same holds for all definition terms
  • TODO: every type is a type (and not an object)
  • returns

    true, if gamma is wellformed, false otherwise

val equivalent : Term.typ -> Term.typ -> Gamma.t -> bool
val check : Term.t -> Gamma.t -> (Term.typ, path * Problem.t) Stdlib.result

check term gamma

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

Precondition:

is_valid_context gamma