Re: [isabelle] Type as argument



2011/5/16 Steve W <s.wong.731 at gmail.com>:
> Thanks all. One more question: what is the "itself" keyword for in "'a
> itself"?

The "itself" is just a type constructor. It is like what you would get
from the following datatype declaration:

datatype 'a itself = Type (* one constructor with no arguments *)

The syntax "TYPE('a)" is an abbreviation for "Type :: 'a itself".

- Brian

>
> Thanks
> Steve
>
> 2011/5/13 René Thiemann <rene.thiemann at uibk.ac.at>
>
>> > 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?
>>
>> Because "definition" cannot be used with pattern matching on left-hand
>> sides.
>> Usually, one can use "fun" instead. However, even with "fun" you cannot
>> do pattern matching on "int" instead of "nat".
>>
>> However, you might write "f x (t:: nat itself) = (if x = (0 :: int) then 0
>> else ...)"
>>
>> René
>> --
>> René Thiemann                    mailto:rene.thiemann at uibk.ac.at
>> Computational Logic Group
>> http://cl-informatik.uibk.ac.at/~thiemann/
>> Institute of Computer Science    phone: +43 512 507-6434
>> University of Innsbruck
>>
>>
>





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