Frédéric Blanqui
Frédéric Blanqui
Hi Ciaran. Which editor do you use?
In various cases, apply fails and you need to instead use refine with various underscores. I'm trying to make apply works more often.
It's because you declared test as sequential. For sequential symbols, rules are tried in the order they are declared. In your example, x does not match C1 but it marches...
Please provide more details and some example so that we can help you more if possible.
Why do you want to use a sequential symbol for doing that?
Right, you need mem to be sequential here. @NotBad4U and @melanie-taprogge do similar things to reify Lambdapi terms into some data types in the implementation of their reflexive tactics. I...
The assert's this issue is about are the OCaml assert's used to implement Lambdapi. For feature requests concerning the Lambdapi commands assert/assertnot, please open a distinct issue.
Shouldn't we get rid of cmdliner?
Hi. Could you please precise what happens when you uncomment the line with print unif_rule? I don't see any problem with vscode 1.96.2.