package lambdapi
Proof assistant for the λΠ-calculus modulo rewriting
Install
Dune Dependency
Authors
Maintainers
Sources
lambdapi-2.5.1.tbz
sha256=2c251021b6fac40c05282ca183902da5b1008e69d9179d7a9543905c2c21a28a
sha512=69535f92766e6fedc2675fc214f0fb699bde2a06aa91d338c93c99756235a293cf16776f6328973dda07cf2ad402e58fe3104a08f1a896990c1778b42f7f9fcf
doc/lambdapi.export/Export/Coq/index.html
Module Export.Coq
Source
Translate the parser-level AST to Coq.
There are two modes:
- raw_coq mode (option -o raw_coq): translation of the AST as it is (lambdapi-calculus is a subset system of coq if we ignore rules)
- stt_coq mode (option -o stt_coq): translation of the AST as an encoding in simple type theory.
The encoding can be specified through a lambdapi file (option --encoding).
In both modes, a renaming map can be provided to rename some identifiers.
The renaming map can be specified through a lambdapi file (option --renaming).
Symbols necessary to encode STT.
Set renaming map from file.
Set symbols whose declarations have to be erased.
Set encoding.
Basic printing functions. We use Printf for efficiency reasons.
Translation of identifiers.
Translation of terms.
Source
val app :
Parsing.Syntax.p_term ->
(Parsing.Syntax.p_term -> Parsing.Syntax.p_term list -> 'a) ->
(Parsing.Syntax.p_term ->
Parsing.Syntax.p_term list ->
bool ->
builtin ->
'a) ->
'a
Translation of commands.
Set Coq required file.
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>