package lambdapi

  1. Overview
  2. Docs
Proof assistant for the λΠ-calculus modulo rewriting

Install

Dune Dependency

Authors

Maintainers

Sources

lambdapi-2.4.1.tbz
sha256=221dff97ab245c49b7e6480fa2a3a331ab70eb86dd5d521e2c73151029bbb787
sha512=a39961bb7f04f739660a98a52981d4793709619cd21310ca6982ba78af81ef09e01c7517ee3b8b2687b09f7d2614d878c1d69494ca6ab8ef8205d240c216ce8a

doc/lambdapi.handle/Handle/Query/index.html

Module Handle.QuerySource

Handling of queries.

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).

Sourcetype result = (unit -> string) option

Result of query displayed on hover in the editor.

handle_query ss ps q

OCaml

Innovation. Community. Security.