Re: [isabelle] Type as argument






The problem is that the types don't match: You've specified in the

"fixes" clause that f should take an argument of type "'a itself", but

in the "defines" clause the argument has type "nat itself". Try the

following:



consts a :: nat



locale A1 =

fixes f :: "nat => 'a itself => bool"

defines "fs (t::'a itself) == (if s = a then True else False)"



Also note that you must use meta-equality (== or \) in the

defines clause, rather than ordinary object-equality (=).


Sure. But what if f is to be overloaded? Eg,

instantiation nat :: foo
begin
definition d1: "fs (t::nat itself) = (if s = a then True else False)"
instance ..
end

instantiation real :: foo
begin
definition d2: "fs (t::real itself) = (if s = a then False else True)"
instance ..
end

but with 'f' and the definitions inside a locale.

Thanks again
Steve




- Brian






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