Email Gateway (Aug 17 2022 at 14:43): Email Gateway (Aug 17 2022 at 14:43):From: "F. Miguel Dionisio" <fmd@math.ist.utl.pt>
Hi,
Does anyone know how to acess to the list of currently bound variables
(namely to know the names of Bound 0, Bound 1, ...)
Many thanks
fmd
Email Gateway (Aug 17 2022 at 14:43):From: Clément Hurlin <Clement.Hurlin@esial.uhp-nancy.fr>
Hi,
If you're "deconstructing" a term you can do that by writing a
push/pop stack where you store name of bounds variable :
When matching a Abs(x, T, P) term, x refers to the name of the
bound variable. You can then push_somewhere x, and when you later
encounter "bound 0", the name of your variable will be at the
corresponding position in your stack.
Is there a cleverer solution ?
Clément
Email Gateway (Aug 17 2022 at 14:43):From: Lawrence Paulson <lp15@cam.ac.uk>
This question only makes sense in the context of some term. In order
to have reached some context, you will have recursively passed
through various term constructors. If every time you pass through the
Abs constructor you "cons" the name to a list of strings, then
reversing that list gives you the names. They are of course comments
only, with no logical significance.
Larry Paulson
Last updated: May 03 2024 at 08:18 UTC