Théo Winterhalter (May 06 2021 at 07:03): Théo Winterhalter (May 06 2021 at 07:03):Hi, is there a Notation trick to show the position of a node, in a tree for instance?
A simpler example would be lists where it would show something like
[ 0: x ; 1: y ; 2: z ]
or something of the sort. It would only be for printing.
I would like to basically do a change (or repeated changes) or something in the goal to make these numbers appear, but if possible not affect the proof term. Otherwise I can just write a tactic which would replace the term with one using numbers that, and the tactic would count them.
Michael Soegtrop (May 06 2021 at 07:10):I usually write Ltac2 tactics to print terms with additional information or analysis - it is quite convenient for that. For release Coq one needs a bit of convenience wrapper code for the Ltac2 message system, though. In master this is much improved via a printf function. In case you need to use release Coq, I can share my wrappers as example (they are a bit clumsy but get the job done until 8.14 is out). One wouldn't have to fire any proof term modifying tactic for that.
I am not a big fan of having fancy print only notations, because it has the effect that one can't copy paste terms.
Théo Winterhalter (May 06 2021 at 07:15):Ah I see, instead you print the terms , I hadn't thought of that.
Yeah you can't copy paste them, but here the point is to only locally have this information. I don't really want to go for coq.dev yet, but it's good to know. Thanks!
Michael Soegtrop (May 06 2021 at 08:50):You don't really need dev. The Ltac2 message system in release works, it is just a bit "bare bone" but it is not hard to fix that if one is happy with a not so elegant intermediate solution. Essentially I have a bunch of print and concat functions for different common combinations of argument types and type combinator, which I extend as needed. Not nice, but works.
Théo Winterhalter (May 06 2021 at 09:29):I see.
Last updated: Apr 20 2024 at 08:02 UTC