Re: [isabelle] subtype definition in Isabelle
On Fri, 15 Jan 2016, 刘涛 wrote:
I am wondering if Isabelle supports subtype definition , something just
like subclass and superclass in C++.
If you look at the latest and greatest developments of the
"object-oriented" approach in Scala, namely "traits", they approximate an
idea of structured algebraic specifications from the good old times.
In Isabelle you can work in that style with "locales".
There is a particularly useful view on locales called "type classes".
This allows to work in the manner and style of Haskell (the classic
version of 1998, without recent additions).
And the subtype inherits the attributes of the parent-type.
If you mean plain record types with structural subtyping (in the sense of
Hindley-Milner polymorphism) then the HOL "record" package will do that.
But it is not as frequently used as one might think.
This archive was generated by a fusion of
Pipermail (Mailman edition) and