09a5b34931
This PR adjusts the experimental module system to make `private` the default visibility modifier in `module`s, introducing `public` as a new modifier instead. `public section` can be used to revert the default for an entire section, though this is more intended to ease gradual adoption of the new semantics such as in `Init` (and soon `Std`) where they should be replaced by a future decl-by-decl re-review of visibilities.
46 lines
1.4 KiB
Text
46 lines
1.4 KiB
Text
/-
|
||
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Authors: Paul Reichert
|
||
-/
|
||
module
|
||
|
||
prelude
|
||
public import Init.Data.Range.Polymorphic.PRange
|
||
|
||
public section
|
||
|
||
/-!
|
||
# Slice notation
|
||
|
||
This module provides the means to obtain a slice from a collection and a range of indices via
|
||
slice notation.
|
||
-/
|
||
|
||
open Std PRange
|
||
|
||
namespace Std.Slice
|
||
|
||
/--
|
||
This typeclass indicates how to obtain slices of `α` of type `γ`, given ranges of shape `shape` in
|
||
the index type `β`.
|
||
-/
|
||
class Sliceable (shape : RangeShape) (α : Type u) (β : outParam (Type v))
|
||
(γ : outParam (Type w)) where
|
||
mkSlice (carrier : α) (range : PRange shape β) : γ
|
||
|
||
macro_rules
|
||
| `($c[*...*]) => `(Sliceable.mkSlice $c *...*)
|
||
| `($c[$a...*]) => `(Sliceable.mkSlice $c $a...*)
|
||
| `($c[$a<...*]) => `(Sliceable.mkSlice $c $a<...*)
|
||
| `($c[*...<$b]) => `(Sliceable.mkSlice $c *...<$b)
|
||
| `($c[$a...<$b]) => `(Sliceable.mkSlice $c $a...<$b)
|
||
| `($c[$a<...<$b]) => `(Sliceable.mkSlice $c $a<...<$b)
|
||
| `($c[*...$b]) => `(Sliceable.mkSlice $c *...<$b)
|
||
| `($c[$a...$b]) => `(Sliceable.mkSlice $c $a...<$b)
|
||
| `($c[$a<...$b]) => `(Sliceable.mkSlice $c $a<...<$b)
|
||
| `($c[*...=$b]) => `(Sliceable.mkSlice $c *...=$b)
|
||
| `($c[$a...=$b]) => `(Sliceable.mkSlice $c $a...=$b)
|
||
| `($c[$a<...=$b]) => `(Sliceable.mkSlice $c $a<...=$b)
|
||
|
||
end Std.Slice
|