*To*: Dmitriy Traytel <traytel at in.tum.de>*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 10:27:28 -0600*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <52F8DEE5.5020501@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> <52F8D659.6050107@gmx.com> <52F8DEE5.5020501@in.tum.de>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 2/10/2014 8:15 AM, Dmitriy Traytel wrote:

This is out of scope for (1). The incompleteness of (2) is visible onyour example, which only will not insert coercions in the firstargument of equality (and of other polymorphic functions). It wouldhave worked if you had reversed the equation:term " Some (y::rat) = (x::rat loidOpt)"

Dmitriy

(*source with error*)

by(auto) declare [[coercion Rep_loidOpt]] definition the_Rep_loidOpt :: "'a::linordered_idom loidOpt => 'a" where "the_Rep_loidOpt x = the(Rep_loidOpt x)" declare [[coercion "the_Rep_loidOpt::rat loidOpt => rat"]] term "(y::rat) = (x::rat loidOpt)" declare [[coercion the_Rep_loidOpt]] (* Bad type for a coercion: the_Rep_loidOpt :: ?'a::linordered_idom loidOpt => ?'a::linordered_idom *) Thanks again, GB

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

**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:*Dmitriy Traytel

- Previous by Date: Re: [isabelle] Two configuration questions
- 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