Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe HaskellNone

Agda.Interaction.Highlighting.Range

Description

Ranges.

Synopsis

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
 

rangeInvariant :: Range -> Bool

The Range invariant.

newtype Ranges

Zero or more consecutive and separated ranges.

Constructors

Ranges [Range] 

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.