package lambdapi

You can search for identifiers within the package.

in-package search v0.2.0

Proof assistant for the λΠ-calculus modulo rewriting

Install

dune-project

Dependency

sha256=66d7d29f7a0d10493b8178c4c3aeb247971e24fab3eba1c54887e1b9a82fe005

sha512=69ecf2406e4c7225ab7f8ebe11624db5d2ab989c8f30f5b6e5d426fd8ef9102f142a2840af16fb9103bb712ebcf7d314635f8b413a05df66e7b7a38548867032

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

Sourcetype 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