Feature Request: Index with ranges

Stream: lean4

[Henrik Böving]

Is there a reason that given r : Std.Range and xs : Array Expr or List Expr we do not support xs[r] because there is no GetElem instance for this configuration? It could even be constructed automatically from instances of GetElem for the beginning and end of r.

[Mario Carneiro]

the syntax for that would be a bit off, xs[[1:5]]

[Mario Carneiro]

also, what would it return?

[Mario Carneiro]

I think the syntax arr[i:j] currently returns a Subarray

[Henrik Böving]

Sounds to me like it would be reasonable to return a subarray as well then?

[Henrik Böving]

Oh and to make clear why I'm asking, when there is an Std.Range stored in some datastructure you actually have this case of r : Std.Range instead of the arr[i:j] syntax so I'm mostly asking for this case, I see the argument against it though.

[Sebastian Ullrich]

Ah, I wanted to create an RFC about this at some point, but here is the gist: as Mario said, the current range syntax would look a bit weird inside indexing syntax, but also it's a bit weird for range syntax in itself. If we switched to a more common notation like i..j (or i..<j for explicitness, and then i..=j for inclusive ranges), using ranges as indices would become very natural.