Stream: Coq users

Topic: Showing the position of a node in tree


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Théo Winterhalter (May 06 2021 at 09:29):

I see.


Last updated: Jan 29 2023 at 01:02 UTC