package lambdapi
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=221dff97ab245c49b7e6480fa2a3a331ab70eb86dd5d521e2c73151029bbb787
sha512=a39961bb7f04f739660a98a52981d4793709619cd21310ca6982ba78af81ef09e01c7517ee3b8b2687b09f7d2614d878c1d69494ca6ab8ef8205d240c216ce8a
doc/lambdapi.core/Core/LibMeta/index.html
Module Core.LibMeta
Source
Functions to manipulate metavariables.
reset_meta_counter ()
resets the counter used to produce meta keys.
fresh p ?name a n
creates a fresh metavariable of type a
and arity n
with the optional name name
, and adds it to p
.
fresh_box p a n
is the boxed counterpart of fresh_meta
. It is only useful in the rare cases where the type of a metavariable contains a free term variable environment. This should only happens when scoping the rewriting rules, use this function with care. The metavariable is created immediately with a dummy type, and the type becomes valid at unboxing. The boxed metavariable should be unboxed at most once, otherwise its type may be rendered invalid in some contexts.
set p m v
sets the metavariable m
of p
to v
. WARNING: No specific check is performed, so this function may lead to cyclic terms. To use with care.
make p ctx a
creates a fresh metavariable term of type a
in the context ctx
, and adds it to p
.
bmake p bctx a
is the boxed version of make
: it creates a fresh boxed metavariable in boxed context bctx
of boxed type a
. It is the same as lift (make p c b)
(provided that bctx
is boxed c
and a
is boxed b
), but more efficient.
make_codomain p ctx a
creates a fresh metavariable term of type Type
in the context ctx
extended with a fresh variable of type a
, and updates p
with generated metavariables.
bmake_codomain p bctx a
is make_codomain p bctx a
but on boxed terms.
iter b f c t
applies the function f
to every metavariable of t
and, if x
is a variable of t
mapped to v
in the context c
, then to every metavariable of v
, and to the type of every metavariable recursively if b
is true.