lambdapi
Proof assistant for the λΠ-calculus modulo rewriting
1024" x-on:close-sidebar="sidebar=window.innerWidth > 1024 && true">
package lambdapi
-
lambdapi.tool
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
is_escaped s
tells if s
begins with "{|"
and ends with "|}"
without overlapping. For efficiency, we just test that it starts with '{'
.
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 ^ "|}"
.
ON THIS PAGE
No table of contents