type_of_term term gamma

Compute the type of term

Precondition: term must be welltyped and the context valid.

sort_of_kind typ gamma

Compute the sort of the kind typ. If typ does not reduce to a kind, then return None.

Precondition: typ must be welltyped and the context gamma must be valid.

A kind has the form

all (x: A) (y: B) .... : s

where s is a sort.

is_kind typ gamma

Is the welltyped term typ in the valid context gamma a kind?

keynormal term gamma

Compute the key normal form of the welltyped term term in the valid context gamma.