Re: [isabelle] list of currently bound variables



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


On 27 Apr 2006, at 14:19, F. Miguel Dionisio wrote:

Does anyone know how to acess to the list of currently bound variables (namely to know the names of Bound 0, Bound 1, ...)






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.