*To*: cl-isabelle-users at lists.cam.ac.uk, Gottfried Barrow <gottfried.barrow at gmx.com>*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 18:02:22 +0100*In-reply-to*: <52F8FDF0.6090304@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> <52F8DEE5.5020501@in.tum.de> <52F8FDF0.6090304@gmx.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.2.0

Am 10.02.2014 17:27, schrieb Gottfried Barrow:

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)"DmitriyThanks. It's fortunate I didn't switch the order, or in the future itcould have been, "I thought I remember that this worked."If Ondrej accommodates, the problem I show next won't be an issue, butbelow, I show how I can coerce to `rat`, but not to`'a::linordered_idom`.And thanks for the explanation. Guessing here, from what you said andwhat Ondrej said, the error below is because the coercion needs a typeconstructor, and `'a::linordered_idom` is only a type variable.

Are there such things as 0-ary type constructor variables, that I canput in place of `'a`? With `show_sorts`, I never see the type/sort of`nat` or `int`.

There is no such thing. Dmitriy

**Follow-Ups**:

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

**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: Re: [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: [isabelle] Prelim lifting & coercion done: 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