Re: [isabelle-dev] Considered harmful: surj
> Yes I second that. It surely is a good idea to just use it only as a > input translation. See now 6af79184bef3. Florian > > - Johannes > > Am Samstag, den 02.07.2016, 21:08 +0200 schrieb Florian Haftmann: >> Hi all, >> >> since cf26dd7395e4, ‹surj f› is a mere abbreviation for ‹range f = >> UNIV›. This is a little bit unfortunate since an ordinary equation is >> just hidden in output that way, resulting in lots of casual >> confusion. I >> would suggest to turn ‹surj› into a mere input abbreviation, similar >> to >> ‹trivial_limit› which also covers an equality. This may also open the >> possibility to re-introduce ‹surj_on f A› as in input abbreviation >> for >> ‹range f = A›, which got abolished in cf26dd7395e4, leaving a strange >> assymmetry wrt. inj(_on), bij(_betw). >> >> Cheers, >> Florian >> >> ___ >> isabelle-dev mailing list >> isabelle-...@in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel >> le-dev > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Considered harmful: surj
Yes I second that. It surely is a good idea to just use it only as a input translation. - Johannes Am Samstag, den 02.07.2016, 21:08 +0200 schrieb Florian Haftmann: > Hi all, > > since cf26dd7395e4, ‹surj f› is a mere abbreviation for ‹range f = > UNIV›. This is a little bit unfortunate since an ordinary equation is > just hidden in output that way, resulting in lots of casual > confusion. I > would suggest to turn ‹surj› into a mere input abbreviation, similar > to > ‹trivial_limit› which also covers an equality. This may also open the > possibility to re-introduce ‹surj_on f A› as in input abbreviation > for > ‹range f = A›, which got abolished in cf26dd7395e4, leaving a strange > assymmetry wrt. inj(_on), bij(_betw). > > Cheers, > Florian > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel > le-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Considered harmful: surj
Hi all, since cf26dd7395e4, ‹surj f› is a mere abbreviation for ‹range f = UNIV›. This is a little bit unfortunate since an ordinary equation is just hidden in output that way, resulting in lots of casual confusion. I would suggest to turn ‹surj› into a mere input abbreviation, similar to ‹trivial_limit› which also covers an equality. This may also open the possibility to re-introduce ‹surj_on f A› as in input abbreviation for ‹range f = A›, which got abolished in cf26dd7395e4, leaving a strange assymmetry wrt. inj(_on), bij(_betw). Cheers, Florian -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_at_haftmann_online_de.pgp signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
