Re: [isabelle] parser translation for sets



This is an interesting idea, but it is non-trivial. The syntactic treatment of sequents is designed to allow expressions like G, ~A, H that represent a sequence of formulas containing ~A somewhere. It relies on an encoding of associative unification in higher-order unification. It allows sequent calculus rules to be written naturally.

It's not immediately clear to me how this could be added to the current syntax for sets or what examples would benefit from it.

Larry Paulson


On 1 Feb 2007, at 15:41, Paqui Lucio wrote:

I wonder if there exists "a parser/print translation" for sets (from
HOL/set.thy) similar to the existing one for sequences in Sequents.thy. This would allows us to work with sets in a more confortable way. ¿Does somebody
know some work on that?






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