taggy-0.1.4: html_files/agda.html
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml"
><head
><title
>index</title
><meta http-equiv="Content-Type" content="text/html; charset=UTF-8"
/><meta http-equiv="Content-Style-Type" content="text/css"
/><link href="Agda.css" rel="stylesheet" type="text/css"
/></head
><body
><pre
><a name="1" class="Keyword"
>module</a
><a name="7"
> </a
><a name="8" href="index.html#1" class="Module"
>index</a
><a name="13"
> </a
><a name="14" class="Keyword"
>where</a
><a name="19"
>
</a
><a name="21" class="Comment"
>-- You probably want to start with this module:</a
><a name="68"
>
</a
><a name="69" class="Keyword"
>import</a
><a name="75"
> </a
><a name="76" href="README.html#1" class="Module"
>README</a
><a name="82"
>
</a
><a name="84" class="Comment"
>-- For a brief presentation of every single module, head over to</a
><a name="148"
>
</a
><a name="149" class="Keyword"
>import</a
><a name="155"
> </a
><a name="156" href="Everything.html#1" class="Module"
>Everything</a
><a name="166"
>
</a
><a name="168" class="Comment"
>-- Otherwise, here is an exhaustive, stern list of all the available modules:</a
><a name="245"
>
</a
><a name="246" class="Keyword"
>import</a
><a name="252"
> </a
><a name="253" href="Algebra.html#1" class="Module"
>Algebra</a
><a name="260"
>
</a
><a name="261" class="Keyword"
>import</a
><a name="267"
> </a
><a name="268" href="Algebra.FunctionProperties.html#1" class="Module"
>Algebra.FunctionProperties</a
><a name="294"
>
</a
><a name="295" class="Keyword"
>import</a
><a name="301"
> </a
><a name="302" href="Algebra.FunctionProperties.Core.html#1" class="Module"
>Algebra.FunctionProperties.Core</a
><a name="333"
>
</a
><a name="334" class="Keyword"
>import</a
><a name="340"
> </a
><a name="341" href="Algebra.Monoid-solver.html#1" class="Module"
>Algebra.Monoid-solver</a
><a name="362"
>
</a
><a name="363" class="Keyword"
>import</a
><a name="369"
> </a
><a name="370" href="Algebra.Morphism.html#1" class="Module"
>Algebra.Morphism</a
><a name="386"
>
</a
><a name="387" class="Keyword"
>import</a
><a name="393"
> </a
><a name="394" href="Algebra.Operations.html#1" class="Module"
>Algebra.Operations</a
><a name="412"
>
</a
><a name="413" class="Keyword"
>import</a
><a name="419"
> </a
><a name="420" href="Algebra.Properties.AbelianGroup.html#1" class="Module"
>Algebra.Properties.AbelianGroup</a
><a name="451"
>
</a
><a name="452" class="Keyword"
>import</a
><a name="458"
> </a
><a name="459" href="Algebra.Properties.BooleanAlgebra.html#1" class="Module"
>Algebra.Properties.BooleanAlgebra</a
><a name="492"
>
</a
><a name="493" class="Keyword"
>import</a
><a name="499"
> </a
><a name="500" href="Algebra.Properties.BooleanAlgebra.Expression.html#1" class="Module"
>Algebra.Properties.BooleanAlgebra.Expression</a
><a name="544"
>
</a
><a name="545" class="Keyword"
>import</a
><a name="551"
> </a
><a name="552" href="Algebra.Properties.DistributiveLattice.html#1" class="Module"
>Algebra.Properties.DistributiveLattice</a
><a name="590"
>
</a
><a name="591" class="Keyword"
>import</a
><a name="597"
> </a
><a name="598" href="Algebra.Properties.Group.html#1" class="Module"
>Algebra.Properties.Group</a
><a name="622"
>
</a
><a name="623" class="Keyword"
>import</a
><a name="629"
> </a
><a name="630" href="Algebra.Properties.Lattice.html#1" class="Module"
>Algebra.Properties.Lattice</a
><a name="656"
>
</a
><a name="657" class="Keyword"
>import</a
><a name="663"
> </a
><a name="664" href="Algebra.Properties.Ring.html#1" class="Module"
>Algebra.Properties.Ring</a
><a name="687"
>
</a
><a name="688" class="Keyword"
>import</a
><a name="694"
> </a
><a name="695" href="Algebra.RingSolver.html#1" class="Module"
>Algebra.RingSolver</a
><a name="713"
>
</a
><a name="714" class="Keyword"
>import</a
><a name="720"
> </a
><a name="721" href="Algebra.RingSolver.AlmostCommutativeRing.html#1" class="Module"
>Algebra.RingSolver.AlmostCommutativeRing</a
><a name="761"
>
</a
><a name="762" class="Keyword"
>import</a
><a name="768"
> </a
><a name="769" href="Algebra.RingSolver.Lemmas.html#1" class="Module"
>Algebra.RingSolver.Lemmas</a
><a name="794"
>
</a
><a name="795" class="Keyword"
>import</a
><a name="801"
> </a
><a name="802" href="Algebra.RingSolver.Natural-coefficients.html#1" class="Module"
>Algebra.RingSolver.Natural-coefficients</a
><a name="841"
>
</a
><a name="842" class="Keyword"
>import</a
><a name="848"
> </a
><a name="849" href="Algebra.RingSolver.Simple.html#1" class="Module"
>Algebra.RingSolver.Simple</a
><a name="874"
>
</a
><a name="875" class="Keyword"
>import</a
><a name="881"
> </a
><a name="882" href="Algebra.Structures.html#1" class="Module"
>Algebra.Structures</a
><a name="900"
>
</a
><a name="901" class="Keyword"
>import</a
><a name="907"
> </a
><a name="908" href="Category.Applicative.html#1" class="Module"
>Category.Applicative</a
><a name="928"
>
</a
><a name="929" class="Keyword"
>import</a
><a name="935"
> </a
><a name="936" href="Category.Applicative.Indexed.html#1" class="Module"
>Category.Applicative.Indexed</a
><a name="964"
>
</a
><a name="965" class="Keyword"
>import</a
><a name="971"
> </a
><a name="972" href="Category.Applicative.Predicate.html#1" class="Module"
>Category.Applicative.Predicate</a
><a name="1002"
>
</a
><a name="1003" class="Keyword"
>import</a
><a name="1009"
> </a
><a name="1010" href="Category.Functor.html#1" class="Module"
>Category.Functor</a
><a name="1026"
>
</a
><a name="1027" class="Keyword"
>import</a
><a name="1033"
> </a
><a name="1034" href="Category.Functor.Predicate.html#1" class="Module"
>Category.Functor.Predicate</a
><a name="1060"
>
</a
><a name="1061" class="Keyword"
>import</a
><a name="1067"
> </a
><a name="1068" href="Category.Monad.html#1" class="Module"
>Category.Monad</a
><a name="1082"
>
</a
><a name="1083" class="Keyword"
>import</a
><a name="1089"
> </a
><a name="1090" href="Category.Monad.Continuation.html#1" class="Module"
>Category.Monad.Continuation</a
><a name="1117"
>
</a
><a name="1118" class="Keyword"
>import</a
><a name="1124"
> </a
><a name="1125" href="Category.Monad.Identity.html#1" class="Module"
>Category.Monad.Identity</a
><a name="1148"
>
</a
><a name="1149" class="Keyword"
>import</a
><a name="1155"
> </a
><a name="1156" href="Category.Monad.Indexed.html#1" class="Module"
>Category.Monad.Indexed</a
><a name="1178"
>
</a
><a name="1179" class="Keyword"
>import</a
><a name="1185"
> </a
><a name="1186" href="Category.Monad.Partiality.html#1" class="Module"
>Category.Monad.Partiality</a
><a name="1211"
>
</a
><a name="1212" class="Keyword"
>import</a
><a name="1218"
> </a
><a name="1219" href="Category.Monad.Partiality.All.html#1" class="Module"
>Category.Monad.Partiality.All</a
><a name="1248"
>
</a
><a name="1249" class="Keyword"
>import</a
><a name="1255"
> </a
><a name="1256" href="Category.Monad.Predicate.html#1" class="Module"
>Category.Monad.Predicate</a
><a name="1280"
>
</a
><a name="1281" class="Keyword"
>import</a
><a name="1287"
> </a
><a name="1288" href="Category.Monad.State.html#1" class="Module"
>Category.Monad.State</a
><a name="1308"
>
</a
><a name="1309" class="Keyword"
>import</a
><a name="1315"
> </a
><a name="1316" href="Coinduction.html#1" class="Module"
>Coinduction</a
><a name="1327"
>
</a
><a name="1328" class="Keyword"
>import</a
><a name="1334"
> </a
><a name="1335" href="Data.AVL.html#1" class="Module"
>Data.AVL</a
><a name="1343"
>
</a
><a name="1344" class="Keyword"
>import</a
><a name="1350"
> </a
><a name="1351" href="Data.AVL.IndexedMap.html#1" class="Module"
>Data.AVL.IndexedMap</a
><a name="1370"
>
</a
><a name="1371" class="Keyword"
>import</a
><a name="1377"
> </a
><a name="1378" href="Data.AVL.Sets.html#1" class="Module"
>Data.AVL.Sets</a
><a name="1391"
>
</a
><a name="1392" class="Keyword"
>import</a
><a name="1398"
> </a
><a name="1399" href="Data.Bin.html#1" class="Module"
>Data.Bin</a
><a name="1407"
>
</a
><a name="1408" class="Keyword"
>import</a
><a name="1414"
> </a
><a name="1415" href="Data.Bool.html#1" class="Module"
>Data.Bool</a
><a name="1424"
>
</a
><a name="1425" class="Keyword"
>import</a
><a name="1431"
> </a
><a name="1432" href="Data.Bool.Base.html#1" class="Module"
>Data.Bool.Base</a
><a name="1446"
>
</a
><a name="1447" class="Keyword"
>import</a
><a name="1453"
> </a
><a name="1454" href="Data.Bool.Properties.html#1" class="Module"
>Data.Bool.Properties</a
><a name="1474"
>
</a
><a name="1475" class="Keyword"
>import</a
><a name="1481"
> </a
><a name="1482" href="Data.Bool.Show.html#1" class="Module"
>Data.Bool.Show</a
><a name="1496"
>
</a
><a name="1497" class="Keyword"
>import</a
><a name="1503"
> </a
><a name="1504" href="Data.BoundedVec.html#1" class="Module"
>Data.BoundedVec</a
><a name="1519"
>
</a
><a name="1520" class="Keyword"
>import</a
><a name="1526"
> </a
><a name="1527" href="Data.BoundedVec.Inefficient.html#1" class="Module"
>Data.BoundedVec.Inefficient</a
><a name="1554"
>
</a
><a name="1555" class="Keyword"
>import</a
><a name="1561"
> </a
><a name="1562" href="Data.Char.html#1" class="Module"
>Data.Char</a
><a name="1571"
>
</a
><a name="1572" class="Keyword"
>import</a
><a name="1578"
> </a
><a name="1579" href="Data.Char.Base.html#1" class="Module"
>Data.Char.Base</a
><a name="1593"
>
</a
><a name="1594" class="Keyword"
>import</a
><a name="1600"
> </a
><a name="1601" href="Data.Char.Core.html#1" class="Module"
>Data.Char.Core</a
><a name="1615"
>
</a
><a name="1616" class="Keyword"
>import</a
><a name="1622"
> </a
><a name="1623" href="Data.Cofin.html#1" class="Module"
>Data.Cofin</a
><a name="1633"
>
</a
><a name="1634" class="Keyword"
>import</a
><a name="1640"
> </a
><a name="1641" href="Data.Colist.html#1" class="Module"
>Data.Colist</a
><a name="1652"
>
</a
><a name="1653" class="Keyword"
>import</a
><a name="1659"
> </a
><a name="1660" href="Data.Colist.Infinite-merge.html#1" class="Module"
>Data.Colist.Infinite-merge</a
><a name="1686"
>
</a
><a name="1687" class="Keyword"
>import</a
><a name="1693"
> </a
><a name="1694" href="Data.Conat.html#1" class="Module"
>Data.Conat</a
><a name="1704"
>
</a
><a name="1705" class="Keyword"
>import</a
><a name="1711"
> </a
><a name="1712" href="Data.Container.html#1" class="Module"
>Data.Container</a
><a name="1726"
>
</a
><a name="1727" class="Keyword"
>import</a
><a name="1733"
> </a
><a name="1734" href="Data.Container.Any.html#1" class="Module"
>Data.Container.Any</a
><a name="1752"
>
</a
><a name="1753" class="Keyword"
>import</a
><a name="1759"
> </a
><a name="1760" href="Data.Container.Combinator.html#1" class="Module"
>Data.Container.Combinator</a
><a name="1785"
>
</a
><a name="1786" class="Keyword"
>import</a
><a name="1792"
> </a
><a name="1793" href="Data.Container.FreeMonad.html#1" class="Module"
>Data.Container.FreeMonad</a
><a name="1817"
>
</a
><a name="1818" class="Keyword"
>import</a
><a name="1824"
> </a
><a name="1825" href="Data.Container.Indexed.html#1" class="Module"
>Data.Container.Indexed</a
><a name="1847"
>
</a
><a name="1848" class="Keyword"
>import</a
><a name="1854"
> </a
><a name="1855" href="Data.Container.Indexed.Combinator.html#1" class="Module"
>Data.Container.Indexed.Combinator</a
><a name="1888"
>
</a
><a name="1889" class="Keyword"
>import</a
><a name="1895"
> </a
><a name="1896" href="Data.Container.Indexed.Core.html#1" class="Module"
>Data.Container.Indexed.Core</a
><a name="1923"
>
</a
><a name="1924" class="Keyword"
>import</a
><a name="1930"
> </a
><a name="1931" href="Data.Container.Indexed.FreeMonad.html#1" class="Module"
>Data.Container.Indexed.FreeMonad</a
><a name="1963"
>
</a
><a name="1964" class="Keyword"
>import</a
><a name="1970"
> </a
><a name="1971" href="Data.Covec.html#1" class="Module"
>Data.Covec</a
><a name="1981"
>
</a
><a name="1982" class="Keyword"
>import</a
><a name="1988"
> </a
><a name="1989" href="Data.DifferenceList.html#1" class="Module"
>Data.DifferenceList</a
><a name="2008"
>
</a
><a name="2009" class="Keyword"
>import</a
><a name="2015"
> </a
><a name="2016" href="Data.DifferenceNat.html#1" class="Module"
>Data.DifferenceNat</a
><a name="2034"
>
</a
><a name="2035" class="Keyword"
>import</a
><a name="2041"
> </a
><a name="2042" href="Data.DifferenceVec.html#1" class="Module"
>Data.DifferenceVec</a
><a name="2060"
>
</a
><a name="2061" class="Keyword"
>import</a
><a name="2067"
> </a
><a name="2068" href="Data.Digit.html#1" class="Module"
>Data.Digit</a
><a name="2078"
>
</a
><a name="2079" class="Keyword"
>import</a
><a name="2085"
> </a
><a name="2086" href="Data.Empty.html#1" class="Module"
>Data.Empty</a
><a name="2096"
>
</a
><a name="2097" class="Keyword"
>import</a
><a name="2103"
> </a
><a name="2104" href="Data.Fin.html#1" class="Module"
>Data.Fin</a
><a name="2112"
>
</a
><a name="2113" class="Keyword"
>import</a
><a name="2119"
> </a
><a name="2120" href="Data.Fin.Dec.html#1" class="Module"
>Data.Fin.Dec</a
><a name="2132"
>
</a
><a name="2133" class="Keyword"
>import</a
><a name="2139"
> </a
><a name="2140" href="Data.Fin.Properties.html#1" class="Module"
>Data.Fin.Properties</a
><a name="2159"
>
</a
><a name="2160" class="Keyword"
>import</a
><a name="2166"
> </a
><a name="2167" href="Data.Fin.Subset.html#1" class="Module"
>Data.Fin.Subset</a
><a name="2182"
>
</a
><a name="2183" class="Keyword"
>import</a
><a name="2189"
> </a
><a name="2190" href="Data.Fin.Subset.Properties.html#1" class="Module"
>Data.Fin.Subset.Properties</a
><a name="2216"
>
</a
><a name="2217" class="Keyword"
>import</a
><a name="2223"
> </a
><a name="2224" href="Data.Fin.Substitution.html#1" class="Module"
>Data.Fin.Substitution</a
><a name="2245"
>
</a
><a name="2246" class="Keyword"
>import</a
><a name="2252"
> </a
><a name="2253" href="Data.Fin.Substitution.Example.html#1" class="Module"
>Data.Fin.Substitution.Example</a
><a name="2282"
>
</a
><a name="2283" class="Keyword"
>import</a
><a name="2289"
> </a
><a name="2290" href="Data.Fin.Substitution.Lemmas.html#1" class="Module"
>Data.Fin.Substitution.Lemmas</a
><a name="2318"
>
</a
><a name="2319" class="Keyword"
>import</a
><a name="2325"
> </a
><a name="2326" href="Data.Fin.Substitution.List.html#1" class="Module"
>Data.Fin.Substitution.List</a
><a name="2352"
>
</a
><a name="2353" class="Keyword"
>import</a
><a name="2359"
> </a
><a name="2360" href="Data.Float.html#1" class="Module"
>Data.Float</a
><a name="2370"
>
</a
><a name="2371" class="Keyword"
>import</a
><a name="2377"
> </a
><a name="2378" href="Data.Graph.Acyclic.html#1" class="Module"
>Data.Graph.Acyclic</a
><a name="2396"
>
</a
><a name="2397" class="Keyword"
>import</a
><a name="2403"
> </a
><a name="2404" href="Data.Integer.html#1" class="Module"
>Data.Integer</a
><a name="2416"
>
</a
><a name="2417" class="Keyword"
>import</a
><a name="2423"
> </a
><a name="2424" href="Data.Integer.Addition.Properties.html#1" class="Module"
>Data.Integer.Addition.Properties</a
><a name="2456"
>
</a
><a name="2457" class="Keyword"
>import</a
><a name="2463"
> </a
><a name="2464" href="Data.Integer.Divisibility.html#1" class="Module"
>Data.Integer.Divisibility</a
><a name="2489"
>
</a
><a name="2490" class="Keyword"
>import</a
><a name="2496"
> </a
><a name="2497" href="Data.Integer.Multiplication.Properties.html#1" class="Module"
>Data.Integer.Multiplication.Properties</a
><a name="2535"
>
</a
><a name="2536" class="Keyword"
>import</a
><a name="2542"
> </a
><a name="2543" href="Data.Integer.Properties.html#1" class="Module"
>Data.Integer.Properties</a
><a name="2566"
>
</a
><a name="2567" class="Keyword"
>import</a
><a name="2573"
> </a
><a name="2574" href="Data.List.html#1" class="Module"
>Data.List</a
><a name="2583"
>
</a
><a name="2584" class="Keyword"
>import</a
><a name="2590"
> </a
><a name="2591" href="Data.List.All.html#1" class="Module"
>Data.List.All</a
><a name="2604"
>
</a
><a name="2605" class="Keyword"
>import</a
><a name="2611"
> </a
><a name="2612" href="Data.List.All.Properties.html#1" class="Module"
>Data.List.All.Properties</a
><a name="2636"
>
</a
><a name="2637" class="Keyword"
>import</a
><a name="2643"
> </a
><a name="2644" href="Data.List.Any.html#1" class="Module"
>Data.List.Any</a
><a name="2657"
>
</a
><a name="2658" class="Keyword"
>import</a
><a name="2664"
> </a
><a name="2665" href="Data.List.Any.BagAndSetEquality.html#1" class="Module"
>Data.List.Any.BagAndSetEquality</a
><a name="2696"
>
</a
><a name="2697" class="Keyword"
>import</a
><a name="2703"
> </a
><a name="2704" href="Data.List.Any.Membership.html#1" class="Module"
>Data.List.Any.Membership</a
><a name="2728"
>
</a
><a name="2729" class="Keyword"
>import</a
><a name="2735"
> </a
><a name="2736" href="Data.List.Any.Properties.html#1" class="Module"
>Data.List.Any.Properties</a
><a name="2760"
>
</a
><a name="2761" class="Keyword"
>import</a
><a name="2767"
> </a
><a name="2768" href="Data.List.Base.html#1" class="Module"
>Data.List.Base</a
><a name="2782"
>
</a
><a name="2783" class="Keyword"
>import</a
><a name="2789"
> </a
><a name="2790" href="Data.List.Countdown.html#1" class="Module"
>Data.List.Countdown</a
><a name="2809"
>
</a
><a name="2810" class="Keyword"
>import</a
><a name="2816"
> </a
><a name="2817" href="Data.List.NonEmpty.html#1" class="Module"
>Data.List.NonEmpty</a
><a name="2835"
>
</a
><a name="2836" class="Keyword"
>import</a
><a name="2842"
> </a
><a name="2843" href="Data.List.NonEmpty.Properties.html#1" class="Module"
>Data.List.NonEmpty.Properties</a
><a name="2872"
>
</a
><a name="2873" class="Keyword"
>import</a
><a name="2879"
> </a
><a name="2880" href="Data.List.Properties.html#1" class="Module"
>Data.List.Properties</a
><a name="2900"
>
</a
><a name="2901" class="Keyword"
>import</a
><a name="2907"
> </a
><a name="2908" href="Data.List.Reverse.html#1" class="Module"
>Data.List.Reverse</a
><a name="2925"
>
</a
><a name="2926" class="Keyword"
>import</a
><a name="2932"
> </a
><a name="2933" href="Data.M.html#1" class="Module"
>Data.M</a
><a name="2939"
>
</a
><a name="2940" class="Keyword"
>import</a
><a name="2946"
> </a
><a name="2947" href="Data.Maybe.html#1" class="Module"
>Data.Maybe</a
><a name="2957"
>
</a
><a name="2958" class="Keyword"
>import</a
><a name="2964"
> </a
><a name="2965" href="Data.Maybe.Base.html#1" class="Module"
>Data.Maybe.Base</a
><a name="2980"
>
</a
><a name="2981" class="Keyword"
>import</a
><a name="2987"
> </a
><a name="2988" href="Data.M.Indexed.html#1" class="Module"
>Data.M.Indexed</a
><a name="3002"
>
</a
><a name="3003" class="Keyword"
>import</a
><a name="3009"
> </a
><a name="3010" href="Data.Nat.html#1" class="Module"
>Data.Nat</a
><a name="3018"
>
</a
><a name="3019" class="Keyword"
>import</a
><a name="3025"
> </a
><a name="3026" href="Data.Nat.Base.html#1" class="Module"
>Data.Nat.Base</a
><a name="3039"
>
</a
><a name="3040" class="Keyword"
>import</a
><a name="3046"
> </a
><a name="3047" href="Data.Nat.Coprimality.html#1" class="Module"
>Data.Nat.Coprimality</a
><a name="3067"
>
</a
><a name="3068" class="Keyword"
>import</a
><a name="3074"
> </a
><a name="3075" href="Data.Nat.Divisibility.html#1" class="Module"
>Data.Nat.Divisibility</a
><a name="3096"
>
</a
><a name="3097" class="Keyword"
>import</a
><a name="3103"
> </a
><a name="3104" href="Data.Nat.DivMod.html#1" class="Module"
>Data.Nat.DivMod</a
><a name="3119"
>
</a
><a name="3120" class="Keyword"
>import</a
><a name="3126"
> </a
><a name="3127" href="Data.Nat.GCD.html#1" class="Module"
>Data.Nat.GCD</a
><a name="3139"
>
</a
><a name="3140" class="Keyword"
>import</a
><a name="3146"
> </a
><a name="3147" href="Data.Nat.GCD.Lemmas.html#1" class="Module"
>Data.Nat.GCD.Lemmas</a
><a name="3166"
>
</a
><a name="3167" class="Keyword"
>import</a
><a name="3173"
> </a
><a name="3174" href="Data.Nat.InfinitelyOften.html#1" class="Module"
>Data.Nat.InfinitelyOften</a
><a name="3198"
>
</a
><a name="3199" class="Keyword"
>import</a
><a name="3205"
> </a
><a name="3206" href="Data.Nat.LCM.html#1" class="Module"
>Data.Nat.LCM</a
><a name="3218"
>
</a
><a name="3219" class="Keyword"
>import</a
><a name="3225"
> </a
><a name="3226" href="Data.Nat.Primality.html#1" class="Module"
>Data.Nat.Primality</a
><a name="3244"
>
</a
><a name="3245" class="Keyword"
>import</a
><a name="3251"
> </a
><a name="3252" href="Data.Nat.Properties.html#1" class="Module"
>Data.Nat.Properties</a
><a name="3271"
>
</a
><a name="3272" class="Keyword"
>import</a
><a name="3278"
> </a
><a name="3279" href="Data.Nat.Properties.Simple.html#1" class="Module"
>Data.Nat.Properties.Simple</a
><a name="3305"
>
</a
><a name="3306" class="Keyword"
>import</a
><a name="3312"
> </a
><a name="3313" href="Data.Nat.Show.html#1" class="Module"
>Data.Nat.Show</a
><a name="3326"
>
</a
><a name="3327" class="Keyword"
>import</a
><a name="3333"
> </a
><a name="3334" href="Data.Plus.html#1" class="Module"
>Data.Plus</a
><a name="3343"
>
</a
><a name="3344" class="Keyword"
>import</a
><a name="3350"
> </a
><a name="3351" href="Data.Product.html#1" class="Module"
>Data.Product</a
><a name="3363"
>
</a
><a name="3364" class="Keyword"
>import</a
><a name="3370"
> </a
><a name="3371" href="Data.Product.N-ary.html#1" class="Module"
>Data.Product.N-ary</a
><a name="3389"
>
</a
><a name="3390" class="Keyword"
>import</a
><a name="3396"
> </a
><a name="3397" href="Data.Rational.html#1" class="Module"
>Data.Rational</a
><a name="3410"
>
</a
><a name="3411" class="Keyword"
>import</a
><a name="3417"
> </a
><a name="3418" href="Data.ReflexiveClosure.html#1" class="Module"
>Data.ReflexiveClosure</a
><a name="3439"
>
</a
><a name="3440" class="Keyword"
>import</a
><a name="3446"
> </a
><a name="3447" href="Data.Sign.html#1" class="Module"
>Data.Sign</a
><a name="3456"
>
</a
><a name="3457" class="Keyword"
>import</a
><a name="3463"
> </a
><a name="3464" href="Data.Sign.Properties.html#1" class="Module"
>Data.Sign.Properties</a
><a name="3484"
>
</a
><a name="3485" class="Keyword"
>import</a
><a name="3491"
> </a
><a name="3492" href="Data.Star.html#1" class="Module"
>Data.Star</a
><a name="3501"
>
</a
><a name="3502" class="Keyword"
>import</a
><a name="3508"
> </a
><a name="3509" href="Data.Star.BoundedVec.html#1" class="Module"
>Data.Star.BoundedVec</a
><a name="3529"
>
</a
><a name="3530" class="Keyword"
>import</a
><a name="3536"
> </a
><a name="3537" href="Data.Star.Decoration.html#1" class="Module"
>Data.Star.Decoration</a
><a name="3557"
>
</a
><a name="3558" class="Keyword"
>import</a
><a name="3564"
> </a
><a name="3565" href="Data.Star.Environment.html#1" class="Module"
>Data.Star.Environment</a
><a name="3586"
>
</a
><a name="3587" class="Keyword"
>import</a
><a name="3593"
> </a
><a name="3594" href="Data.Star.Fin.html#1" class="Module"
>Data.Star.Fin</a
><a name="3607"
>
</a
><a name="3608" class="Keyword"
>import</a
><a name="3614"
> </a
><a name="3615" href="Data.Star.List.html#1" class="Module"
>Data.Star.List</a
><a name="3629"
>
</a
><a name="3630" class="Keyword"
>import</a
><a name="3636"
> </a
><a name="3637" href="Data.Star.Nat.html#1" class="Module"
>Data.Star.Nat</a
><a name="3650"
>
</a
><a name="3651" class="Keyword"
>import</a
><a name="3657"
> </a
><a name="3658" href="Data.Star.Pointer.html#1" class="Module"
>Data.Star.Pointer</a
><a name="3675"
>
</a
><a name="3676" class="Keyword"
>import</a
><a name="3682"
> </a
><a name="3683" href="Data.Star.Properties.html#1" class="Module"
>Data.Star.Properties</a
><a name="3703"
>
</a
><a name="3704" class="Keyword"
>import</a
><a name="3710"
> </a
><a name="3711" href="Data.Star.Vec.html#1" class="Module"
>Data.Star.Vec</a
><a name="3724"
>
</a
><a name="3725" class="Keyword"
>import</a
><a name="3731"
> </a
><a name="3732" href="Data.Stream.html#1" class="Module"
>Data.Stream</a
><a name="3743"
>
</a
><a name="3744" class="Keyword"
>import</a
><a name="3750"
> </a
><a name="3751" href="Data.String.html#1" class="Module"
>Data.String</a
><a name="3762"
>
</a
><a name="3763" class="Keyword"
>import</a
><a name="3769"
> </a
><a name="3770" href="Data.String.Base.html#1" class="Module"
>Data.String.Base</a
><a name="3786"
>
</a
><a name="3787" class="Keyword"
>import</a
><a name="3793"
> </a
><a name="3794" href="Data.Sum.html#1" class="Module"
>Data.Sum</a
><a name="3802"
>
</a
><a name="3803" class="Keyword"
>import</a
><a name="3809"
> </a
><a name="3810" href="Data.Unit.html#1" class="Module"
>Data.Unit</a
><a name="3819"
>
</a
><a name="3820" class="Keyword"
>import</a
><a name="3826"
> </a
><a name="3827" href="Data.Unit.Base.html#1" class="Module"
>Data.Unit.Base</a
><a name="3841"
>
</a
><a name="3842" class="Keyword"
>import</a
><a name="3848"
> </a
><a name="3849" href="Data.Unit.NonEta.html#1" class="Module"
>Data.Unit.NonEta</a
><a name="3865"
>
</a
><a name="3866" class="Keyword"
>import</a
><a name="3872"
> </a
><a name="3873" href="Data.Vec.html#1" class="Module"
>Data.Vec</a
><a name="3881"
>
</a
><a name="3882" class="Keyword"
>import</a
><a name="3888"
> </a
><a name="3889" href="Data.Vec.Equality.html#1" class="Module"
>Data.Vec.Equality</a
><a name="3906"
>
</a
><a name="3907" class="Keyword"
>import</a
><a name="3913"
> </a
><a name="3914" href="Data.Vec.N-ary.html#1" class="Module"
>Data.Vec.N-ary</a
><a name="3928"
>
</a
><a name="3929" class="Keyword"
>import</a
><a name="3935"
> </a
><a name="3936" href="Data.Vec.Properties.html#1" class="Module"
>Data.Vec.Properties</a
><a name="3955"
>
</a
><a name="3956" class="Keyword"
>import</a
><a name="3962"
> </a
><a name="3963" href="Data.W.html#1" class="Module"
>Data.W</a
><a name="3969"
>
</a
><a name="3970" class="Keyword"
>import</a
><a name="3976"
> </a
><a name="3977" href="Data.W.Indexed.html#1" class="Module"
>Data.W.Indexed</a
><a name="3991"
>
</a
><a name="3992" class="Keyword"
>import</a
><a name="3998"
> </a
><a name="3999" href="Foreign.Haskell.html#1" class="Module"
>Foreign.Haskell</a
><a name="4014"
>
</a
><a name="4015" class="Keyword"
>import</a
><a name="4021"
> </a
><a name="4022" href="Function.html#1" class="Module"
>Function</a
><a name="4030"
>
</a
><a name="4031" class="Keyword"
>import</a
><a name="4037"
> </a
><a name="4038" href="Function.Bijection.html#1" class="Module"
>Function.Bijection</a
><a name="4056"
>
</a
><a name="4057" class="Keyword"
>import</a
><a name="4063"
> </a
><a name="4064" href="Function.Equality.html#1" class="Module"
>Function.Equality</a
><a name="4081"
>
</a
><a name="4082" class="Keyword"
>import</a
><a name="4088"
> </a
><a name="4089" href="Function.Equivalence.html#1" class="Module"
>Function.Equivalence</a
><a name="4109"
>
</a
><a name="4110" class="Keyword"
>import</a
><a name="4116"
> </a
><a name="4117" href="Function.Injection.html#1" class="Module"
>Function.Injection</a
><a name="4135"
>
</a
><a name="4136" class="Keyword"
>import</a
><a name="4142"
> </a
><a name="4143" href="Function.Inverse.html#1" class="Module"
>Function.Inverse</a
><a name="4159"
>
</a
><a name="4160" class="Keyword"
>import</a
><a name="4166"
> </a
><a name="4167" href="Function.LeftInverse.html#1" class="Module"
>Function.LeftInverse</a
><a name="4187"
>
</a
><a name="4188" class="Keyword"
>import</a
><a name="4194"
> </a
><a name="4195" href="Function.Related.html#1" class="Module"
>Function.Related</a
><a name="4211"
>
</a
><a name="4212" class="Keyword"
>import</a
><a name="4218"
> </a
><a name="4219" href="Function.Related.TypeIsomorphisms.html#1" class="Module"
>Function.Related.TypeIsomorphisms</a
><a name="4252"
>
</a
><a name="4253" class="Keyword"
>import</a
><a name="4259"
> </a
><a name="4260" href="Function.Surjection.html#1" class="Module"
>Function.Surjection</a
><a name="4279"
>
</a
><a name="4280" class="Keyword"
>import</a
><a name="4286"
> </a
><a name="4287" href="Induction.html#1" class="Module"
>Induction</a
><a name="4296"
>
</a
><a name="4297" class="Keyword"
>import</a
><a name="4303"
> </a
><a name="4304" href="Induction.Lexicographic.html#1" class="Module"
>Induction.Lexicographic</a
><a name="4327"
>
</a
><a name="4328" class="Keyword"
>import</a
><a name="4334"
> </a
><a name="4335" href="Induction.Nat.html#1" class="Module"
>Induction.Nat</a
><a name="4348"
>
</a
><a name="4349" class="Keyword"
>import</a
><a name="4355"
> </a
><a name="4356" href="Induction.WellFounded.html#1" class="Module"
>Induction.WellFounded</a
><a name="4377"
>
</a
><a name="4378" class="Keyword"
>import</a
><a name="4384"
> </a
><a name="4385" href="IO.html#1" class="Module"
>IO</a
><a name="4387"
>
</a
><a name="4388" class="Keyword"
>import</a
><a name="4394"
> </a
><a name="4395" href="IO.Primitive.html#1" class="Module"
>IO.Primitive</a
><a name="4407"
>
</a
><a name="4408" class="Keyword"
>import</a
><a name="4414"
> </a
><a name="4415" href="Irrelevance.html#1" class="Module"
>Irrelevance</a
><a name="4426"
>
</a
><a name="4427" class="Keyword"
>import</a
><a name="4433"
> </a
><a name="4434" href="Level.html#1" class="Module"
>Level</a
><a name="4439"
>
</a
><a name="4440" class="Keyword"
>import</a
><a name="4446"
> </a
><a name="4447" href="Record.html#1" class="Module"
>Record</a
><a name="4453"
>
</a
><a name="4454" class="Keyword"
>import</a
><a name="4460"
> </a
><a name="4461" href="Reflection.html#1" class="Module"
>Reflection</a
><a name="4471"
>
</a
><a name="4472" class="Keyword"
>import</a
><a name="4478"
> </a
><a name="4479" href="Relation.Binary.html#1" class="Module"
>Relation.Binary</a
><a name="4494"
>
</a
><a name="4495" class="Keyword"
>import</a
><a name="4501"
> </a
><a name="4502" href="Relation.Binary.Consequences.html#1" class="Module"
>Relation.Binary.Consequences</a
><a name="4530"
>
</a
><a name="4531" class="Keyword"
>import</a
><a name="4537"
> </a
><a name="4538" href="Relation.Binary.Consequences.Core.html#1" class="Module"
>Relation.Binary.Consequences.Core</a
><a name="4571"
>
</a
><a name="4572" class="Keyword"
>import</a
><a name="4578"
> </a
><a name="4579" href="Relation.Binary.Core.html#1" class="Module"
>Relation.Binary.Core</a
><a name="4599"
>
</a
><a name="4600" class="Keyword"
>import</a
><a name="4606"
> </a
><a name="4607" href="Relation.Binary.EqReasoning.html#1" class="Module"
>Relation.Binary.EqReasoning</a
><a name="4634"
>
</a
><a name="4635" class="Keyword"
>import</a
><a name="4641"
> </a
><a name="4642" href="Relation.Binary.Flip.html#1" class="Module"
>Relation.Binary.Flip</a
><a name="4662"
>
</a
><a name="4663" class="Keyword"
>import</a
><a name="4669"
> </a
><a name="4670" href="Relation.Binary.HeterogeneousEquality.html#1" class="Module"
>Relation.Binary.HeterogeneousEquality</a
><a name="4707"
>
</a
><a name="4708" class="Keyword"
>import</a
><a name="4714"
> </a
><a name="4715" href="Relation.Binary.HeterogeneousEquality.Core.html#1" class="Module"
>Relation.Binary.HeterogeneousEquality.Core</a
><a name="4757"
>
</a
><a name="4758" class="Keyword"
>import</a
><a name="4764"
> </a
><a name="4765" href="Relation.Binary.Indexed.html#1" class="Module"
>Relation.Binary.Indexed</a
><a name="4788"
>
</a
><a name="4789" class="Keyword"
>import</a
><a name="4795"
> </a
><a name="4796" href="Relation.Binary.Indexed.Core.html#1" class="Module"
>Relation.Binary.Indexed.Core</a
><a name="4824"
>
</a
><a name="4825" class="Keyword"
>import</a
><a name="4831"
> </a
><a name="4832" href="Relation.Binary.InducedPreorders.html#1" class="Module"
>Relation.Binary.InducedPreorders</a
><a name="4864"
>
</a
><a name="4865" class="Keyword"
>import</a
><a name="4871"
> </a
><a name="4872" href="Relation.Binary.List.NonStrictLex.html#1" class="Module"
>Relation.Binary.List.NonStrictLex</a
><a name="4905"
>
</a
><a name="4906" class="Keyword"
>import</a
><a name="4912"
> </a
><a name="4913" href="Relation.Binary.List.Pointwise.html#1" class="Module"
>Relation.Binary.List.Pointwise</a
><a name="4943"
>
</a
><a name="4944" class="Keyword"
>import</a
><a name="4950"
> </a
><a name="4951" href="Relation.Binary.List.StrictLex.html#1" class="Module"
>Relation.Binary.List.StrictLex</a
><a name="4981"
>
</a
><a name="4982" class="Keyword"
>import</a
><a name="4988"
> </a
><a name="4989" href="Relation.Binary.NonStrictToStrict.html#1" class="Module"
>Relation.Binary.NonStrictToStrict</a
><a name="5022"
>
</a
><a name="5023" class="Keyword"
>import</a
><a name="5029"
> </a
><a name="5030" href="Relation.Binary.On.html#1" class="Module"
>Relation.Binary.On</a
><a name="5048"
>
</a
><a name="5049" class="Keyword"
>import</a
><a name="5055"
> </a
><a name="5056" href="Relation.Binary.OrderMorphism.html#1" class="Module"
>Relation.Binary.OrderMorphism</a
><a name="5085"
>
</a
><a name="5086" class="Keyword"
>import</a
><a name="5092"
> </a
><a name="5093" href="Relation.Binary.PartialOrderReasoning.html#1" class="Module"
>Relation.Binary.PartialOrderReasoning</a
><a name="5130"
>
</a
><a name="5131" class="Keyword"
>import</a
><a name="5137"
> </a
><a name="5138" href="Relation.Binary.PreorderReasoning.html#1" class="Module"
>Relation.Binary.PreorderReasoning</a
><a name="5171"
>
</a
><a name="5172" class="Keyword"
>import</a
><a name="5178"
> </a
><a name="5179" href="Relation.Binary.Product.NonStrictLex.html#1" class="Module"
>Relation.Binary.Product.NonStrictLex</a
><a name="5215"
>
</a
><a name="5216" class="Keyword"
>import</a
><a name="5222"
> </a
><a name="5223" href="Relation.Binary.Product.Pointwise.html#1" class="Module"
>Relation.Binary.Product.Pointwise</a
><a name="5256"
>
</a
><a name="5257" class="Keyword"
>import</a
><a name="5263"
> </a
><a name="5264" href="Relation.Binary.Product.StrictLex.html#1" class="Module"
>Relation.Binary.Product.StrictLex</a
><a name="5297"
>
</a
><a name="5298" class="Keyword"
>import</a
><a name="5304"
> </a
><a name="5305" href="Relation.Binary.Properties.DecTotalOrder.html#1" class="Module"
>Relation.Binary.Properties.DecTotalOrder</a
><a name="5345"
>
</a
><a name="5346" class="Keyword"
>import</a
><a name="5352"
> </a
><a name="5353" href="Relation.Binary.Properties.Poset.html#1" class="Module"
>Relation.Binary.Properties.Poset</a
><a name="5385"
>
</a
><a name="5386" class="Keyword"
>import</a
><a name="5392"
> </a
><a name="5393" href="Relation.Binary.Properties.Preorder.html#1" class="Module"
>Relation.Binary.Properties.Preorder</a
><a name="5428"
>
</a
><a name="5429" class="Keyword"
>import</a
><a name="5435"
> </a
><a name="5436" href="Relation.Binary.Properties.StrictPartialOrder.html#1" class="Module"
>Relation.Binary.Properties.StrictPartialOrder</a
><a name="5481"
>
</a
><a name="5482" class="Keyword"
>import</a
><a name="5488"
> </a
><a name="5489" href="Relation.Binary.Properties.StrictTotalOrder.html#1" class="Module"
>Relation.Binary.Properties.StrictTotalOrder</a
><a name="5532"
>
</a
><a name="5533" class="Keyword"
>import</a
><a name="5539"
> </a
><a name="5540" href="Relation.Binary.Properties.TotalOrder.html#1" class="Module"
>Relation.Binary.Properties.TotalOrder</a
><a name="5577"
>
</a
><a name="5578" class="Keyword"
>import</a
><a name="5584"
> </a
><a name="5585" href="Relation.Binary.PropositionalEquality.html#1" class="Module"
>Relation.Binary.PropositionalEquality</a
><a name="5622"
>
</a
><a name="5623" class="Keyword"
>import</a
><a name="5629"
> </a
><a name="5630" href="Relation.Binary.PropositionalEquality.Core.html#1" class="Module"
>Relation.Binary.PropositionalEquality.Core</a
><a name="5672"
>
</a
><a name="5673" class="Keyword"
>import</a
><a name="5679"
> </a
><a name="5680" href="Relation.Binary.PropositionalEquality.TrustMe.html#1" class="Module"
>Relation.Binary.PropositionalEquality.TrustMe</a
><a name="5725"
>
</a
><a name="5726" class="Keyword"
>import</a
><a name="5732"
> </a
><a name="5733" href="Relation.Binary.Reflection.html#1" class="Module"
>Relation.Binary.Reflection</a
><a name="5759"
>
</a
><a name="5760" class="Keyword"
>import</a
><a name="5766"
> </a
><a name="5767" href="Relation.Binary.SetoidReasoning.html#1" class="Module"
>Relation.Binary.SetoidReasoning</a
><a name="5798"
>
</a
><a name="5799" class="Keyword"
>import</a
><a name="5805"
> </a
><a name="5806" href="Relation.Binary.Sigma.Pointwise.html#1" class="Module"
>Relation.Binary.Sigma.Pointwise</a
><a name="5837"
>
</a
><a name="5838" class="Keyword"
>import</a
><a name="5844"
> </a
><a name="5845" href="Relation.Binary.Simple.html#1" class="Module"
>Relation.Binary.Simple</a
><a name="5867"
>
</a
><a name="5868" class="Keyword"
>import</a
><a name="5874"
> </a
><a name="5875" href="Relation.Binary.StrictPartialOrderReasoning.html#1" class="Module"
>Relation.Binary.StrictPartialOrderReasoning</a
><a name="5918"
>
</a
><a name="5919" class="Keyword"
>import</a
><a name="5925"
> </a
><a name="5926" href="Relation.Binary.StrictToNonStrict.html#1" class="Module"
>Relation.Binary.StrictToNonStrict</a
><a name="5959"
>
</a
><a name="5960" class="Keyword"
>import</a
><a name="5966"
> </a
><a name="5967" href="Relation.Binary.Sum.html#1" class="Module"
>Relation.Binary.Sum</a
><a name="5986"
>
</a
><a name="5987" class="Keyword"
>import</a
><a name="5993"
> </a
><a name="5994" href="Relation.Binary.Vec.Pointwise.html#1" class="Module"
>Relation.Binary.Vec.Pointwise</a
><a name="6023"
>
</a
><a name="6024" class="Keyword"
>import</a
><a name="6030"
> </a
><a name="6031" href="Relation.Nullary.html#1" class="Module"
>Relation.Nullary</a
><a name="6047"
>
</a
><a name="6048" class="Keyword"
>import</a
><a name="6054"
> </a
><a name="6055" href="Relation.Nullary.Decidable.html#1" class="Module"
>Relation.Nullary.Decidable</a
><a name="6081"
>
</a
><a name="6082" class="Keyword"
>import</a
><a name="6088"
> </a
><a name="6089" href="Relation.Nullary.Implication.html#1" class="Module"
>Relation.Nullary.Implication</a
><a name="6117"
>
</a
><a name="6118" class="Keyword"
>import</a
><a name="6124"
> </a
><a name="6125" href="Relation.Nullary.Negation.html#1" class="Module"
>Relation.Nullary.Negation</a
><a name="6150"
>
</a
><a name="6151" class="Keyword"
>import</a
><a name="6157"
> </a
><a name="6158" href="Relation.Nullary.Product.html#1" class="Module"
>Relation.Nullary.Product</a
><a name="6182"
>
</a
><a name="6183" class="Keyword"
>import</a
><a name="6189"
> </a
><a name="6190" href="Relation.Nullary.Sum.html#1" class="Module"
>Relation.Nullary.Sum</a
><a name="6210"
>
</a
><a name="6211" class="Keyword"
>import</a
><a name="6217"
> </a
><a name="6218" href="Relation.Nullary.Universe.html#1" class="Module"
>Relation.Nullary.Universe</a
><a name="6243"
>
</a
><a name="6244" class="Keyword"
>import</a
><a name="6250"
> </a
><a name="6251" href="Relation.Unary.html#1" class="Module"
>Relation.Unary</a
><a name="6265"
>
</a
><a name="6266" class="Keyword"
>import</a
><a name="6272"
> </a
><a name="6273" href="Relation.Unary.PredicateTransformer.html#1" class="Module"
>Relation.Unary.PredicateTransformer</a
><a name="6308"
>
</a
><a name="6309" class="Keyword"
>import</a
><a name="6315"
> </a
><a name="6316" href="Size.html#1" class="Module"
>Size</a
><a name="6320"
>
</a
><a name="6321" class="Keyword"
>import</a
><a name="6327"
> </a
><a name="6328" href="Universe.html#1" class="Module"
>Universe</a
><a name="6336"
>
</a
></pre
></body
></html
>