Package base - Namespaces

• Control.App
• Control.App.Console
• Control.App.FileIO
• Control.Applicative.Const
• Control.Function
• Control.Function.FunExt
• Control.Monad.Either
• Control.Monad.Error.Either

  Provides a monad transformer `EitherT` that extends an inner monad with the ability to throw and catch exceptions.
• Control.Monad.Error.Interface

  The Error monad (also called the Exception monad).
• Control.Monad.Identity
• Control.Monad.Maybe
• Control.Monad.Partial
• Control.Monad.RWS
• Control.Monad.RWS.CPS

  Note: The difference to a 'strict' RWST implementation is that accumulation of values does not happen in the Applicative and Monad instances but when invoking `Writer`-specific functions like `writer` or `listen`.
• Control.Monad.RWS.Interface
• Control.Monad.Reader
• Control.Monad.Reader.Interface
• Control.Monad.Reader.Reader
• Control.Monad.ST

  Provides mutable references as described in Lazy Functional State Threads.
• Control.Monad.State
• Control.Monad.State.Interface
• Control.Monad.State.State
• Control.Monad.Trans
• Control.Monad.Writer
• Control.Monad.Writer.CPS

  Note: The difference to a 'strict' Writer implementation is that accumulation of values does not happen in the Applicative and Monad instances but when invoking `Writer`-specific functions like `writer` or `listen`.
• Control.Monad.Writer.Interface
• Control.Ord
• Control.Order

  An order is a particular kind of binary relation. The order relation is intended to proceed in some direction, though not necessarily with a unique path. Orders are often defined simply as bundles of binary relation properties. A prominent example of an order relation is LTE over Nat.
• Control.Relation

  A binary relation is a function of type (ty -> ty -> Type). A prominent example of a binary relation is LTE over Nat. This module defines some interfaces for describing properties of binary relations. It also proves somes relations among relations.
• Control.Relation.Closure
• Control.WellFounded

  Defines well-founded induction and recursion. Induction is way to consume elements of recursive types where each step of the computation has access to the previous steps. Normally, induction is structural: the previous steps are the children of the current element. Well-founded induction generalises this as follows: each step has access to any value that is less than the current element, based on a relation. Well-founded induction is implemented in terms of accessibility: an element is accessible (with respect to a given relation) if every element less than it is also accessible. This can only terminate at minimum elements. This corresponds to the idea that for a computation to terminate, there must be a finite path to an element from which there is no way to recurse. Many instances of well-founded induction are actually induction over natural numbers that are derived from the elements being inducted over. For this purpose, the `Sized` interface and related functions are provided.
• Data.Bifoldable

  Additional utility functions for the `Bifoldable` interface.
• Data.Bits
• Data.Bool
• Data.Bool.Decidable
• Data.Bool.Xor
• Data.Buffer
• Data.Colist
• Data.Colist1
• Data.Contravariant
• Data.Double

  Various IEEE floating-point number constants
• Data.DPair
• Data.Either
• Data.Fin
• Data.Fin.Arith

  Result-type changing `Fin` arithmetics
• Data.Fin.Order

  Implementation of ordering relations for `Fin`ite numbers
• Data.Fin.Properties

  Some properties of functions defined in `Data.Fin`
• Data.Fin.Split

  Splitting operations and their properties
• Data.Fuel
• Data.Fun
• Data.IOArray
• Data.IOArray.Prims
• Data.IORef
• Data.Integral
• Data.List
• Data.List.AtIndex

  Indexing into Lists. `Elem` proofs give existential quantification that a given element *is* in the list, but not where in the list it is! Here we give a predicate that presents proof that a given index in a list, given by a natural number, will return a certain element.
• Data.List.Elem
• Data.List.HasLength

  This module implements a relation between a natural number and a list. The relation witnesses the fact the number is the length of the list. It is meant to be used in a runtime-irrelevant fashion in computations manipulating data indexed over lists where the computation actually only depends on the length of said lists. Instead of writing: ```idris example f0 : (xs : List a) -> P xs ``` We would write either of: ```idris example f1 : (n : Nat) -> (0 _ : HasLength n xs) -> P xs f2 : (n : Subset n (flip HasLength xs)) -> P xs ``` See `sucR` for an example where the update to the runtime-relevant Nat is O(1) but the update to the list (were we to keep it around) an O(n) traversal.
• Data.List.Lazy
• Data.List.Lazy.Quantifiers

  WIP: same as Data.List.Quantifiers but for lazy lists
