Re: [isabelle] Type as argument



2011/5/17  <s.wong.731 at gmail.com>:
> With the example, would it be possible to let f be a parameter of a locale
> instead, ie
>
> locale A1 =
> fixes f :: "nat => 'a itself => bool"
> defines "fs (t::nat itself) = (if s = a then True else False)"
>
> complains about the operand "t::nat itself". Is it asking for "nat" to be a
> parameter?

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 "f s (t::'a itself) == (if s = a then True else False)"

Also note that you must use meta-equality (== or \<equiv>) in the
defines clause, rather than ordinary object-equality (=).

- Brian





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