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



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 on your example, which only will not insert coercions in the first argument of equality (and of other polymorphic functions). It would have worked if you had reversed the equation:

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

Thanks. It's fortunate I didn't switch the order, or in the future it could have been, "I thought I remember that this worked."

If Ondrej accommodates, the problem I show next won't be an issue, but below, 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 and what Ondrej said, the error below is because the coercion needs a type constructor, and `'a::linordered_idom` is only a type variable.
Exactly. In principle this could be supported in the incomplete algorithm (2), but it isn't yet (and I will not promise anything ;-) ).


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

Dmitriy




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.