package lambdapi
Proof assistant for the λΠ-calculus modulo rewriting
Install
dune-project
Dependency
Authors
Maintainers
Sources
lambdapi-3.0.0.tbz
sha256=1066aed2618fd8e6a400c5147dbf55ea977ce8d3fe2e518ac6785c6775a1b8be
sha512=f7f499626aba92e070ae69581299a58525973fdbfd04a160ed3ac89209fb6cbe307b816d0b23e1b75bc83467ce8b4b0530c6f9816eaf58f7a07fde65a450106c
doc/lambdapi.common/Common/Name/index.html
Module Common.Name
Source
Generation of fresh names.
If s
ends with some digits, then root_and_index s = (root,i)
such that i
is the biggest integer such that s = root^string_of_int i
. Otherwise, root_and_index s = (s,-1)
.
Assume that root_and_index p = (r,i)
. If i<0
then get_safe_prefix p idmap
returns p,StrMap.add p (-1) idmap
and, for all non-negative integer k
, StrSet.mem (p^string_of_int k) (strings idmap')=false
. Otherwise, get_safe_prefix p idmap
returns r^string_of_int k,StrMap.add r k idmap
, where k
is greater than or equal to i
and 1 + the index of r
in idmap
.
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>