*To*: s.wong.731 at gmail.com*Subject*: Re: [isabelle] Type as argument*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Fri, 20 May 2011 06:52:58 -0700*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <002354332f2ad4d43a04a3b4d786@google.com>*References*: <002354332f2ad4d43a04a3b4d786@google.com>*Sender*: huffman.brian.c at gmail.com

2011/5/20 <s.wong.731 at gmail.com>: >> 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 \) in the >> defines clause, rather than ordinary object-equality (=). > > Sure. But what if f is to be overloaded? E.g., > > instantiation nat :: foo > begin > definition d1: "f s (t::nat itself) = (if s = a then True else False)" > instance .. > end > > instantiation real :: foo > begin > definition d2: "f s (t::real itself) = (if s = a then False else True)" > instance .. > end > > but with 'f' and the definitions inside a locale. I am sorry, but this is not possible. Functions that are fixed by a "fixes" clause in a locale cannot be overloaded or polymorphic; they each must have a single, fixed type. (They may mention type variables like 'a, but this does not make them polymorphic -- such type variables are treated as fixed types within the locale context). A workaround may be possible, though: You can define "f" at the top level, making it polymorphic or overloaded. Then you can put assumptions about the definitions of "f" at various types inside a locale. For example: class foo = fixes f :: "nat => 'a itself => bool" consts a :: nat locale A = assumes "f s TYPE('a::foo) = (if s = a then True else False)" assumes "f s TYPE('b::foo) = (if s = a then False else True)" Later on, you could interpret locale A with type 'a instantiated as nat, and type 'b as real. - Brian

**Follow-Ups**:**Re: [isabelle] Type as argument***From:*s . wong . 731

**References**:**Re: [isabelle] Type as argument***From:*s . wong . 731

- Previous by Date: Re: [isabelle] Type as argument
- Next by Date: Re: [isabelle] unexpected behaviour of user defined command in jedit
- Previous by Thread: Re: [isabelle] Type as argument
- Next by Thread: Re: [isabelle] Type as argument
- Cl-isabelle-users May 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list