Re: [isabelle] Uses of type quantification
Last autumn I came across examples that would have been improved by
some kind of type quantification in HOL.
Problems arise in relating two polymorphic properties:
(1) (all 'a. !!(x::'a). P x) ==> all 'a. !!(x::'a). Q x
cannot be stated in HOL. Perhaps the reason this isn't seen as a
common problem is that (1) can often be restated as
(2) all 'a. (!!(x::'a). P x) ==> !!(x::'a). Q x
However, in a locale with assumption (!!(x::'a). P x) one might expect
to use the assumption at more than one type.
This archive was generated by a fusion of
Pipermail (Mailman edition) and