Tealeaves
Index
Table of Contents
Switch to Coqdocs
List of Links
Tealeaves/Axioms
Tealeaves/Tactics/Debug
Tealeaves/Tactics/LibTactics
Tealeaves/Tactics/Prelude
Tealeaves/Misc/Product
Tealeaves/Classes/EqDec_eq
Tealeaves/Classes/Category
Tealeaves/Classes/Monoid
Tealeaves/Classes/Comonoid
Tealeaves/Misc/Iterate
Tealeaves/Misc/NaturalNumbers
Tealeaves/Misc/Prop
Tealeaves/Classes/Functor
Tealeaves/Functors/Identity
Tealeaves/Functors/Compose
Tealeaves/Misc/Strength
Tealeaves/Classes/Categorical/Applicative
Tealeaves/Classes/Categorical/ApplicativeCommutativeIdempotent
Tealeaves/Classes/Categorical/Monad
Tealeaves/Classes/Categorical/Comonad
Tealeaves/Classes/Categorical/BeckDistributiveLaw
Tealeaves/Classes/Categorical/Bimonad
Tealeaves/Classes/Categorical/RightModule
Tealeaves/Classes/Categorical/RightComodule
Tealeaves/Classes/Categorical/ParamComonad
Tealeaves/Classes/Kleisli/Applicative
Tealeaves/Classes/Kleisli/Monad
Tealeaves/Classes/Kleisli/Comonad
Tealeaves/Adapters/CategoricalToKleisli/Monad
Tealeaves/Adapters/KleisliToCategorical/Monad
Tealeaves/Adapters/Roundtrips/Monad
Tealeaves/Functors/Early/Reader
Tealeaves/Classes/Categorical/DecoratedFunctor
Tealeaves/Classes/Kleisli/DecoratedFunctor
Tealeaves/Adapters/CategoricalToKleisli/Comonad
Tealeaves/Adapters/CategoricalToKleisli/DecoratedFunctor
Tealeaves/Adapters/KleisliToCategorical/DecoratedFunctor
Tealeaves/Adapters/Roundtrips/DecoratedFunctor
Tealeaves/Functors/Early/Writer
Tealeaves/Classes/Categorical/DecoratedMonad
Tealeaves/Classes/Kleisli/DecoratedMonad
Tealeaves/Adapters/CategoricalToKleisli/DecoratedMonad
Tealeaves/Adapters/KleisliToCategorical/DecoratedMonad
Tealeaves/Adapters/Roundtrips/DecoratedMonad
Tealeaves/Classes/Categorical/TraversableFunctor
Tealeaves/Classes/Kleisli/TraversableFunctor
Tealeaves/Classes/Kleisli/TraversableCommIdemFunctor
Tealeaves/Functors/Early/Batch
Tealeaves/Classes/Coalgebraic/TraversableFunctor
Tealeaves/Adapters/CategoricalToKleisli/TraversableFunctor
Tealeaves/Adapters/KleisliToCategorical/TraversableFunctor
Tealeaves/Adapters/CoalgebraicToKleisli/TraversableFunctor
Tealeaves/Adapters/KleisliToCoalgebraic/TraversableFunctor
Tealeaves/Adapters/Roundtrips/TraversableFunctor
Tealeaves/Classes/Categorical/TraversableMonad
Tealeaves/Classes/Kleisli/TraversableMonad
Tealeaves/Classes/Coalgebraic/TraversableMonad
Tealeaves/Adapters/CategoricalToKleisli/TraversableMonad
Tealeaves/Adapters/KleisliToCategorical/TraversableMonad
Tealeaves/Adapters/CoalgebraicToKleisli/TraversableMonad
Tealeaves/Adapters/KleisliToCoalgebraic/TraversableMonad
Tealeaves/Adapters/Roundtrips/TraversableMonad
Tealeaves/Classes/Categorical/DecoratedTraversableFunctor
Tealeaves/Classes/Kleisli/DecoratedTraversableFunctor
Tealeaves/Classes/Kleisli/DecoratedTraversableCommIdemFunctor
Tealeaves/Classes/Coalgebraic/DecoratedTraversableFunctor
Tealeaves/Adapters/CategoricalToKleisli/DecoratedTraversableFunctor
Tealeaves/Adapters/KleisliToCategorical/DecoratedTraversableFunctor
Tealeaves/Adapters/CoalgebraicToKleisli/DecoratedTraversableFunctor
Tealeaves/Adapters/KleisliToCoalgebraic/DecoratedTraversableFunctor
Tealeaves/Adapters/Roundtrips/DecoratedTraversableFunctor
Tealeaves/Classes/Kleisli/DecoratedTraversableMonad
Tealeaves/Classes/Categorical/DecoratedTraversableMonad
Tealeaves/Classes/Coalgebraic/DecoratedTraversableMonad
Tealeaves/Adapters/CategoricalToKleisli/DecoratedTraversableMonad
Tealeaves/Adapters/KleisliToCategorical/DecoratedTraversableMonad
Tealeaves/Adapters/KleisliToCoalgebraic/DecoratedTraversableMonad
Tealeaves/Adapters/CoalgebraicToKleisli/DecoratedTraversableMonad
Tealeaves/Adapters/Roundtrips/DecoratedTraversableMonad
Tealeaves/Adapters/Compositions/DecoratedTraversableModule
Tealeaves/Adapters/MonadToApplicative
Tealeaves/Categories/Type
Tealeaves/Categories/TypeFamily
Tealeaves/Categories/DecoratedFunctor
Tealeaves/Categories/TraversableFunctor
Tealeaves/Categories/DecoratedTraversableFunctor
Tealeaves/Functors/Early/Subset
Tealeaves/Classes/Categorical/ContainerFunctor
Tealeaves/Classes/Kleisli/ContainerMonad
Tealeaves/Functors/Early/Ctxset
Tealeaves/Classes/Kleisli/DecoratedContainerFunctor
Tealeaves/Classes/Kleisli/DecoratedContainerMonad
Tealeaves/Functors/Early/List
Tealeaves/Classes/Categorical/ShapelyFunctor
Tealeaves/Functors/Early/Environment
Tealeaves/Classes/Kleisli/DecoratedShapelyFunctor
Tealeaves/Functors/Backwards
Tealeaves/Functors/Constant
Tealeaves/Functors/ProductFunctor
Tealeaves/Functors/Diagonal
Tealeaves/Classes/Kleisli/Theory/TraversableFunctor
Tealeaves/Classes/Categorical/Theory/TraversableFunctor
Tealeaves/Classes/Kleisli/Theory/TraversableCommutativeIdempotent
Tealeaves/Classes/Kleisli/Theory/ContainerMonad
Tealeaves/Classes/Kleisli/Theory/TraversableMonad
Tealeaves/Classes/Kleisli/Theory/DecoratedContainerFunctor
Tealeaves/Classes/Kleisli/Theory/DecoratedTraversableFunctor
Tealeaves/Classes/Kleisli/Theory/DecoratedContainerMonad
Tealeaves/Classes/Kleisli/Theory/DecoratedTraversableMonad
Tealeaves/Functors/Ctxset
Tealeaves/Functors/List
Tealeaves/Functors/Environment
Tealeaves/Functors/Option
Tealeaves/Functors/Pathspace
Tealeaves/Functors/Pair
Tealeaves/Functors/Reader
Tealeaves/Functors/State
Tealeaves/Functors/Store
Tealeaves/Functors/Subset
Tealeaves/Functors/Writer
Tealeaves/Functors/ListHistory
Tealeaves/Functors/Vector
Tealeaves/Functors/KStore
Tealeaves/Functors/VectorRefinement
Tealeaves/Functors/Batch
Tealeaves/Adapters/Isomorphisms/BatchtoKStore
Tealeaves/Theory/TraversableFunctor
Tealeaves/Theory/TraversableMonad
Tealeaves/Theory/DecoratedTraversableFunctor
Tealeaves/Theory/DecoratedTraversableMonad
Tealeaves/Theory/LiftRel/TraversableFunctor
Tealeaves/Theory/LiftRel/DecoratedTraversableFunctor
Tealeaves/Functors/List_Telescoping
Tealeaves/Classes/Multisorted/Multifunctor
Tealeaves/Classes/Multisorted/DecoratedTraversableMonad
Tealeaves/Functors/Multisorted/Batch
Tealeaves/Adapters/KleisliToCoalgebraic/Multisorted/DTM
Tealeaves/Classes/Multisorted/Theory/Container
Tealeaves/Classes/Multisorted/Theory/Targeted
Tealeaves/Classes/Multisorted/Theory/Foldmap
Tealeaves/Theory/Multisorted/DecoratedTraversableMonad
Tealeaves/Simplification/Support
Tealeaves/Simplification/Binddt
Tealeaves/Simplification/DeriveDTM
Tealeaves/Simplification/Simplification
Tealeaves/Simplification/MBinddt
Tealeaves/Simplification/Tests/Support
Tealeaves/Backends/LN/LN
Tealeaves/Backends/LN/Simplification
Tealeaves/Backends/LN/Parallel
Tealeaves/Backends/LN
Tealeaves/Backends/Multisorted/LN/LN
Tealeaves/Backends/Multisorted/LN
Tealeaves/Backends/DB/DB
Tealeaves/Backends/DB/Simplification
Tealeaves/Backends/DB/AutosubstShim
Tealeaves/Backends/DB
Tealeaves/Misc/PartialBijection
Tealeaves/Backends/Adapters/Key
Tealeaves/Backends/Adapters/LNtoDB
Tealeaves/Backends/Adapters/DBtoLN
Tealeaves/Backends/Adapters/Roundtrips/LNDB
Tealeaves/Backends/Common/Names
Tealeaves/Backends/Common/AtomSet
Tealeaves/Backends/Common/AssocList
Tealeaves/Adapters/MonoidHom/DecoratedTraversableMonad
Tealeaves/Examples/Lambda/Confluence
Tealeaves/Examples/Lambda/MapWithPolicyDemo
Tealeaves/Examples/JAR/TranslateDemo
Tealeaves/Examples/STLC/Syntax
Tealeaves/Examples/STLC/CompatTest
Tealeaves/Examples/STLC/SyntaxCategorical
Tealeaves/Examples/STLC/TypeSoundness
Tealeaves/Simplification/Tests/STLC_Binddt
Tealeaves/Simplification/Tests/STLC_Container
Tealeaves/Simplification/Tests/STLC_LN
Tealeaves/Simplification/Tests/STLC_DB
Tealeaves/Examples/VariadicLet/Terms
Tealeaves/Examples/VariadicLet/Instances/Simple
Tealeaves/Examples/VariadicLet/Instances/Tele
Tealeaves/Examples/VariadicLet/Instances/LetRec
Tealeaves/Examples/VariadicLet/Demo
Tealeaves/Examples/SystemF/Syntax
Tealeaves/Examples/SystemF/Contexts
Tealeaves/Examples/SystemF/TypeSoundness
Tealeaves/Simplification/Tests/SystemF_Binddt
Tealeaves/Simplification/Tests/SystemF_Targeted
Tealeaves/Simplification/Tests/SystemF_LN