Module Handle.QuerySource

infer pos p c t returns a type for the term t in context c and under the constraints of p if there is one, or

• raises Fatal.

  c must well sorted. Note that p gets modified.

check pos p c t a checks that the term t has type a in context c and under the constraints of p, or

• raises Fatal.

  c must well sorted. Note that p gets modified.

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, or

• raises Fatal.

  c must be well sorted.

Result of query displayed on hover in the editor.

handle_query ss ps q