[isabelle] pairs and friends



Dear mailing list,

In Isabelle/HOL development version 6703434c96d6 I have the following
problem: I want to have a friendly function 'foo' (which I reduced so
much, that it does not do anything useful anymore for sake of a minimal
example). If I use the type "a list â 'a stream â 'a stream" everything
works out as expected, but if I switch to streams of pairs, like shown
below I get the following error message:

Cannot have type variable "'a" in the argument types when it does not
occur in the result type

Now "'a" clearly appears in the result type, so I don't see what is
going wrong.

theory Foo
imports
  "~~/src/HOL/Library/Stream"
  "~~/src/HOL/Library/BNF_Corec"
begin
primcorec foo :: "'a list â
  ('a à 'a) stream â ('a à 'a) stream" where
  "foo us T = (case us of
    [] â SCons (shd T) (stl T)
  | u # us â SCons (shd T) (stl T))"

friend_of_corec foo :: "'a list â
  ('a à 'a) stream â ('a à 'a) stream" where
  "foo us T = (case us of
    [] â SCons (shd T) (stl T)
  | u # us â SCons (shd T) (stl T))"

end

Cheers,
Tom




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