[isabelle] Defining operators in locale
Once again with operators, can they be defined inside a locale? E.g.,
locale A =
fixes approx :: "['a,'a] => bool" (infixl "~~" 50)
assumes "(f::real=>real) ~~ g"
fails type unification. But if I had
approx :: "['a,'a] => bool" (infixl "~~" 50)
then it goes through fine. It seems when it's defined inside a locale, the
type variables can't be instantiated, i.e. "'a" can't be instantiated to
"real" so it'd have to be "(f::'a) ~~ g". If so, why's that?
This archive was generated by a fusion of
Pipermail (Mailman edition) and