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 MHonArc.