[isabelle-dev] ML equality types
makarius at sketis.net
Thu Sep 10 17:27:11 CEST 2015
On Thu, 10 Sep 2015, Florian Haftmann wrote:
> 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
These operations are a bit old-fashioned, but why are they discouraged?
As far as I know, David Matthews is doing a dictionary construction
internally (for some years already). So it is just a minimal form of
Haskell-style type-class discipline.
More information about the isabelle-dev