Re: [isabelle] Type as argument

On Fri, May 13, 2011 at 9:55 AM, Steve W <s.wong.731 at> wrote:
> Thanks. If I change f to a binary function:
> class foo =
>  fixes f :: "int => 'a itself => int"
> and with the following instantiation:
> instantiation nat :: foo
> begin
>  definition "f 0 (t::nat itself) = 0"
>  instance ..
> end
> I get an error on "0::int". It works if 0 is replaced by a free variable
> though. Why's that?
> Thanks
> Steve

The "definition" command only allows a single equation with variables
for function arguments on the left-hand side. If you want to write
definitions with patterns and/or multiple equations, use "fun",
"function", "primrec", etc.

- Brian

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