infer pos p c t returns a couple (t',a) where a is the type of t in context c and under constraints of problem p; and t' is the refinement of t. Note that p gets modified. Context c must well sorted.

• raises Fatal

  if t cannot be typed.

check pos p c t a checks that the term t has type a in context c and under the constraints of p, and returns t refined. Context c must be well-sorted. Note that p is modified.

• raises Fatal

  if t is not of type a.

check_sort pos p c t checks that the term t has type Type or Kind in context c and under the constraints of p. Context c must be well sorted.

• raises Fatal

  if t cannot be typed by a sort (Type or Kind).

Result of query displayed on hover in the editor.

handle_query ss ps q