*To*: 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*: Gottfried Barrow <igbi at gmx.com>*Date*: Mon, 10 Feb 2014 07:38:33 -0600*In-reply-to*: <52F803E9.2010005@in.tum.de>*References*: <52F68FD1.3060307@gmx.com> <52F695E2.7080602@gmx.com> <52F6CB1A.7060500@gmx.com> <52F7ACAC.6040100@gmx.com> <52F803E9.2010005@in.tum.de>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

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 shown below.

by(auto)

(* declare [[coercion Rep_loidOpt]] declare [[coercion "Rep_loidOpt::rat loidOpt => rat option"]] term "(x::rat loidOpt) = Some (y::rat)" *) (*Going the Abs direction works, but it's not the subtyping I need.*) declare [[coercion Abs_loidOpt]] term "(x::rat loidOpt) = Some (y::rat)" term "(x::'a::linordered_idom loidOpt) = Some (y::'a::linordered_idom)" (*I tried messing with coercion_map, but it didn't help.*)

"MAPloidOpt f q = Abs_loidOpt(Some(f (the(Rep_loidOpt q))))" declare [[coercion_map MAPloidOpt]]

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

**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

- Previous by Date: [isabelle] type variable and locales extension
- Next by Date: Re: [isabelle] Want a type of non-negatives for a field, to work like nat/int
- 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