Radosław Rowicki
Radosław Rowicki
A loop construct in fcode could help
@UlfNorell How does it break the consensus?
Note that state modifications are still explicit, as one needs to refer to the `state` as lvalue.
I think it would be much more user friendly if we explicitly point out that dependency cycles are not supported. For example functions within one namespace do support mutual recursion,...
Printout of the params to `decompose_prod_n`, where the anomaly happens: ``` n = 4 c = forall P:forall b:Ind(Test.A,1), Type(Test.26), forall f:(#1 Constr(Test.A,1,1)), forall b:Ind(Test.A,1), (#3 #1) ``` crash on...
The failure comes from `build_combined_scheme` in `vernac/indschemes.ml` which receives the following `defs` (the anomaly example): ```coq DEF 0: forall P:forall a:Ind(Test.A,0), Type(Test.25), forall P0:forall b:Ind(Test.A,1), Type(Test.26), forall f:forall a:Ind(Test.A,0), ((#3...
Setting `force_mutual` in `do_mutual_induction_scheme` to `length l > 1` (call in `do_scheme`) seems to solve the issue (setting to `true` breaks some tests). Idk if it's a viable solution.
To me that's actually pretty annoying. I ditched isearch specifically because of this, since it was barely usable with a similar issue. It just takes a single mouse click to...
Bumping the issue — reproduced in `8.19.2`
Wow, is that documented somewhere? I never stumbled upon it in Ltac2 references. Though, it behaves slightly weird if it appears multiple times in an `open_constr`: `open_constr:(?[var] + ?[var])` doesn't...