Did we ever discuss the naming issue? "insert_mset" would be the canonical name, but it would make larger expressions hard to read.
Tobias On 26/07/2016 13:59, Mathias Fleury wrote:
Hello all, (Relaunching this nearly-one-and-a-half-years-old thread.) Before I start working on it, has anyone already done some work towards adding insert_mset? Thanks, MathiasOn 08 Apr 2015, at 11:12, Larry Paulson <l...@cam.ac.uk> wrote: Sounds logical to me. LarryOn 8 Apr 2015, at 08:13, Tobias Nipkow <nip...@in.tum.de> wrote: Currently the setup in Multiset is geared towards having the 3 basic (non-free) constructors: empty, singleton and union. Although induction already has only two cases (empty and union with singleton), it would be nicer to have only two constructors, like for finite sets: empty and insert. In particular, this often avoids the use of ac_simps for union because representations are more canonical. The singleton constructor would be retained as an abbreviation for "insert_mset _ {#}" but "M + {#x#}" would be simplified to "insert_mset x M", like for sets. Any views? Tobias _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
