Thomas Sternagel
2016-09-30 10:20:15 UTC
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
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