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.common/Common/Escape/index.html

Module Common.EscapeSource

Escaped identifiers "{|...|}".

Sourceval is_escaped : string -> bool

is_escaped s tells if s begins with "{|" and ends with "|}" without overlapping. For efficiency, we just test that it starts with '{'.

Sourceval unescape : string -> string

unescape s removes "{|" and "|}" if s is an escaped identifier.

Sourceval add_prefix : string -> string -> string

p is assumed to be a regular identifier. If n is a regular identifier too, then add_prefix p n is just p ^ n. Otherwise, it is "{|" ^ p ^ unescape n ^ "|}".

Sourceval add_suffix : string -> string -> string

s is assumed to be a regular identifier. If n is a regular identifier too, then add_suffix n s is just n ^ s. Otherwise, it is "{" ^ unescape n ^ s ^ "|}".

OCaml

Innovation. Community. Security.