Email Gateway (Aug 18 2022 at 16:52): Email Gateway (Aug 18 2022 at 16:52):From: Eg Gloor <egglue@gmail.com>
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!
Last updated: Apr 20 2024 at 01:05 UTC