Switch to strict bulleting everywhere
Solve #82 (closed).
The flag isn't enforced anywhere, but with this we can add it seamlessly (ideally soon after so there aren't more violations that creep in).
Merge request reports
Activity
I think this is pretty OK. I would prefer
split; [tac1|]orsplit; [|tac2]iftac1ortac2is relatively short. If they are longer (which is quite subjective, but certainly more than justby apply foo,left; by apply foo,apply foo; lia,apply foo; auto), I would prefer bullets.That said, I could also do this myself, if you prefer. But if you agree to my above suggestion, then I am likely to support this MR with few comments :).
What about importing enough of ssreflect to be able to use
first/last? This does not incur an extra dependency any more (if we raise the minimal Coq version enough).EDIT: Oh, the ssreflect merger already was back with Coq 8.7... I forgot.^^
Edited by Ralf JungI tried to go along with your suggestion, to the extent I understand what you meant by "relatively short". If you spot anything that should be changed, I'm happy to fix it - I think there aren't that many unclear changes, most were straightforward.
I would also prefer the more basic
[done|]compared to importing ssreflect and usingfirst. It's one less thing to learn.-
I find
tac; first tacmuch easier to type and read thantac; [tac|..]. The latter uses sigils instead of a clear keyword, making it much harder to read, and it involves[,], and|, making it really hard to type as well (at least on my keyboard layout).Arguably,
tac; first tachardly requires any learning. I certainly never read the docs for that. I did have to read the docs for;[..|].Edited by Ralf Jung I think I'd prefer to not introduce a dependency on ssreflect for std++, while in Iris we can use
firstas much of the existing code does already. Once you're usingfirstI agree that; first donebecomes a nicer pattern, but I was personally confused to see a tactical change goal focusing, since vanilla Ltac1 has no such tactical to my knowledge.I'm not that concerned about making code harder to type since it'll be read more than written. That said, I did adjust my keyboard layout to make it easier to type Iris code.
Note that std++ always (or nearly always) uses a fixed number of tactic and not the
; [tac | ..]variadic thing.For a single tactic,
firstandlastare reasonable. But for multiple tacticsfirst tac1; tac2, it's totally impossible to read that without knowing the precedence rules (I don't know them for this case). You seemed to have ignored that argument @jung...Anyway, this discussion is most likely moot, because I don't think we should let std++ depend on ssreflect, and certainly, this MR should not do that.
-
For a single tactic,
firstandlastare reasonable. But for multiple tacticsfirst tac1; tac2, it's totally impossible to read that without knowing the precedence rules (I don't know them for this case). You seemed to have ignored that argument @jung...Sorry, forgot to respond to that part. As usual when precedence is unclear, the solution is to add parentheses. That is IMO still easier to read and type than the
[...]alternative.I am not sure what "depend on" means here given that everything we need is part of the Coq standard library. But I am okay with dropping this point for now, since I don't write std++ MRs so often. It's just every single time I upstream something from an Iris-using project, I have to remove all the
lastandfirsteverywhere which is the most annoying part of the upstreaming process.^^ So this is a way in which having different proof styles between std++ and Iris is actually a problem for moving code around between the two. I am not sure what "depend on" means here given that everything we need is part of the Coq standard library.
The problem is that ssreflect overrides a bunch of stuff, in particular
rewrite(same name, totally different tactic). So, once we start importing ssreflect, it will have quite severe consequences (some maybe good, some bad, who knows, it's certainly a major change).
mentioned in commit f4a2763b
