ModuleAgda-2.7.0.1Haskell2010

Agda.Interaction.Highlighting.Range

Ranges.

datadata Range

Character ranges. The first character in the file has position 1. Note that the to position is considered to be outside of the range.

Invariant: from <= to.

Instances6Eq, Ord, Show, NFData, Null, EmbPrj

Eq RangeDefined in Agda-2.7.0.1 · Agda.Interaction.Highlighting.Range
Ord RangeDefined in Agda-2.7.0.1 · Agda.Interaction.Highlighting.Range
Show RangeDefined in Agda-2.7.0.1 · Agda.Interaction.Highlighting.Range
NFData RangeDefined in Agda-2.7.0.1 · Agda.Interaction.Highlighting.Range
Null RangeDefined in Agda-2.7.0.1 · Agda.Interaction.Highlighting.Range
EmbPrj RangeDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Highlighting · orphan

valuerangeInvariant :: Range -> Bool

The Range invariant.

newtypenewtype Ranges

Zero or more consecutive and separated ranges.

Instances3Eq, Show, NFData

valuerangesInvariant :: Ranges -> Bool

The Ranges invariant.

valueoverlapping :: Range -> Range -> Bool

True iff the ranges overlap.

The ranges are assumed to be well-formed.

valueoverlappings :: Ranges -> Ranges -> Bool

methodempty :: a

valuerangeToPositions :: Range -> [Int]

Converts a range to a list of positions.

valuerangesToPositions :: Ranges -> [Int]

Converts several ranges to a list of positions.

valuerToR :: Range -> Ranges

Converts a Range to a Ranges.

valuerangeToRange :: Range -> Range

Converts a Range, seen as a continuous range, to a Range.

valueminus :: Ranges -> Ranges -> Ranges

minus xs ys computes the difference between xs and ys: the result contains those positions which are present in xs but not in ys.

Linear in the lengths of the input ranges.