*To*: Gottfried Barrow <igbi at gmx.com>, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Want a type of non-negatives for a field, to work like nat/int*From*: Dmitriy Traytel <traytel at in.tum.de>*Date*: Mon, 10 Feb 2014 15:15:01 +0100*In-reply-to*: <52F8D659.6050107@gmx.com>*References*: <52F68FD1.3060307@gmx.com> <52F695E2.7080602@gmx.com> <52F6CB1A.7060500@gmx.com> <52F7ACAC.6040100@gmx.com> <52F803E9.2010005@in.tum.de> <52F8D659.6050107@gmx.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.2.0

Am 10.02.2014 14:38, schrieb Gottfried Barrow:

On 2/9/2014 4:40 PM, Ondřej Kunčar wrote:On 02/09/2014 05:28 PM, Gottfried Barrow wrote:(*NOTE: The "exception TYPE raised" error shown below might be of interest to someone.)For example me. Your type definition uses as a raw type a typevariable. The new code in lifting that deals with parametricityassumes that the raw type is always a type constructor. I'll take alook at it.Ondrej,Thanks. I use `'a::linordered_idom option` as a workaround, as shownbelow.NOTE for anyone: I can't get subtype coercion in the Rep direction, asshow below. If someone can tell me whether I can or can't do that, I'dappreciate it.

Hi Gottfried, there are two different algorithms in charge of inserting coercions:

typedef ('a::linordered_idom) loidOpt = "{x::'a option. x ~= None &the x >= 0}"by(auto)(* The Rep declares don't return an error, but have no affect oncoercions. *)(* declare [[coercion Rep_loidOpt]] declare [[coercion "Rep_loidOpt::rat loidOpt => rat option"]] term "(x::rat loidOpt) = Some (y::rat)" *)

term " Some (y::rat) = (x::rat loidOpt)" Dmitriy

**Follow-Ups**:**Re: [isabelle] Want a type of non-negatives for a field, to work like nat/int***From:*Gottfried Barrow

**References**:**[isabelle] Want a type of non-negatives for a field, to work like nat/int***From:*Gottfried Barrow

**Re: [isabelle] Want a type of non-negatives for a field, to work like nat/int***From:*Gottfried Barrow

**Re: [isabelle] Want a type of non-negatives for a field, to work like nat/int***From:*Gottfried Barrow

**Re: [isabelle] Want a type of non-negatives for a field, to work like nat/int***From:*Gottfried Barrow

**Re: [isabelle] Want a type of non-negatives for a field, to work like nat/int***From:*Ondřej Kunčar

**Re: [isabelle] Want a type of non-negatives for a field, to work like nat/int***From:*Gottfried Barrow

- Previous by Date: Re: [isabelle] Want a type of non-negatives for a field, to work like nat/int
- Next by Date: [isabelle] Two configuration questions
- Previous by Thread: Re: [isabelle] Want a type of non-negatives for a field, to work like nat/int
- Next by Thread: Re: [isabelle] Want a type of non-negatives for a field, to work like nat/int
- Cl-isabelle-users February 2014 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