[isabelle-dev] Considered harmful: surj

[Johannes Hölzl]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev