[isabelle-dev] ML equality types

[Lars Hupel]

I use those frequently as a curried version of 'op =', e.g. 'filter (equal "..." o fst) ...'.

Lars

Le 10 septembre 2015 12:31:14 GMT+02:00, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> a écrit :
>In src/Pure/library.ML, the signature still contains the discouraged
>and
>nowadays rarely used entries
>	
>	val equal: ''a -> ''a -> bool
>	val not_equal:  ''a -> ''a -> bool
>
>Shall we attempt to get rid of them finally?
>
>	Florian
>
>-- 
>
>PGP available:
>http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>
>
>
>------------------------------------------------------------------------
>
>_______________________________________________
>isabelle-dev mailing list
>isabelle-dev at in.tum.de
>https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150910/39de4d52/attachment-0002.html>