4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maedertype t

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maederop f : ? t -> t

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maederop g : t -> (? t)

75a6279dbae159d018ef812185416cf6df386c10Till Mossakowskiops a, b : t

f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maederops c, d : ? t

eca29a7be76eb73944ec19b06eda3d6a9e6e543dChristian Maeder. f a = g c

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder. def c ();

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder%% Type Constructors -----------------------------------------------------

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maedert : Type

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder%% Assumptions -----------------------------------------------------------

f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maedera : t %(op)%

f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maederb : t %(op)%

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederc : ? t %(op)%

f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maederd : ? t %(op)%

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maederf : ? t -> t %(op)%

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maederg : t -> ? t %(op)%

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder%% Sentences -------------------------------------------------------------

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maederf a = g c

23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maederdef c ()

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder%% Diagnostics -----------------------------------------------------------

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder### Hint 10.8, in type of '(op c : ? t)'

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder typename 't' (6.10)

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder is not unifiable with type 'Unit ->? ? _v12_a'

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder