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

github.com Readme Changelog Edit opam file Versions (12)

Authors

D

Deducteam

Maintainers

D

dedukti-dev@inria.fr

Sources

lambdapi-2.1.0.tbz

sha256=04fac3b56d1855795d7d2d2442bc650183bcd71f676c3ea77f37240e33769ce9

sha512=37f7bec3bc48632379ca9fb3eb562a0c0387e54afbdd10fb842b8da70c6dad529bb98c14b9d7cddf44a1d5aa61bba86338d310e6a7b420e95b2996b4fbafc95c

doc/lambdapi.tool/Tool/External/index.html

Module `Tool.External`Source

Provides a function for calling external checkers using a Unix command.

Sourceval log_xtrn : 'a Lplib.Base.outfmt -> 'a

Source

val run : 
  string ->
  Core.Sign.t Lplib.Base.pp ->
  string ->
  Core.Sign.t ->
  bool option

run prop pp cmd sign runs the external checker given by the Unix command cmd on the signature sign. The signature is processed and written to a Unix pipe using the formatter pp, and the produced output is fed to the command on its standard output. The return value is Some true in case of a successful check, Some false in the case of a failed check, and None if the external tool cannot conclude. Note that the command cmd should write either "YES", "NO" or "MAYBE" as its first line of (standard) output. The exception Fatal may be raised if cmd exhibits a different behavior. The name prop is used to refer to the checked property when an error message is displayed.

NOTE that for any given property being checked, the simplest possible valid command is "echo MAYBE". Moreover, "cat > file; echo MAYBE" can conveniently be used to write generated data to the file "file". This is useful for debugging purposes.