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

Safe HaskellNone
LanguageHaskell98

Agda.Interaction.Highlighting.Range

Description

Ranges.

Synopsis

Documentation

data Range Source

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 :: Int
 
to :: Int
 

rangeInvariant :: Range -> Bool Source

The Range invariant.

newtype Ranges Source

Zero or more consecutive and separated ranges.

Constructors

Ranges [Range] 

overlapping :: Range -> Range -> Bool Source

True iff the ranges overlap.

The ranges are assumed to be well-formed.

empty :: Range -> Bool Source

True iff the range is empty.

rangeToPositions :: Range -> [Int] Source

Converts a range to a list of positions.

rangesToPositions :: Ranges -> [Int] Source

Converts several ranges to a list of positions.

rToR :: Range -> Ranges Source

Converts a Range to a Ranges.

minus :: Ranges -> Ranges -> Ranges Source

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 Source

All the properties.