Re: [isabelle] malformed dependency

> The last definition produces this error:
>  Malformed dependency of constant Eq(obj ^ obj ^ 'a) -> Eq(obj ^ 'a)
>  *** (restriction Eq(obj ^ obj ^ 'a) from "PM.EqX_frmN_def")
>  *** The error(s) above occurred in definition "EqX_frmN_def":
>  ***   "F = G : ALL x. (ly. F y x) = (ly. G y x)"
>  *** At command "defs".
> From this, I conclude that Isabelle does not understand that my
> definition is well defined, i.e. that the type "obj => obj => 'a"
> is "smaller", in some sense, than "obj => 'a".

Isabelle's check for non-circularity of overloaded definitions restricts
checked overloaded definitions to overloading patterns similiar to what
is possible in Haskell 1.0; if this is not enough and you trust your
definitions not to introduce inconsistencies (by a suitable meta-proof),
you may turn the check of by writing

defs (unchecked)

instead of

defs (overloaded)

fn:Florian Haftmann
org;quoted-printable;quoted-printable:Technische Universit=C3=A4t M=C3=BCnchen ;Institut f=C3=BCr Informatik, Lehrstuhl Software and Systems Engineering
adr;quoted-printable;quoted-printable:;;Boltzmannstra=C3=9Fe 3;M=C3=BCnchen;Bayern;85748;Deutschland
email;internet:florian.haftmann at
title:M. Sc.
tel;work:(++49 89) 289 - 17300
note;quoted-printable:PGP available: =

Attachment: signature.asc
Description: OpenPGP digital signature

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