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






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.




from :: Integer
to :: Integer

rangeInvariant :: Range -> BoolSource

The Range invariant.

overlapping :: Range -> Range -> BoolSource

True iff the ranges overlap.

The ranges are assumed to be well-formed.

toList :: Range -> [Integer]Source

Converts a range to a list of positions.

getRanges :: Name -> ([Range], Bool)Source

Calculates a set of ranges associated with a name.

For an operator the ranges associated with the NameParts are returned. Otherwise the range associated with the Name is returned.

A boolean, indicating operatorness, is also returned.

getRangesA :: QName -> ([Range], Bool)Source

Like getRanges, but for QNames. Note that the module part of the name is thrown away; only the base part is used.

rToR :: Range -> [Range]Source

Converts a Range to a list of Ranges.

tests :: IO BoolSource

All the properties.