<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Agda.Interaction.Highlighting.Range</title><link href="ocean.css" rel="stylesheet" type="text/css" title="Ocean" /><script src="haddock-util.js" type="text/javascript"></script><script type="text/javascript">//<![CDATA[
window.onload = function () {pageLoad();setSynopsis("mini_Agda-Interaction-Highlighting-Range.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-Interaction-Highlighting-Range.html">Source</a></li><li><a href="index.html">Contents</a></li><li><a href="doc-index.html">Index</a></li></ul><p class="caption">Agda-2.3.2.1: A dependently typed functional programming language and proof assistant</p></div><div id="content"><div id="module-header"><table class="info"><tr><th>Safe Haskell</th><td>None</td></tr></table><p class="caption">Agda.Interaction.Highlighting.Range</p></div><div id="description"><p class="caption">Description</p><div class="doc"><p>Ranges.
</p></div></div><div id="synopsis"><p id="control.syn" class="caption expander" onclick="toggleSection('syn')">Synopsis</p><ul id="section.syn" class="hide" onclick="toggleSection('syn')"><li class="src short"><span class="keyword">data</span> <a href="#t:Range">Range</a> = <a href="#v:Range">Range</a> {<ul class="subs"><li><a href="#v:from">from</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Integer">Integer</a></li><li><a href="#v:to">to</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Integer">Integer</a></li></ul>}</li><li class="src short"><a href="#v:rangeInvariant">rangeInvariant</a> :: <a href="Agda-Interaction-Highlighting-Range.html#t:Range">Range</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><span class="keyword">newtype</span> <a href="#t:Ranges">Ranges</a> = <a href="#v:Ranges">Ranges</a> [<a href="Agda-Interaction-Highlighting-Range.html#t:Range">Range</a>]</li><li class="src short"><a href="#v:rangesInvariant">rangesInvariant</a> :: <a href="Agda-Interaction-Highlighting-Range.html#t:Ranges">Ranges</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><a href="#v:overlapping">overlapping</a> :: <a href="Agda-Interaction-Highlighting-Range.html#t:Range">Range</a> -> <a href="Agda-Interaction-Highlighting-Range.html#t:Range">Range</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><a href="#v:empty">empty</a> :: <a href="Agda-Interaction-Highlighting-Range.html#t:Range">Range</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><a href="#v:rangeToPositions">rangeToPositions</a> :: <a href="Agda-Interaction-Highlighting-Range.html#t:Range">Range</a> -> [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Integer">Integer</a>]</li><li class="src short"><a href="#v:rangesToPositions">rangesToPositions</a> :: <a href="Agda-Interaction-Highlighting-Range.html#t:Ranges">Ranges</a> -> [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Integer">Integer</a>]</li><li class="src short"><a href="#v:rToR">rToR</a> :: <a href="Agda-Syntax-Position.html#t:Range">Range</a> -> <a href="Agda-Interaction-Highlighting-Range.html#t:Ranges">Ranges</a></li><li class="src short"><a href="#v:minus">minus</a> :: <a href="Agda-Interaction-Highlighting-Range.html#t:Ranges">Ranges</a> -> <a href="Agda-Interaction-Highlighting-Range.html#t:Ranges">Ranges</a> -> <a href="Agda-Interaction-Highlighting-Range.html#t:Ranges">Ranges</a></li><li class="src short"><a href="#v:tests">tests</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:IO">IO</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li></ul></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:Range" class="def">Range</a> <a href="src/Agda-Interaction-Highlighting-Range.html#Range" class="link">Source</a></p><div class="doc"><p>Character ranges. The first character in the file has position 1.
Note that the <code><a href="Agda-Interaction-Highlighting-Range.html#v:to">to</a></code> position is considered to be outside of the
range.
</p><p>Invariant: <code><code><a href="Agda-Interaction-Highlighting-Range.html#v:from">from</a></code> <code><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Ord.html#v:-60--61-"><=</a></code> <code><a href="Agda-Interaction-Highlighting-Range.html#v:to">to</a></code></code>.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Range" class="def">Range</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div class="subs fields"><p class="caption">Fields</p><dl><dt class="src"><a name="v:from" class="def">from</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Integer">Integer</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:to" class="def">to</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Integer">Integer</a></dt><dd class="doc empty"> </dd></dl><div class="clear"></div></div></td></tr></table></div><div class="subs instances"><p id="control.i:Range" class="caption collapser" onclick="toggleSection('i:Range')">Instances</p><div id="section.i:Range" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> <a href="Agda-Interaction-Highlighting-Range.html#t:Range">Range</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Ord.html#t:Ord">Ord</a> <a href="Agda-Interaction-Highlighting-Range.html#t:Range">Range</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-Interaction-Highlighting-Range.html#t:Range">Range</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Typeable-Internal.html#t:Typeable">Typeable</a> <a href="Agda-Interaction-Highlighting-Range.html#t:Range">Range</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/QuickCheck-2.5.1.1/Test-QuickCheck-Arbitrary.html#t:Arbitrary">Arbitrary</a> <a href="Agda-Interaction-Highlighting-Range.html#t:Range">Range</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/QuickCheck-2.5.1.1/Test-QuickCheck-Arbitrary.html#t:CoArbitrary">CoArbitrary</a> <a href="Agda-Interaction-Highlighting-Range.html#t:Range">Range</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Interaction-Highlighting-Range.html#t:Range">Range</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:rangeInvariant" class="def">rangeInvariant</a> :: <a href="Agda-Interaction-Highlighting-Range.html#t:Range">Range</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-Interaction-Highlighting-Range.html#rangeInvariant" class="link">Source</a></p><div class="doc"><p>The <code><a href="Agda-Interaction-Highlighting-Range.html#t:Range">Range</a></code> invariant.
</p></div></div><div class="top"><p class="src"><span class="keyword">newtype</span> <a name="t:Ranges" class="def">Ranges</a> <a href="src/Agda-Interaction-Highlighting-Range.html#Ranges" class="link">Source</a></p><div class="doc"><p>Zero or more consecutive and separated ranges.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Ranges" class="def">Ranges</a> [<a href="Agda-Interaction-Highlighting-Range.html#t:Range">Range</a>]</td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:Ranges" class="caption collapser" onclick="toggleSection('i:Ranges')">Instances</p><div id="section.i:Ranges" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> <a href="Agda-Interaction-Highlighting-Range.html#t:Ranges">Ranges</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-Interaction-Highlighting-Range.html#t:Ranges">Ranges</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/QuickCheck-2.5.1.1/Test-QuickCheck-Arbitrary.html#t:Arbitrary">Arbitrary</a> <a href="Agda-Interaction-Highlighting-Range.html#t:Ranges">Ranges</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:rangesInvariant" class="def">rangesInvariant</a> :: <a href="Agda-Interaction-Highlighting-Range.html#t:Ranges">Ranges</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-Interaction-Highlighting-Range.html#rangesInvariant" class="link">Source</a></p><div class="doc"><p>The <code><a href="Agda-Interaction-Highlighting-Range.html#t:Ranges">Ranges</a></code> invariant.
</p></div></div><div class="top"><p class="src"><a name="v:overlapping" class="def">overlapping</a> :: <a href="Agda-Interaction-Highlighting-Range.html#t:Range">Range</a> -> <a href="Agda-Interaction-Highlighting-Range.html#t:Range">Range</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-Interaction-Highlighting-Range.html#overlapping" class="link">Source</a></p><div class="doc"><p><code><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#v:True">True</a></code> iff the ranges overlap.
</p><p>The ranges are assumed to be well-formed.
</p></div></div><div class="top"><p class="src"><a name="v:empty" class="def">empty</a> :: <a href="Agda-Interaction-Highlighting-Range.html#t:Range">Range</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-Interaction-Highlighting-Range.html#empty" class="link">Source</a></p><div class="doc"><p><code><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#v:True">True</a></code> iff the range is empty.
</p></div></div><div class="top"><p class="src"><a name="v:rangeToPositions" class="def">rangeToPositions</a> :: <a href="Agda-Interaction-Highlighting-Range.html#t:Range">Range</a> -> [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Integer">Integer</a>]<a href="src/Agda-Interaction-Highlighting-Range.html#rangeToPositions" class="link">Source</a></p><div class="doc"><p>Converts a range to a list of positions.
</p></div></div><div class="top"><p class="src"><a name="v:rangesToPositions" class="def">rangesToPositions</a> :: <a href="Agda-Interaction-Highlighting-Range.html#t:Ranges">Ranges</a> -> [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Integer">Integer</a>]<a href="src/Agda-Interaction-Highlighting-Range.html#rangesToPositions" class="link">Source</a></p><div class="doc"><p>Converts several ranges to a list of positions.
</p></div></div><div class="top"><p class="src"><a name="v:rToR" class="def">rToR</a> :: <a href="Agda-Syntax-Position.html#t:Range">Range</a> -> <a href="Agda-Interaction-Highlighting-Range.html#t:Ranges">Ranges</a><a href="src/Agda-Interaction-Highlighting-Range.html#rToR" class="link">Source</a></p><div class="doc"><p>Converts a <code><a href="Agda-Syntax-Position.html#t:Range">Range</a></code> to a <code><a href="Agda-Interaction-Highlighting-Range.html#t:Ranges">Ranges</a></code>.
</p></div></div><div class="top"><p class="src"><a name="v:minus" class="def">minus</a> :: <a href="Agda-Interaction-Highlighting-Range.html#t:Ranges">Ranges</a> -> <a href="Agda-Interaction-Highlighting-Range.html#t:Ranges">Ranges</a> -> <a href="Agda-Interaction-Highlighting-Range.html#t:Ranges">Ranges</a><a href="src/Agda-Interaction-Highlighting-Range.html#minus" class="link">Source</a></p><div class="doc"><p><code>minus xs ys</code> computes the difference between <code>xs</code> and <code>ys</code>: the
result contains those positions which are present in <code>xs</code> but not
in <code>ys</code>.
</p><p>Linear in the lengths of the input ranges.
</p></div></div><div class="top"><p class="src"><a name="v:tests" class="def">tests</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:IO">IO</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-Interaction-Highlighting-Range.html#tests" class="link">Source</a></p><div class="doc"><p>All the properties.
</p></div></div></div></div><div id="footer"><p>Produced by <a href="http://www.haskell.org/haddock/">Haddock</a> version 2.11.0</p></div></body></html>
