bodeveix
bodeveix
It seems the problem can be fixed by modifying line 247 of tactic.ml: | Some (_, a) -> count_products c a **- count_products c gt.goal_type**
Hello Frédéric, Thanks for your reply. (λ h, h) was used to make an apply, not a refine. So it should let the goal unchanged. In the original proof, the...
I have a definition x y := not (x = y) and a goal : \pi (P x y => x y) apply (fun (h: \pi (P x y =>...
Can you send me the failing proof? Thanks. > Le 27 août 2024 à 13:57, Jean-Paul Bodeveix ***@***.***> a écrit : > > I have a definition x y :=...
But, because x is unknown, we cannot decide if x=C1 or not, so rule application should block. Otherwise, reduction becomes non confluent: (λ x, test x) C1 --> C2 if...
Here I would say that we don't know if x matches C1 or not. We need sequential to write some meta level functions and we need default cases, those that...
For example, looking for a given element in list of formulas (any lambdapi formula of a given type).
If I don't have equality on formulas: I would declare mem sequential and the rules: ``` rule mem $f ($f::_) --> true with mem $f (_::$l) --> mem $f $l...
I have solved the issue by adding a tactic "#call f a" which allows delaying the evaluation of (f a) until the interpretation of #call: In tactic.ml: ``` | T_call,...