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


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.


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

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