• Data.List.Quantifiers
• Data.List.Views
• Data.List1
• Data.List1.Elem
• Data.List1.Properties

  This module contains stuff that may use functions from `Data.List`. This separation is needed because `Data.List` uses `List1` type inside it, thus the core of `List1` must not import `Data.List`.
• Data.List1.Quantifiers
• Data.Maybe
• Data.Morphisms
• Data.Nat
• Data.Nat.Order

  Implementation of ordering relations for `Nat`ural numbers
• Data.Nat.Order.Properties

  Additional properties/lemmata of Nats involving order
• Data.Nat.Views
• Data.OpenUnion

  This module is inspired by the open union used in the paper Freer Monads, More Extensible Effects by Oleg Kiselyov and Hiromi Ishii By using an AtIndex proof, we are able to get rid of all of the unsafe coercions in the original module.
• Data.Primitives.Interpolation
• Data.Primitives.Views
• Data.Ref
• Data.Rel
• Data.Singleton
• Data.SnocList

  A Reversed List
• Data.SnocList.Elem
• Data.SnocList.HasLength
• Data.SnocList.Operations

  Operations on `SnocList`s, analogous to the `List` ones. Depending on your style of programming, these might cause ambiguities, so import with care
• Data.SnocList.Quantifiers
• Data.So
• Data.SortedMap
• Data.SortedMap.Dependent
• Data.SortedSet
• Data.Stream
• Data.String
• Data.These
• Data.Vect
• Data.Vect.AtIndex

  Indexing Vectors. `Elem` proofs give existential quantification that a given element *is* in the list, but not where in the list it is! Here we give a predicate that presents proof that a given index of a vector, given by a `Fin` instance, will return a certain element. Two decidable decision procedures are presented: 1. Check that a given index points to the provided element in the presented vector. 2. Find the element at the given index in the presented vector.
• Data.Vect.Elem
• Data.Vect.Quantifiers
• Data.Vect.Views

  Views for Vect
• Data.Void
• Data.Zippable
• Debug.Trace
• Decidable.Decidable
• Decidable.Equality
• Decidable.Equality.Core
• Deriving.Common
• Deriving.Foldable

  Deriving foldable instances using reflection You can for instance define: ``` data Tree a = Leaf a | Node (Tree a) (Tree a) treeFoldable : Foldable Tree treeFoldable = %runElab derive ```
• Deriving.Functor

  Deriving functor instances using reflection You can for instance define: ``` data Tree a = Leaf a | Node (Tree a) (Tree a) treeFunctor : Functor Tree treeFunctor = %runElab derive ```
• Deriving.Show

  Deriving show instances using reflection You can for instance define: ``` data Tree a = Leaf a | Node (Tree a) (Tree a) treeShow : Show a => Show (Tree a) treeShow = %runElab derive ```
• Deriving.Traversable

  Deriving traversable instances using reflection You can for instance define: ``` data Tree a = Leaf a | Node (Tree a) (Tree a) treeFoldable : Traversable Tree treeFoldable = %runElab derive ```
• Language.Reflection
• Language.Reflection.TT
• Language.Reflection.TTImp
• Syntax.PreorderReasoning

  Until Idris2 starts supporting the 'syntax' keyword, here's a poor-man's equational reasoning
• Syntax.PreorderReasoning.Ops
• Syntax.PreorderReasoning.Generic
• Syntax.WithProof
• System
• System.Clock

  Types and functions for reasoning about time.
• System.Concurrency

  Concurrency primitives, e.g. threads, mutexes, etc. N.B.: At the moment this is pretty fundamentally tied to the Scheme RTS. Given that different back ends will have entirely different threading models, it might be unavoidable, but we might want to think about possible primitives that back ends should support.
• System.Directory

  Directory access and handling.
• System.Errno

  Managing error codes.
• System.Escape
• System.FFI

  Additional FFI help for more interesting C types
• System.File
• System.File.Buffer
• System.File.Error
• System.File.Handle
• System.File.Meta

  Functions for accessing file metadata.
• System.File.Mode
• System.File.Permissions
• System.File.Process
• System.File.ReadWrite
• System.File.Support
• System.File.Types
• System.File.Virtual

  Magic/Virtual files
• System.Info

  Miscellaneous functions for getting information about the system.
• System.REPL
• System.Signal

  Signal raising and handling. NOTE that there are important differences between what can be done out-of-box in Windows and POSIX based operating systems. This module tries to honor both by putting things only available in POSIX environments into appropriately named namespaces or data types.
• System.Term