package lambdapi

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

Install

Dune Dependency

Authors

Maintainers

Sources

lambdapi-2.5.0.tbz
sha256=9bc8ae3694dd51bd5742e7aba760bd2878c4b0e5ef9b3d4a7b06f3cd303b611d
sha512=c812c3129b3d85b0c4d7e741d11137dbb4fe2a0aaba3a5968409080b742924ecb506280c19ad83ef6bc910346db96d87780313fa7683c29345edae16ae79c704

doc/lambdapi.lplib/Lplib/Extra/index.html

Module Lplib.ExtraSource

Sourcemodule IntMap : sig ... end

Functional maps with int keys.

Sourcemodule IntSet : sig ... end

Functional sets of integers.

Sourcemodule StrMap : sig ... end

Functional maps with string keys.

Sourcemodule StrSet : sig ... end

Functional sets of strings.

Sourceval get_safe_prefix : string -> StrSet.t -> string

get_safe_prefix p strings returns a string starting with p and so that there is no non-negative integer k such that p ^ string_of_int k belongs to strings.

Sourceval time : ('a -> 'b) -> 'a -> float * 'b

time f x times the application of f to x, and returns the evaluation time in seconds together with the result of the application.

Sourceexception Timeout

Exception raised by the with_timeout function on a timeout.

Sourceval with_timeout : int -> ('a -> 'b) -> 'a -> 'b

with_timeout nbs f x computes f x with a timeout of nbs seconds. The exception Timeout is raised if the computation takes too long, otherwise everything goes the usual way.

Sourceval input_lines : in_channel -> string list

input_lines ic reads the input channel ic line by line and returns its contents. The trailing newlines are removed in lines. The input channel is not closed by the function.

Sourceval run_process : string -> string list option

run_process cmd runs the command cmd and returns the list of the lines that it printed to its standard output (if the command was successful). If the command failed somehow, then None is returned.

Sourceval file_time : string -> float

file_time fname returns the modification time of file fname represented as a float. neg_infinity is returned if the file does not exist.

Sourceval more_recent : string -> string -> bool

more_recent source target checks whether the target (produced from the source file) should be produced again. This is the case when source is more recent than target.

Sourceval files : (string -> bool) -> string -> string list

files f d returns all the filenames in d and its sub-directories recursively satisfying the function f, assuming that d is a directory.

OCaml

Innovation. Community. Security.