ExtLib.ExtLib

ExtLib.Tactics

ExtLib.Core.Any

ExtLib.Core.CmpDec

ExtLib.Core.EquivDec

ExtLib.Core.RelDec

ExtLib.Core.Decision

ExtLib.Structures.Applicative

ExtLib.Structures.BinOps

ExtLib.Structures.CoFunctor

ExtLib.Structures.CoMonad

ExtLib.Structures.CoMonadLaws

ExtLib.Structures.EqDep

ExtLib.Structures.Foldable

ExtLib.Structures.FunctorLaws

ExtLib.Structures.Functor

ExtLib.Structures.Maps

ExtLib.Structures.MonadCont

ExtLib.Structures.MonadExc

ExtLib.Structures.MonadFix

ExtLib.Structures.MonadLaws

• • of domain theory. It generalizes the usual equivalence relation by,
  • enabling the relation to talk about computations that are "more defined"
  • than others.
  • This generalization is done to support the fixpoint law.

ExtLib.Structures.MonadPlus

ExtLib.Structures.MonadReader

ExtLib.Structures.MonadState

ExtLib.Structures.Monads

ExtLib.Structures.MonadTrans

ExtLib.Structures.Monad

ExtLib.Structures.MonadWriter

ExtLib.Structures.MonadZero

ExtLib.Structures.Monoid

ExtLib.Structures.Reducible

ExtLib.Structures.Sets

ExtLib.Structures.Traversable

ExtLib.Data.Bool

ExtLib.Data.Char

ExtLib.Data.Checked

ExtLib.Data.Eq

ExtLib.Data.Eq.UIP_trans

• • in the Coq standard library. It is duplicated so that the definitions
  • can be made transparent, and therefore computable.
  • See Coq.Logic.Eqdep_dec for complete information

ExtLib.Data.Fin

• • i.e. a finite set of size n

ExtLib.Data.Fun

ExtLib.Data.HList

• • This is weak because it does not change the key type

ExtLib.Data.LazyList

ExtLib.Data.Lazy

• • be beta-delta reduced.

ExtLib.Data.ListFirstnSkipn

ExtLib.Data.ListNth

ExtLib.Data.List

ExtLib.Data.Member

ExtLib.Data.Nat

ExtLib.Data.N

ExtLib.Data.Option

ExtLib.Data.Pair

ExtLib.Data.Positive

ExtLib.Data.PreFun

ExtLib.Data.Prop

ExtLib.Data.SigT

ExtLib.Data.Stream

ExtLib.Data.String

ExtLib.Data.SumN

ExtLib.Data.Sum

ExtLib.Data.Tuple

ExtLib.Data.Unit

ExtLib.Data.Vector

ExtLib.Data.Z

ExtLib.Data.POption

ExtLib.Data.PList

ExtLib.Data.PPair

ExtLib.Generic.Data

ExtLib.Generic.DerivingData

ExtLib.Generic.Func

ExtLib.Generic.Ind

ExtLib.Programming.Eqv

ExtLib.Programming.Extras

ExtLib.Programming.Injection

ExtLib.Programming.Le

ExtLib.Programming.Show

ExtLib.Programming.With

ExtLib.Recur.Facts

ExtLib.Recur.GenRec

ExtLib.Recur.Measure

ExtLib.Recur.Relation

ExtLib.Relations.Compose

ExtLib.Relations.TransitiveClosure

ExtLib.Tactics.BoolTac

ExtLib.Tactics.Cases

• • are matched on. It only does this on terms where only
  • one of the cases is non-trivial (i.e. by intuition congruence).

ExtLib.Tactics.Consider

• • decision procedures when they are implemented as functions into bool.
  • Implementation by Thomas Braibant (thomas.braibant@gmail.com)

ExtLib.Tactics.EqDep

ExtLib.Tactics.Equality

ExtLib.Tactics.Forward

ExtLib.Tactics.Injection

ExtLib.Tactics.MonadTac

ExtLib.Tactics.Parametric

• • for functions

ExtLib.Tactics.Reify

ExtLib.Tactics.Hide

ExtLib.Data.Graph.BuildGraph

ExtLib.Data.Graph.GraphAdjList

ExtLib.Data.Graph.GraphAlgos

ExtLib.Data.Graph.Graph

ExtLib.Data.Map.FMapAList

ExtLib.Data.Map.FMapPositive

ExtLib.Data.Map.FMapTwoThreeK

ExtLib.Data.Monads.ContMonad

ExtLib.Data.Monads.EitherMonad

ExtLib.Data.Monads.FuelMonadLaws

ExtLib.Data.Monads.FuelMonad

• • it encapsulates the "gas" that is used as the measure

ExtLib.Data.Monads.IdentityMonadLaws

ExtLib.Data.Monads.IdentityMonad

ExtLib.Data.Monads.ListMonad

ExtLib.Data.Monads.OptionMonadLaws

ExtLib.Data.Monads.OptionMonad

ExtLib.Data.Monads.ReaderMonadLaws

ExtLib.Data.Monads.ReaderMonad

ExtLib.Data.Monads.StateMonad

ExtLib.Data.Monads.WriterMonad

• • which yields the `writer` monad.

ExtLib.Data.Set.ListSet

ExtLib.Data.Set.SetMap

• • are unit

ExtLib.Data.Set.TwoThreeTrees