lambdapi
lambdapi copied to clipboard
Deducteam
Proof assistant based on the λΠ-calculus modulo rewriting
PR #289 silently removed important unit tests in the Pure module. We try to recover them, but indeed, they don't work, as it seems the library handling API introduced in...
The following code defines the relation used in our algorithm for checking subject reduction. There might be some modifications after since some details in the algorithm still need to be...
The example ``` symbol Set: TYPE set declared "η" injective symbol η: Set ⇒ TYPE symbol arr: Set ⇒ Set ⇒ Set rule η (arr &X &Y) → (η &X)...
Would it be possible to have why3 as an optional dependency of the project?
Currently, it is not possible to write rewrite rule such as: ``` [a] f (double 0) a --> a. ``` where `double 0` reduces to `S (S 0)`. Because this...
This field would be set after checking subjection reduction. This would simplify termination and confluence checking. Note that it is important that termination and confluence checking is fast. Otherwise people...
Dear all, As you may know, some of us are interested in interactivity features during unification. Whatever it means concretely (unification hints #361, a new tactic language, etc...), this is...
To have a nicer access to the documentation. If I'm not mistaken, the only thing to do is rename `doc` into `docs` and activate some switch in the settings. Perhaps...
In a rule LHS, type annotations of abstractions are replaced by the *same* variable m_typ: https://github.com/Deducteam/lambdapi/blob/82dccc5074bd42574d8d21b9b39527052d2014cd/src/core/hrs.ml#L38