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:
Exactly. In principle this could be supported in the incomplete
algorithm (2), but it isn't yet (and I will not promise anything ;-) ).
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)"
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
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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and