[isabelle] using mono predicate



Hello,

I have the following theory fragment:

theory test imports Main
begin

class test = lattice
begin

theorem test:
  "f x  = (x::'a) ==> mono f ==> f x = x"

When processing the theorem test I get the following error:

*** Type unification failed: Variable 'a::type not of sort order

The predicate mono is defined in class order and class lattice
extends the class order.

Best regards,

Viorel Preoteasa





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