Re: [isabelle] Bizarre type unification error



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:
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).






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