Re: [isabelle] Type as argument
On Fri, May 13, 2011 at 9:55 AM, Steve W <s.wong.731 at gmail.com> 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
> definition "f 0 (t::nat itself) = 0"
> instance ..
> I get an error on "0::int". It works if 0 is replaced by a free variable
> though. Why's that?
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and