Re: [isabelle] Turning intervals into lists: upt and upto

Define yes, but we'd still need it to be a typeclass argument because we
also need implementations of it. "Least" is not executable.

"countable + linorder" is not enough though because e.g. "enat" does not
work. [0..∞] is not a finite list. You could define "succ", but not
"pred". (So on the dual of "enat" you could not define "succ").


On 16/07/2021 11:22, Peter Lammich wrote:
> Hi,
> shouldn't linearly ordered and countable be enough to define the succ
> operation, e.g. as succ x = LEAST y. x<y.
> One could leave succ undefined if there is no successor.
> --
>   Peter
> On Fri, 2021-07-16 at 10:57 +0200, Manuel Eberl wrote:
>> I just stumbled across this while talking to Katharina Kreuzer.
>> Currently, we have two notions of making a list from an interval of
>> numbers:
>> [a..b], which desugars to "upto a b" with "upto :: int => int => int"
>> [a..<b], which desugars to "upt a b" with "upt :: nat => nat => nat"
>> Clearly, this is confusing and I suspect that it is a historic
>> accident.
>> I think we should clean this up.
>> What one would like to have, in my opinion, is four notations [a..b],
>> [a<..b], [a..<b], [a<..<b] to mirror the same notation on sets.
>> The question is: how do we implement this properly? Haskell does it
>> with
>> an "Enum" type class that has "succ"/"pred" operations. A "succ"
>> would
>> be enough for us, but to implement the above operations one would
>> additionally need to assume that {a..b} is finite for any a, b. And,
>> in
>> the specification of `succ`, one would have to figure out what to do
>> if
>> there is no successor (e.g. in finite types).
>> Any ideas/comments?
>> Manuel

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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