[isabelle] Defining operators in locale



Hi again,

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

consts
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?

Thanks again!




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.