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.
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
would allows us to work with sets in a more confortable way. ¿Does
know some work on that?
This archive was generated by a fusion of
Pipermail (Mailman edition) and