Email Gateway (Aug 18 2022 at 11:39): Email Gateway (Aug 18 2022 at 11:39):From: Denis Bueno <dbueno@gmail.com>
Removing the type annotation fixed my problem, thanks.
Is the cause one of impredicative instantiation? Is that what you
mean by "once you write down a type variable in a fix, it really is
fixed"?
--
Denis
--
Denis
Email Gateway (Aug 18 2022 at 11:48):From: Denis Bueno <dbueno@gmail.com>
In the attached proof script, I receive the following message after
loading the buffer into Isabelle:
*** Type unification failed
*** Type error in application: Incompatible operand type
*** Operator: Cl_P :: 'a set => 'a set
*** Operand: T :: ??'a llist set
*** At command "assume".
I expect these types to be unifiable. Should not "??'a llist set"
unify with "'a set" such that "??'a llist = 'a"?
I'm attempting to use a set of functions out of which I'm going to
pick an arbitrary function and invoke the only property I know about
it (namely, that it's monotonic; see the definition Cls). What have I
done wrong?
The proof script depends on the LList2 library, available on AFP
(http://afp.sourceforge.net/entries/Lazy-Lists-II.shtml).
Error.thy
Email Gateway (Aug 18 2022 at 11:49):From: Tobias Nipkow <nipkow@in.tum.de>
The problem was that you did something like this:
fix x :: 'a set
assume "x = {{}}"
where x should really be of type 'a set set. But when you write down a
type variable in a fix, it really is fixed. Hence the type unification
error. Solution for fix/assume: either no types at all (in which case
type inference solves the problem in most cases) or full types.
Regards
Tobias
Denis Bueno schrieb:
Last updated: May 03 2024 at 12:27 UTC