## Tealeaves.Util.LibTactics

## Tealeaves.Util.EqDec_eq

## Tealeaves.Util.Prelude

- Some useful automation
- Support for rewriting the left/right side of equations
- Support for reasoning with extensionality
- Support for re-association of expressions
- Support for rewriting functions as compositions
- Support for comparing naturals
- Support for decidable equalities
- Support for rewriting with setoids
- General logical reasoning suport

- Support for unfolding operational typeclasses

## Tealeaves.Util.Product

## Tealeaves.Classes.Category

## Tealeaves.Classes.Monoid

## Tealeaves.Classes.Functor

## Tealeaves.Classes.Applicative

- Applicative functors
- The "ap" combinator
`<⋆>`

- Applicative functors form a monoidal category
- Cartesian product of applicative functors
- Notations

## Tealeaves.Classes.Monad

- Monads
- Kleisli presentation of monads
- The identity monad
- Miscellaneous properties
- Equivalence between monads and Kleisli triples
- Monadic applicative functors
- Notations

## Tealeaves.Classes.Comonad

## Tealeaves.Classes.RightModule

## Tealeaves.Classes.RightComodule

## Tealeaves.Classes.BeckDistributiveLaw

## Tealeaves.Classes.Bimonad

## Tealeaves.Functors.Writer

## Tealeaves.Classes.DecoratedFunctor

- Decorated functors
- The shift operation
- Decorated functors form a monoidal category
- Decorated functor instance for Writer
- Kleisli presentation of decorated functors
- Miscellaneous properties of decorated functors

## Tealeaves.Classes.DecoratedMonad

- Basic properties of shift on monads
- Decorated monads
- Kleisli presentation of decorated monads
- Notations

## Tealeaves.Classes.DecoratedModule

- Basic properties of shift on modules
- Decorated right modules
- Kleisli presentation of decorated modules

## Tealeaves.Theory.Decorated

- A decorated functor is precisely a right comodule of
`prod W`

- Decorated monads in terms of homomorphisms
- Pushing decorations through a monoid homomorphism

## Tealeaves.Functors.Sets

## Tealeaves.Classes.SetlikeFunctor

## Tealeaves.Classes.SetlikeMonad

## Tealeaves.Classes.SetlikeModule

## Tealeaves.Functors.List

- list monoid
- list functor
- list monad
- list is set-like
- Folding over lists
`fmap`

equality inversion lemmas

## Tealeaves.Classes.ListableFunctor

- The shape operation
- Listable functors
- Properties of
`shape`

- Listable functors form a monoidal category
- Respectfulness conditions for listable functors
- Properties of listable functors
- fold and foldMap operations
- Decorated listable functors

## Tealeaves.Classes.ListableMonad

## Tealeaves.Classes.ListableModule

- Listable modules
- Listable right modules are set-like
- Respectfulness conditions for listable modules
- Non-collapse of right actions

## Tealeaves.Theory.Listable

- Characterizations of listable monad compatibility conditions
- A counter-example of a respectfulness property.

## Tealeaves.Functors.Constant

## Tealeaves.Classes.TraversableFunctor

- Traversable functors
- Monoid structure of traversable functors
- Basic properties of traversable functors
- Kleisi presentation of traversable functors
- Characterization of distribution w.r.t. (F ◻ G)
- Traversable functors are listable
- Traversable instance for list
- Traversable instance for
`prod`

- Respectfulness properties
- Notations

## Tealeaves.Classes.TraversableMonad

- Traversable monads
- Kleisli-style presentation of traversable monads
- Instance for list
- Traversable monads are listable
- Notations

## Tealeaves.Classes.TraversableModule

- Traversable right modules
- Kleisli-style presentation of traversable monads
- Traversable modules are listable

## Tealeaves.Classes.DecoratedTraversableFunctor

## Tealeaves.Classes.DecoratedTraversableMonad

- Decorated-traversable monads
- Kleisli presentation of D-T monads
- Lifting operation
`binddt`

and Kleisli composition - Specifications for sub-operations
- Functoriality of binddt
- Kleisli composition laws
- Composition with sub-operations
- Re-statement of inherited composition properties for bindd
- Re-statement of inherited composition properties for bindt
- Purity laws for binddt
- Respectfulness properties

- Lifting operation
- Notations

## Tealeaves.Classes.DecoratedTraversableModule

## Tealeaves.Functors.Maybe

## Tealeaves.Functors.State

## Tealeaves.Functors.Diagonal

## Tealeaves.Functors.Pathspace

## Tealeaves.Theory.Category

## Tealeaves.LN.Atom

## Tealeaves.LN.Leaf

## Tealeaves.LN.AtomSet

## Tealeaves.LN.AssocList

- Miscellaneous
- The
`alist`

functor - Specifications for operations on association lists
- Specifications for
`∈`

and alist operations - Specifications for ∈ and
`envmap`

- Rewriting principles for envmap
- Rewriting lemmas for dom
- Rewriting lemmas for domset
- Rewriting lemmas for range
- Rewriting principles for ∈
- Tactical lemmas for ∈
- Rewriting principles for disjoint
- Tactical lemmas for disjoint
- Tactical lemmas for uniq
- Rewriting principles for uniq
- More facts about uniq
- Stronger theorems for
`∈`

on uniq lists

- Specifications for
- Facts about binds
- Tactic support for picking fresh atoms

## Tealeaves.LN.Operations

## Tealeaves.LN.Theory

- Lemmas for local reasoning
- Locally nameless metatheory
- Leaf analysis: substitution with contexts
- Leaf analysis: substitution without contexts
- Free variables after substitution
- Upper and lower bounds for leaves after substitution
- Substitution of fresh variables
- Composing substitutions
- Commuting two substitutions
- Local closure is preserved by substitution
- Decompose substitution into closing/opening
- Substitution when
`u`

is a leaf - Substitution by the same variable is the identity
- Free variables after variable closing
- Variable closing and local closure
- Upper and lower bounds on free variables after opening
- Opening a locally closed term is the identity
- Opening followed by substitution
- Decompose opening into variable opening followed by substitution
- Opening by a variable, followed by non-equal substitution
- Closing, followed by opening
- Opening by a leaf reduces to an fmapkr
- Opening, followed by closing
- Opening and local closure

## Tealeaves.LN.Environment

## Tealeaves.Examples.STLC.Language

- Language definition
- Functor instance
- Monad instance
- Decorated instance
- Traversable instance
- Listable instance (redundant)
- Compatibility between decoration and traversal
- Locally nameless operations
- Rewriting lemmas for high-level operations
- Typing judgments for STLC