package lambdapi

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

val infer : 
  Common.Pos.popt ->
  Core.Term.problem ->
  Core.Term.ctxt ->
  Core.Term.term ->
  Core.Term.term

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

val check : 
  Common.Pos.popt ->
  Core.Term.problem ->
  Core.Term.ctxt ->
  Core.Term.term ->
  Core.Term.term ->
  unit

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

val check_sort : 
  Common.Pos.popt ->
  Core.Term.problem ->
  Core.Term.ctxt ->
  Core.Term.term ->
  unit

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

type result = (unit -> string) option

Result of query displayed on hover in the editor.

val handle : 
  Core.Sig_state.t ->
  Proof.proof_state option ->
  Parsing.Syntax.p_query ->
  result

handle_query ss ps q