Agda.Interaction.Highlighting.Range

Ranges.

Documentation

data 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.

Constructors

Range

Fields

from :: Integer

to :: Integer

Instances

Eq Range

Ord Range

Show Range

Typeable Range

Arbitrary Range

CoArbitrary Range

EmbPrj Range

rangeInvariant :: Range -> Bool

The Range invariant.

newtype Ranges

Zero or more consecutive and separated ranges.

Constructors

Ranges [Range]

Instances

Eq Ranges

Show Ranges

Arbitrary Ranges

rangesInvariant :: Ranges -> Bool

The Ranges invariant.

overlapping :: Range -> Range -> Bool

True iff the ranges overlap.

The ranges are assumed to be well-formed.

empty :: Range -> Bool

True iff the range is empty.

rangeToPositions :: Range -> [Integer]

Converts a range to a list of positions.

rangesToPositions :: Ranges -> [Integer]

Converts several ranges to a list of positions.

rToR :: Range -> Ranges

Converts a Range to a Ranges.

minus :: 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.

tests :: IO Bool

All the properties.