bodeveix
bodeveix
The apply has a strange behaviour when the goal is quantified. In the following proof, apply (λ h, h) lets the goal unchanged as expected. However, if we try to...
The eval tactic seems to ignore the implicit parameter annotation when reconstructing terms and thus acts as if functions were prefixed by @ while they are not. The problem seems...
An exception is raised by the remove tactic from function codom_binder when the list of hypotheses contains a defined variable. The following modified code (libTerm.ml) seems to solve the problem:...
When a global identifier has the same name as a binder and is inserted under the binder after beta reduction, the binder should be renamed. In the following example, `x`...
In the following example, the function (λ x, test x) is reduced to (λ x, C2), which seems strange as the parameter is unknown. I would expect the expression to...