var a : Type

type Flag a

ops mkf : Logical -> Flag a;

getl : Flag a -> Logical

vars x : Flag a; b : Logical

. mkf (getl x) = x

. getl (mkf b : Flag a) = b;

op sg : Flag a = mkf forall x, y : a . x = y;

op c : Logical = getl (sg : Flag a);

type

Flag : Type -> Type

var

a : Type %(var_1)%

op c : ? Unit

%[ =

\

. (op getl : forall a : Type . Flag a -> Logical)

((op sg : forall a : Type . Flag a) : Flag a)

as Unit ]%

op getl : forall a : Type . Flag a -> Logical

op mkf : forall a : Type . Logical -> Flag a

op sg : forall a : Type . Flag a

%[ =

(op mkf : forall a : Type . Logical -> Flag a)

forall x, y : a . (var x : a) = (var y : a) ]%

vars

b : Logical;

x : Flag a

forall a : Type; x : Flag a . mkf (getl x) = x

forall a : Type; b : Logical . getl (mkf b : Flag a) = b

forall a : Type . sg = mkf forall x, y : a . x = y

forall a : Type . c = (getl (sg : Flag a) as Unit)

1.6: ### Hint: is type variable 'a'

5.8: ### Hint: not a kind 'Flag a'

5.20: ### Hint: not a class 'Logical'

8.32: ### Hint: not a class 'a'

8.36: ### Hint: not a class 'a'

8.31: ### Hint: rebound variable 'x'