Re: [isabelle] list of currently bound variables
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 ?
This archive was generated by a fusion of
Pipermail (Mailman edition) and