package lambdapi

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

Install

dune-project
 Dependency

Authors

Maintainers

Sources

lambdapi-2.4.0.tbz
sha256=739cab9a0a6c3ab0e7df210fb6fdcdb749a6fa70aa7ca59145da177c25428cb6
sha512=f1413e65259d1587d57d656a5153890c355fa339d981c0b038736bcaf53c698cc10466fbc77444d103c7b6ccb8d63290ff80a506d057bc199a29d53947e898c9

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.