Package contrib - Namespaces

• Control.ANSI
• Control.ANSI.SGR
• Control.ANSI.CSI
• Control.Delayed

  Utilities functions for conditionally delaying values.
• Control.Arrow
• Control.Category
• Control.Validation
• Data.Binary.Digit
• Data.Binary
• Data.Fin.Extra
• Data.Fun.Extra
• Data.Fun.Graph
• Data.IMaybe

  Version of Maybe indexed by an `isJust' boolean
• Data.Int.Order

  Implementation of ordering relations for the primitive type `Int` This is full of tricks as `Int` is a primitive type that can only be interacted with using either literals or built-in functions. The exported interface should however be safe.
• Data.IOMatrix
• Data.Late
• Data.Linear.Array
• Data.List.TailRec

  Contains:
• Data.List.Equalities
• Data.List.Extra
• Data.List.Reverse

  Properties of the reverse function.
• Data.List.Views.Extra
• Data.List.Palindrome
• Data.List.Alternating
• Data.List.Sufficient

  WellFounded on List suffixes
• Data.List.Elem.Extra
• Data.Logic.Propositional
• Data.Monoid.Exponentiation
• Data.Nat.Ack

  Properties of Ackermann functions
• Data.Nat.Division

  Division theorem for (type-level) natural number division
• Data.Nat.Equational
• Data.Nat.Exponentiation
• Data.Nat.Fact

  Properties of factorial functions
• Data.Nat.Factor
• Data.Nat.Fib

  Properties of Fibonacci functions
• Data.Nat.Order.Strict

  Implementing `Decidable.Order.Strict` for `Data.Nat.LT`
• Data.Nat.Order.Relation

  An example implementation for the Tolerance relation.
• Data.Nat.Properties

  Additional properties/lemmata of Nats
• Data.Order

  Additional data types related to ordering notions
• Data.Path
• Data.Rel.Complement
• Data.Seq.Internal

  This module is not intended to be imported directly. Please use Data.Seq or Data.Seq.Seq' instead.
• Data.Seq.Sized

  General purpose two-end finite sequences, with length in its type.
• Data.Seq.Unsized

  General purpose two-end finite sequences.
• Data.Stream.Extra
• Data.String.Extra
• Data.String.Interpolation

  A DYI version of 'string interpolation', mimicking Python 3's 'f-string' syntax Not as fancy
• Data.String.Iterator
• Data.String.Parser

  A simple parser combinator library for String. Inspired by attoparsec zepto.
• Data.String.Parser.Expression
• Data.String.Position

  A small library introducing string positions This can be used as an alternative to unpacking a string into a list of characters
• Data.Telescope

  A telescope is the variable context in a dependently typed program. Dependent types with free variables are really only well-defined in a telescope.
• Data.Telescope.Telescope

  The telescope data structures.
• Data.Telescope.Segment

  A segment is a compositional fragment of a telescope. A key difference is that segments are right-nested, whereas telescopes are left nested. So telescopes are convenient for well-bracketing dependencies, but segments are convenient for processing telescopes from left to right.
• Data.Telescope.Fun

  N-ary dependent functions using telescopes
• Data.Telescope.SimpleFun

  N-ary simple (non-dependent) functions using telescopes
• Data.Telescope.Congruence

  N-ary congruence for reasoning
• Data.Validated
• Data.Vect.Properties

  Additional properties and lemmata to do with Vect
• Data.Vect.Properties.Tabulate

  Tabulation gives a bijection between functions `f : Fin n -> a` (up to extensional equality) and vectors `tabulate f : Vect n a`.
• Data.Vect.Properties.Index

  Properties of Data.Vect.index
• Data.Vect.Properties.Foldr
• Data.Vect.Properties.Map

  Properties of Data.Vect.map
• Data.Vect.Properties.Fin
• Data.Vect.Extra

  Additional functions about vectors
• Data.Vect.Sort
• Debug.Buffer
• Decidable.Finite.Fin
• Decidable.Order.Strict

  An strict preorder (sometimes known as a quasi-order, or an ordering) is what you get when you remove the diagonal `{(a,b) | a r b , b r a}` from a preorder. For example a < b is an ordering. This module extends base's Control.Order with the strict versions. The interface system seems to struggle a bit with some of the constructions, so I hacked them a bit. Sorry.
• Decidable.Decidable.Extra
• Language.JSON

  The JSON language, as described at https://json.org/
• Language.JSON.Data
• Language.JSON.Lexer
• Language.JSON.Parser
• Language.JSON.String
• Language.JSON.String.Lexer
• Language.JSON.String.Parser
• Language.JSON.String.Tokens
• Language.JSON.Tokens
• System.Console.GetOpt

  This library provides facilities for parsing the command-line options in a standalone program. It is essentially an Idris port of the GNU getopt library. (Actually, it is an Idris port of the [corresponding Haskell module] (http://hackage.haskell.org/package/base-4.14.1.0/docs/System-Console-GetOpt.html)).
• System.Directory.Tree
• System.Future
• System.Random
• System.Path
• Text.Bounded
• Text.Distance.Levenshtein
• Text.Lexer
• Text.Lexer.Core
• Text.Lexer.Tokenizer
• Text.Literate

  A simple module to process 'literate' documents.
• Text.Parser
• Text.Parser.Core
• Text.Parser.Expression
• Text.PrettyPrint.Prettyprinter

  A Idris port of the prettyprinter library [1] and the ANSI terminal backend [2].
• Text.PrettyPrint.Prettyprinter.Doc
• Text.PrettyPrint.Prettyprinter.Render.HTML
• Text.PrettyPrint.Prettyprinter.Render.String
• Text.PrettyPrint.Prettyprinter.Render.Terminal
• Text.PrettyPrint.Prettyprinter.SimpleDocTree
• Text.PrettyPrint.Prettyprinter.Symbols
• Text.PrettyPrint.Prettyprinter.Util
• Text.Quantity
• Text.Token