Tealeaves.Axioms

Tealeaves.Tactics.Debug

Tealeaves.Tactics.CoreTactics

• • Introduction
  • Proving Equalities

Tealeaves.Tactics.Prelude

• General Purpose Operations
• General Purpose Tactics
  • Reasoning with Extensionality
  • Support for Rewriting
  • Unfolding Operational Typeclasses
  • Support for Comparing Natural Numbers
  • Miscellaneous

Tealeaves.Misc.Product

• Monoidal Category-Theoretic Structure on Type
  • Reassociating Cartesian Products
  • Notations
  • Monoidal Category Theory Laws
  • Currying and Uncurrying
  • Deletions/Projections
  • Miscellaneous
  • Commuting Maps

Tealeaves.Classes.EqDec_eq

• Types with Decidable Equality
  • Tactics for Comparing Elements

Tealeaves.Classes.Category

• Categories
  • Operational Typeclasses
  • Notations
  • Category Typeclass
• Functors
  • Natural Transformations
  • Monoidal Structure on Endofunctors
• Monads and Right Modules
  • Monad Operations
  • Monad Typeclass
  • Right Modules
  • The bind Operation

Tealeaves.Classes.Monoid

• Monoids
  • Operational typeclasses
  • Monoid typeclass
  • Monoid homomorphsims
  • Some Rudimentary Automation
• Monoid Constructions
  • Cartesian Product of Monoids
  • The Opposite Monoid
• Increment and Pre-increment
  • The incr Operation
  • The preincr Operation
• Preordered Monoids
• Opposite Monoid
• Commutative Monoids
  • Opposite of a Commutative Monoid
• Idempotent Monoids
• Notations

Tealeaves.Classes.Comonoid

• Comonoids
  • Operational Typeclasses
  • Typeclass
• The "Duplicate" Comonoid

Tealeaves.Misc.Iterate

• Iterating Functions
  • Rewriting Rules

Tealeaves.Misc.NaturalNumbers

• Natural Numbers with Addition
• Natural Numbers with Maximum

Tealeaves.Misc.Prop

• Propositional monoids
  • Disjunction
  • Conjunction
  • Simplification Support
• Boolean monoids
  • Disjunction
  • Conjunction

Tealeaves.Classes.Functor

• Endofunctors
  • The map Operation
• Functor Typeclass
  • Natural transformations
• Notations

Tealeaves.Functors.Identity

• The Identity Functor

Tealeaves.Functors.Compose

• The Composition of Two Functors
  • Composition with the Identity Functor
  • Composition of Natural Transformations

Tealeaves.Misc.Strength

• Tensorial Strength
• Notations

Tealeaves.Classes.Categorical.Applicative

• Applicative Functors
  • Homomorphisms Between Applicative Functors
  • Basic Lemmas
  • Mapping and Reassociating ⊗
• The Category of Applicative Functors
  • The Identity Applicative Functor
  • Composition of Applicative Functors
  • Composition with the Identity Functor
  • Parallel Composition of Applicative Homomorphisms
• The "ap" combinator <⋆>
  • Convenience Laws for ap
  • Composition of Functors and ap / <⋆>
• Monoids as Constant Applicative Functors
  • Monoids Homomorphisms as Applicative Homomorphisms
• Notations

Tealeaves.Classes.Categorical.ApplicativeCommutativeIdempotent

• Commutative and Idempotent Elements and Functors
  • The Center of an Applicative Functor
  • The Idempotent and Central Elements of an Applicative Functor
  • pure is always CI
  • Everything is always CI for (fun A => A)
  • Rewriting Laws for C-I Elements
  • Commutative Idempotent Applicative Functors
  • Rewriting Laws for C-I Applicative Funtors

Tealeaves.Classes.Categorical.Monad

• Monads
  • Operations join and ret
  • Typeclass
  • Monad Homomorphisms
  • The Identity Monad
  • Miscellaneous Properties
• Notations

Tealeaves.Classes.Categorical.Comonad

• Comonads
  • Operations cojoin and extract
  • Typeclass
• Notations

Tealeaves.Classes.Categorical.BeckDistributiveLaw

• Beck Distribution Laws
• Beck Distributive Laws Induce a Composite Monad

Tealeaves.Classes.Categorical.Bimonad

• Bimonad typeclass
• Kleisli lifting operation bibind

Tealeaves.Classes.Categorical.RightModule

• Right modules
  • Operation
  • Typeclass
• Coercing Monads into Right Modules
  • Right Modules Compose with Functors

Tealeaves.Classes.Categorical.RightComodule

• Right Comodules
  • Operation right_coaction
  • Typeclass
  • Homomorphisms of Right Comodules
  • Coercing a Comonads to a Right Comodule

Tealeaves.Classes.Categorical.ParamComonad

• Parameterized comonads

Tealeaves.Classes.Kleisli.Applicative

• Applicative Functors
  • Derived Categorical Applicative Functor

Tealeaves.Classes.Kleisli.Monad

• Monads
  • Operations
  • Kleisli Composition
  • Typeclasses
  • Kleisli Category Laws
  • Monad Homomorphisms
• Derived Structures
  • Derived Operations
  • Derived Kleisli Composition laws
  • Derived Composition Laws
  • Derived Typeclass Instances
  • Naturality Properties
• Notations

Tealeaves.Classes.Kleisli.Comonad

• Comonads
  • Operations
  • Co-Kleisli Composition
  • Typeclasses
  • Kleisli Category Laws
  • Comonad Homomorphisms
• Derived Structures
  • Derived Operations
  • Derived Kleisli Composition Laws
  • Derived Typeclass Instances
• Notations

Tealeaves.Adapters.CategoricalToKleisli.Monad

• Categorical Monad to Kleisli Monad
  • Derived bind Operation
  • Derived bind is Compatible with Original <map>>
  • join as id ⋆ id
  • Derived Kleisli Monad Laws
• Right modules
  • Specification for map

Tealeaves.Adapters.KleisliToCategorical.Monad

• Kleisli Monads to Categorical Monads
  • Derived join Operation
  • Derived Categorical Laws

Tealeaves.Adapters.Roundtrips.Monad

• Categorical ~> Kleisli ~> Categorical
• Kleisli ~> Categorical ~> Kleisli

Tealeaves.Functors.Early.Reader

• Environment/Reader Comonad
  • Functor Instances
  • Categorical Comonad Instance
  • Kleisli Comonad Instance
• Properties of strength
  • Interaction with Categorical Monad Operations
  • Interaction with Reader Comonad Operations
  • Miscellaneous Properties

Tealeaves.Classes.Categorical.DecoratedFunctor

• Decorated functors
  • Operations
  • Typeclass
  • Decoration-preserving natural transformations
  • Decoration-preserving natural transformation, generalized
• Decorated functor instance for Reader

Tealeaves.Classes.Kleisli.DecoratedFunctor

• Decorated Functors
  • mapd Operation
  • Kleisli Composition
  • Typeclasses
  • Homomorphisms between Decorated Functors
• Derived Structures
  • Derived Operations
  • Derived Composition Laws
  • Derived Typeclass Instances
• Instance for Reader

Tealeaves.Adapters.CategoricalToKleisli.Comonad

• Comonad to Kleisli comonad
  • Derived cobind Operation
  • cojoin as id ⋆1 id
  • Derived co-Kleisli Laws
  • Typeclass Instance

Tealeaves.Adapters.CategoricalToKleisli.DecoratedFunctor

• Categorical Decorated Functors to Kleisli Decorated Functors
  • Derived mapd Operation
  • Compatibility Classes
  • Interaction of dec with mapd
  • Derived co-Kleisli Laws
  • Typeclass Instance
  • Miscellaneous Properties

Tealeaves.Adapters.KleisliToCategorical.DecoratedFunctor

• Categorical Decorated Functors to Kleisli Decorated Functors
  • Derived mapd Operation
  • Compatibility Classes
  • Derived Decorated Functor Laws

Tealeaves.Adapters.Roundtrips.DecoratedFunctor

• Categorical ~> Kleisli ~> Categorical
• Kleisli ~> Categorical ~> Kleisli

Tealeaves.Functors.Early.Writer

• Writer monad
  • Categorical instance
  • Tensor Strength Makes any T ∘ (W ×) a Monad
  • Writer Bimonad Instances
  • Kleisli Monad Instance
  • Miscellaneous Properties

Tealeaves.Classes.Categorical.DecoratedMonad

• The shift operation
  • Basic Properties of shift
• Decorated Monads
• Decorated Right Modules
• Basic Properties of shift on Monads
  • Helper Lemmas for Proving Typeclass Instances
• Pushing Decorations through a Monoid Homomorphism

Tealeaves.Classes.Kleisli.DecoratedMonad

• Decorated Monads
  • Operation bindd
  • Kleisli Composition
  • Typeclass
  • Kleisli Category Laws
  • Decorated Monad Homomorphisms
• Derived Structures
  • Derived Operations
  • Derived Kleisli Composition Laws
  • Derived Composition Laws
  • Derived Typeclass Instances
• Instance for Writer
• Notations

Tealeaves.Adapters.CategoricalToKleisli.DecoratedMonad

• Categorical Decorated Monad to Kleisli Decorated Monad
  • Derived bindd Operation
  • Derived Laws
  • Typeclass Instances

Tealeaves.Adapters.KleisliToCategorical.DecoratedMonad

• Categorical Decorated monads from Kleisli Decorated Monads
  • Operations
  • Derived Laws

Tealeaves.Adapters.Roundtrips.DecoratedMonad

• Categorical ~> Kleisli ~> Categorical
• Kleisli ~> Categorical ~> Kleisli

Tealeaves.Classes.Categorical.TraversableFunctor

• Traversable functors
  • Operation dist
  • Typeclass
  • Homomorphisms of Traversable Functors
• Basic Properties of Traversable Functors
• Notations

Tealeaves.Classes.Kleisli.TraversableFunctor

• Traversable Functors
  • Operation traverse
  • Kleisli Composition
  • Typeclass
  • Kleisli Composition Laws
  • Traversable Functor Homomorphisms
• Derived Structures
  • Derived map Operation
  • Composition with the Identity Applicative
  • Derived Composition Laws
  • Derived Typeclass Instances
• Notations

Tealeaves.Classes.Kleisli.TraversableCommIdemFunctor

• Commutative/Idempotent-Traversable Functors
  • The traverse Operation
  • Kleisli Composition
  • Typeclass

Tealeaves.Functors.Early.Batch

• The Batch Functor
  • Map Operations
  • Rewriting Principles
  • Functor Laws
  • Commuting Independent maps
  • Functoriality In the B Argument
• Applicative Functor Instance
  • Operations
  • Rewriting Principles
  • Applicative Laws
  • Typeclass Instance
  • mapfst and mapsnd as Applicative Homomorphisms
• The runBatch Operation
  • Rewriting Principles
  • Naturality of runBatch
  • runBatch as an Applicative Homomorphism
• Batch as a Parameterized Monad
  • Operations batch and join_Batch
  • join_Batch as runBatch (Batch A B) id
  • Naturality
  • join as an Applicative Homomorphism
  • Other Laws
  • Monad Laws
• Batch as a Parameterized Comonad
  • Operations extract_Batch and cojoin_Batch
  • Rewriting Principles
  • extract_Batch as runBatch (fun A => A) id
  • cojoin_Batch as runBatch double_batch
  • extract_Batch and cojoin_Batch as Applicative Homomorphisms
  • Composition with ret/batch
  • Naturality
  • Comonad Laws
• Batch is Traversable in the First Argument
  • Rewriting Principles
  • Traversable Functor Laws
  • runBatch Characterized by traverse
• Notations
• Arguments

Tealeaves.Classes.Coalgebraic.TraversableFunctor

• Coalgebraic Traversable Functors
  • toBatch Operation
  • Typeclass

Tealeaves.Adapters.CategoricalToKleisli.TraversableFunctor

• Kleisli Traversable Functors from Categorical Traversable Functors
  • Derived Operations
  • Compatibility Classes
  • Derived Laws

Tealeaves.Adapters.KleisliToCategorical.TraversableFunctor

• Categorical Traversable Functors from Kleisli Traversable Functors
  • Derived Operations
  • Compatibility Classes
  • Derived Instances

Tealeaves.Adapters.CoalgebraicToKleisli.TraversableFunctor

• Categorical Traversable Monads from Kleisli Traversable Monads
  • Derived Operations
  • ⋆2 as runBatch ∘ map runBatch ∘ double_batch
  • Derived Laws
  • Typeclass Instances

Tealeaves.Adapters.KleisliToCoalgebraic.TraversableFunctor

• Coalgebraic Traversable Functors From Kleisli Traversable Functors
  • Derived ToBatch Operation
  • Derived Laws

Tealeaves.Adapters.Roundtrips.TraversableFunctor

• Categorical ~> Kleisli ~> Categorical
• Kleisli ~> Categorical ~> Kleisli
• Coalgebraic ~> Kleisli ~> Coalgebraic (TODO)
• Kleisli ~> Coalgebraic ~> Kleisli (TODO)

Tealeaves.Classes.Categorical.TraversableMonad

• Traversable monads
  • Typeclass

Tealeaves.Classes.Kleisli.TraversableMonad

• Traversable Monads
  • The bindt operation
  • Kleisli Composition
  • Typeclass
  • Kleisli Category laws
• Derived Structures
  • Derived Operations
  • Composition with the Identity Applicative
  • Derived Kleisli Composition Laws
  • Derived Composition Laws
  • Monad Laws
  • Traversable Laws
  • Derived Typeclass Instances
• Notations

Tealeaves.Classes.Coalgebraic.TraversableMonad

• Coalgebraic Traversable Monads
  • Operation toBatch6
  • Operation cojoin_Batch6
  • cojoin_Batch6 Alternate Definition
  • cojoin_Batch6 as runBatch double_batch6
  • Typeclasses

Tealeaves.Adapters.CategoricalToKleisli.TraversableMonad

• Kleisli Traversable Monads from Categorical Traversable Monads
  • Operation
  • Derived Laws
  • Typeclass Instances

Tealeaves.Adapters.KleisliToCategorical.TraversableMonad

• Categorical Traversable Monads from Kleisli Traversable Monads
  • Derived Operations
• Derived Instances
  • Monad Instance
  • Traversable Functor Instance
  • Traversable Monad Instance

Tealeaves.Adapters.CoalgebraicToKleisli.TraversableMonad

• Kleisli Traversable Monad from Kleisli Traversable Monad
  • Derived Operation toBatch6
  • ⋆6 as runBatch ∘ map runBatch ∘ double_batch6
  • Derived Laws
  • Typeclass Instances

Tealeaves.Adapters.KleisliToCoalgebraic.TraversableMonad

• Coalgebraic Traversable Monads
  • Derived Operations
  • double_batch6 as batch ⋆6 batch
  • Derived Laws
  • Typeclass Instances

Tealeaves.Adapters.Roundtrips.TraversableMonad

• Categorical ~> Kleisli ~> Categorical
• Kleisli ~> Categorical ~> Kleisli
• Coalgebraic ~> Kleisli ~> Coalgebraic
• Kleisli ~> Coalgebraic ~> Kleisli

Tealeaves.Classes.Categorical.DecoratedTraversableFunctor

• Decorated Traversable Functors
  • Typeclass

Tealeaves.Classes.Kleisli.DecoratedTraversableFunctor

• Decorated Traversable Functor
  • Operation mapdt
  • Kleisli Composition
  • Typeclass
  • Kleisli Category Laws
• Derived Structures
  • Derived Operations
  • Composition with the Identity Applicative Functor
  • Derived Kleisli Composition Laws
  • Derived Composition Laws
  • Derived Typeclass Instances
• Notations

Tealeaves.Classes.Kleisli.DecoratedTraversableCommIdemFunctor

• CI-Decorated Traversable functor
  • The mapdt_ci Operation
  • Kleisli Composition
  • Typeclasses
  • Basic Laws
• Notations

Tealeaves.Classes.Coalgebraic.DecoratedTraversableFunctor

• Coalgebraic Decorated Traversable Functors
  • The toBatch3 Operation
  • Operation cojoin_Batch3
  • cojoin_Batch3 as runBatch double_batch3
  • Typeclass

Tealeaves.Adapters.CategoricalToKleisli.DecoratedTraversableFunctor

• Kleisli DTFs from Categorical DTFs
  • Derived Operations
  • Derived Instances
  • Typeclass Instance

Tealeaves.Adapters.KleisliToCategorical.DecoratedTraversableFunctor

• Categorical DTFs from Kleisli DTFs
  • Derived Operations
  • Derived Instances
  • Typeclass Instance

Tealeaves.Adapters.CoalgebraicToKleisli.DecoratedTraversableFunctor

• Coalgebraic DTFs to Kleisli DTFs
  • Derived Operations
  • ⋆3 as runBatch ∘ map runBatch ∘ double_batch3
  • Derived Laws
  • Typeclass Instances

Tealeaves.Adapters.KleisliToCoalgebraic.DecoratedTraversableFunctor

• Coalgebraic DTFs from Kleisli DTFs
  • Derived Operations
  • double_batch3 as batch ⋆3 batch
  • Derived Laws

Tealeaves.Adapters.Roundtrips.DecoratedTraversableFunctor

• Categorical ~> Kleisli ~> Categorical
• Kleisli ~> Categorical ~> Kleisli

Tealeaves.Classes.Kleisli.DecoratedTraversableMonad

• Decorated Traversable Monads
  • Operation binddt
  • Kleisli composition
  • Typeclass
  • Homomorphisms
  • Kleisi Category Laws
• Derived Structures
  • Derived Operations
  • Compatibility Typeclasses
  • Rewriting X to binddt Lemmas
  • Composition with the Identity Applicative Functor
  • Derived Kleisli Composition Laws
  • Rewriting rules for special cases of kc7
  • Derived Composition Laws
  • Derived Identity/ret/Appl. Homomorphism Laws
  • Derived Typeclass Instances
• Notations

Tealeaves.Classes.Categorical.DecoratedTraversableMonad

• Decorated-traversable monads

Tealeaves.Classes.Coalgebraic.DecoratedTraversableMonad

• Coalgebraic Decorated Traversable Monads
  • The toBatch7 Operation
  • The cojoin_Batch7 Operation
  • cojoin_Batch7 as double_batch7
  • Typeclass

Tealeaves.Adapters.CategoricalToKleisli.DecoratedTraversableMonad

• Kleisli DTMs from Categorical DTMs
  • Derived Operations
  • Derived Instances
  • Typeclass Instances

Tealeaves.Adapters.KleisliToCategorical.DecoratedTraversableMonad

• Categorical DTMs from Kleisli DTMs
  • Derived Operations
  • Monad Instance
  • Decorated Functor Instance
  • Decorated Monad Instance
  • Traversable Functor instance
  • Traversable Monad Instance
  • Decorated Traversable Functor instance

Tealeaves.Adapters.KleisliToCoalgebraic.DecoratedTraversableMonad

• DecoratedTraversableMonads as Batch7 coalgebras
  • double_batch7 as batch ⋆7 batch
  • Derived Laws

Tealeaves.Adapters.CoalgebraicToKleisli.DecoratedTraversableMonad

• Coalgebraic DTMsto Kleisli DTM
  • Derived Operation
  • ⋆7 as runBatch ∘ map runBatch ∘ double_batch7
  • Derived Laws
  • Typeclass Instances

Tealeaves.Adapters.Roundtrips.DecoratedTraversableMonad

• Categorical ~> Kleisli ~> Categorical
• Kleisli ~> Categorical ~> Kleisli

Tealeaves.Adapters.Compositions.DecoratedTraversableModule

• Composition of Two DTF Instances
  • Composition of mapdt Operations
  • DecoratedTraversableFunctor Laws
  • DecoratedTraversableFunctor Instance
• Composition of a DTF with a DTM Right Module
  • Composition of mapdt with binddt
  • DecoratedTraversableRightModule Laws
  • DecoratedTraversableRightModule Instances

Tealeaves.Adapters.MonadToApplicative

• Monadic Applicative Functors
  • Derived Operations
  • Derived Laws
  • Typeclass Instance

Tealeaves.Categories.Type

• Category Instance for Type
• Coercing Monad to Category.Monad

Tealeaves.Categories.TypeFamily

• The Category of Constant K-Indexed Families
  • The Index Typeclass
  • Operations on Families of Functions
  • Lemmas for Composition
  • Category Instance
• Specialized Notations for Multisorted Tealeaves
• The Category of K-Indexed Families
• Targeted Morphisms
  • Rewriting Hints for tgt-like combinators
  • Map-Building Combinators: tgt, tgt_def
  • Map-building Combinator tgtd
  • Automation support

Tealeaves.Categories.DecoratedFunctor

• A Decorated Functor is Precisely a Right comodule of (E ×)
• Decorated Functors Form a Monoidal Category
  • Null-Decorated Functors
  • The Identity Null-Decorated functor
  • Decorated Functors are Closed under Composition
  • Category Laws for Composition of Decorated Functors
  • Composition with Null-Decorated Functors
• Monad Operations in As Homomorphisms of Decorated Functors

Tealeaves.Categories.TraversableFunctor

• Monoid Structure of Traversable Functors
  • The Identity Functor is Traversable
  • Traversable Functors are Closed under Composition
• Monad Operations as Homomorphisms between Traversable Functors

Tealeaves.Categories.DecoratedTraversableFunctor

• Monoid Structure of Decorated Traversable Functors
  • The Identity Functor is Decorated Traversable
  • Decorated Traversable Functors are Closed under Composition
  • Null-Decorated Traversable Functors are Decorated Traversable
  • Identity and Associativity Laws

Tealeaves.Functors.Early.Subset

• Subsets
  • Operations
  • Notations and Tactics
• The subset Monoid
  • Simplification Support
  • Querying for an Element is a Monoid Homomorphism
• Functor Instance
  • The Map Operation
  • Rewriting Laws
  • Functor Laws
  • Mapping is a Monoid Homomorphism
• Monad Instance (Categorical)
  • Monad Laws
• Monad Instance (Kleisli)
  • Rewriting Laws
  • Monad Laws
  • bind is a Monoid Homomorphism
  • {{ - }} is Injective
• Applicative Instance
  • Non-Idempotence of the Applicative
  • The Applicative Functor is Commutative

Tealeaves.Classes.Categorical.ContainerFunctor

• Container-Like Functors
  • Operation tosubset and x ∈ -
  • Typeclass
  • Homomorphisms of Container-Like Functors
• Container Instance for subset
• Basic Properties of Containers
  • Interaction between (∈) and map
  • Respectfulness Conditions
  • Properness Conditions
• Quantification over Elements (Forall, Forany)
• Notations

Tealeaves.Classes.Kleisli.ContainerMonad

• Typeclasses

Tealeaves.Functors.Early.Ctxset

• The ctxset Decorated Functor
  • Operations and Specifications
  • Decorated Functor Laws
  • Typeclass Instance
• Monoid Instance
  • map and mapd are Homomorphisms
• The ctxset Monad (Kleisli)
  • Operations and Specifications
  • Compatibility Instances
  • Rewriting Laws
  • Decorated Monad Laws
  • Typeclass Instances
  • bind is a Monoid Homomorphism
  • Querying for an Element is a Monoid Homomorphism

Tealeaves.Classes.Kleisli.DecoratedContainerFunctor

• Decorated Container-Like
  • Operation toctxset
  • Compatibility with tosubset
  • element_ctx_of operation (∈d)
  • Typeclass
  • Homomorphisms of Decorated Container Functors
• Notations

Tealeaves.Classes.Kleisli.DecoratedContainerMonad

• Decorated Container Monads
  • Typeclasses

Tealeaves.Functors.Early.List

• Automation: simpl_list
• Monoid Instance
  • Simplification
• Functor Instance
  • Rewriting Laws for map
  • Functor Laws
  • map is a Monoid Homomorphism
• Monad Instance (Categorical)
  • Monad Operations
  • Rewriting Laws for join
  • Monad Laws
  • join is a monoid homomorphism
• Traversable Monad Instance (Kleisli)
  • The bindt Operation
  • Rewriting Laws for bindt
  • Traversable Monad Laws
  • Typeclass Instance
• Traversable Functor Instance (Kleisli)
  • Rewriting Laws for traverse
• Monad Instance (Kleisli)
  • Rewriting Laws for bind
  • bind is a Monoid Homomorphism
• Traversable Instance (Categorical)
  • Rewriting Laws
  • Traversable Functor Laws
  • Typeclass Instance
• Folding over lists
  • Rewriting Laws for mconcat
  • mconcat is a Monoid Morphism
  • Miscellaneous properties
  • The mapReduce_list Operation
  • mapReduce_list is a Monoid Homomorphism
  • mapReduce_list Commutes with Monoid Homomorphism
  • Rewriting Laws for mapReduce_list
  • Monoids form list (monad-)algebras
• Container Instance
  • Rewriting Laws for tosubset
  • Naturality of tosubset
  • tosubset is a Monoid Homomorphism
  • Rewriting Laws for x ∈ _
  • x ∈ is a Monoid Homomorphism
  • Respectfulness Conditions
  • tosubset as a Monad Homomorphism

Tealeaves.Classes.Categorical.ShapelyFunctor

• Shapely functors
• Operation tolist
  • Operation shape
  • Shapeliness Condition
  • Typeclass
  • Homomorphisms of Shapely Functors
  • Various Characterizations of Shapeliness
  • Equivalences
• Derived Container Instance
  • Enumerating Elements of Shapely Functors
  • Container Laws
  • Typeclass Instance

Tealeaves.Functors.Early.Environment

• Decorated Traversable Functor Instance (Kleisli)]
  • Operation mapdt and Derived Operations
  • Rewriting Laws for mapdt
  • Compatibility Typeclass Instances
  • Decorated Traversable Functor Laws
  • Typeclass Instance
  • Alternative Specifications for mapd
• Decorated Traversable Monad Instance (Kleisli)

Tealeaves.Classes.Kleisli.DecoratedShapelyFunctor

• Operation toctxlist

Tealeaves.Functors.Backwards

• The Backwards Applicative
  • Functor Instance
  • Applicative Instance
  • Involutive Properties
  • Traversing by Backwards (Backwards G)
  • Miscellaneous
  • Traversing over Lists Backwards

Tealeaves.Functors.Constant

• Inductive Definition of the Constant Functor
  • Monoids as Constant Applicative Functors
• Computational Definition of the Constant Functor
  • Monoids as Constant Applicative Functors
• Simplification Support
  • Constant applicatives
  • Constant maps

Tealeaves.Functors.ProductFunctor

• Cartesian Product of Functors
  • Functor Instance
• Applicative Functor Instance
  • Operations
  • Applicative Laws
  • Projections as Applicative Homomorphisms
  • Parallel Composition of Applicative Homomorphisms
• Notations

Tealeaves.Functors.Diagonal

• Diagonal (Duplication) Applicative Functor
  • Applicative Functor Instance
  • Traversable Functor Instance

Tealeaves.Classes.Kleisli.Theory.TraversableFunctor

• Miscellaneous Properties of Traversable Functors
  • Traversing in the Idempotent Center stays in the Idempotent Center
  • Interaction between traverse and pure
• Factorizing Operations through runBatch
  • Factoring operations through toBatch
  • Naturality of toBatch
• Traversals by Particular Applicative Functors
  • Product of Two Applicative Functors
  • Constant Applicative Functors
  • Traversals by Commutative Applicatives
• Derived Operation: mapReduce
  • Operation mapReduce
  • As a Special Case of traverse
  • Composition with map and traverse
  • Composition with Homomorphisms
  • Factorizing through runBatch
  • Factorizing through toBatch
• mapReduce Corollary: tolist
  • Operation tolist
  • Relating mapReduce (T := list) to mapReduce_list
  • Naturality
  • Rewriting tolist to traverse
  • Factoring tolist through runBatch and toBatch
  • Factoring any mapReduce through tolist
• mapReduce Corollary: tosubset
  • The tosubset Operation
  • Compatibility
  • Naturality
  • Rewriting tosubset to mapReduce
  • Factoring tosubset through tolist
  • Rewriting a ∈ t to mapReduce
  • Factoring a ∈ t through tolist
  • Factoring tosubset through runBatch
• mapReduce Corollary: Forall, Forany
  • Operations Forall and Forany
  • Specification via element_of
  • Decidability of Forall and Forany
  • Corollaries of decidability
• mapReduce Corollary: plength
  • plength of a list
  • Factoring plength through list
  • Naturality of plength
• mapReduce by a Commutative Monoid
• Notations

Tealeaves.Classes.Categorical.Theory.TraversableFunctor

• Traversable Instance for Certain Functors
  • Traversable Instance for (E ×)
• Distribution over Certain Applicative Functors
  • Constant Applicative Functors

Tealeaves.Classes.Kleisli.Theory.TraversableCommutativeIdempotent

• Examples of Commutative-Idempotent-Traversable Homomorphisms
  • Traverse Commutes with List Reversal
  • "Duplicate First Element"
  • "Pair All with First Element"

Tealeaves.Classes.Kleisli.Theory.ContainerMonad

• Derived Properties of ContainerMonad
  • ret is Injective
  • Specification of a ∈ ret -
  • Specification of b ∈ bind f t
  • Respectfulness Properties for bind
• Derived Properties of ContainerRightModule
  • Specification of b ∈ bind f t
  • Respectfulness Properties for bind

Tealeaves.Classes.Kleisli.Theory.TraversableMonad

• Theory of Traversable Monads
  • mapReduce on Traversble Monads
  • tolist on Traversable Monads
  • tosubset on Traversable Monads
  • element_of on Traversable Monads

Tealeaves.Classes.Kleisli.Theory.DecoratedContainerFunctor

• Derived Properties of DecoratedContainerFunctor
  • Relating a ∈ t to (e, a) ∈d t
• Basic Properties of Decorated Containers
  • Respectful Properties between (∈d) and mapd

Tealeaves.Classes.Kleisli.Theory.DecoratedTraversableFunctor

• Theory of Decorated Traversable Functors
  • mapdt with constant applicative functors
• Derived Operation mapdReduce
  • Rewriting Laws
  • Composition Laws with mapd and map
  • Composition with Monoid Homomorphisms
• The toctxlist operation
  • Rewriting to mapdReduce/mapdt
  • Naturality
  • Composing toctxlist with mapd
  • Naturality for toctxlist
  • Factoring mapdReduce through toctxlist
  • Relating tolist and toctxlist
• toctxset and ∈d
  • Rewriting toctxset_of and ∈d to mapdReduce
  • Factoring toctxset_of through toctxlist/mapdReduce
  • Fusion Laws for toctxset
  • Naturality for toctxset
  • Relating tosubset and toctxset
  • Characterizing ∈d
  • Folding by Preordered Monoids
• Quantification with Context: Forall_ctx and Forany_ctx
  • Decidability of Forall_ctx and Forany_ctx
  • Booleans

Tealeaves.Classes.Kleisli.Theory.DecoratedContainerMonad

• Basic properties of containers
  • Instance for env

Tealeaves.Classes.Kleisli.Theory.DecoratedTraversableMonad

• Theory of Decorated Traversable Monads
  • Composition in the Applicative Functor
  • Rewriting Lemmas for Particular Applicative Functors
  • Properties of mapdReduce
  • Properties of mapReduce
  • Properties of tolistd
  • Properties of tolist
  • Properties of toctxset
  • Properties of tosubset
  • Properties of ∈d
  • Properties of ∈
• Monad Homomorphism Instances

Tealeaves.Functors.Ctxset

• DecoratedContainerFunctor Instance for ctxset

Tealeaves.Functors.List

• toBatch Instance
• map equality inversion lemmas
• Shapely Functor Instance for list
  • Rewriting shape on Lists
  • Reasoning Princples for shape on Lists
• Reasoning principles for shape on listable functors
• Quantification Over Elements
  • a ∈ - in terms of mapReduce_list
  • Rewriting Laws for mapReduce
• Specification of Permutation
• Miscellaneous
• Un-con-sing Nonempty Lists
  • Total Head and Tail Functions for Nonempty Lists
• Filtering Lists
  • Rewriting Laws for filter

Tealeaves.Functors.Environment

• Decorated Container Instance for env
  • Rewriting Rules for toctxset
  • Naturality
  • toctxset is a Homomorphism of Decorated Functors

Tealeaves.Functors.Option

• The option Monad
  • Functor Instance
  • Applicative Instance
  • Monad Instance

Tealeaves.Functors.Pathspace

• Pathspace Applicative Functor
  • Applicative Instance

Tealeaves.Functors.Pair

• Cartesian Product Bifunctor
  • Bi-map Operation
  • Bi-traverse Operation

Tealeaves.Functors.Reader

Tealeaves.Functors.State

• State Monad
  • Functor Instance
  • Monad Instance (Kleisli)
  • Monad Instance (Categorical)

Tealeaves.Functors.Store

• The Store functor
  • Functor Instance
  • Store as a Parameterized Comonad
  • A Representation Lemma

Tealeaves.Functors.Subset

Tealeaves.Functors.Writer

• T ∘ (W ×) is a monad
• Miscellaneous Properties

Tealeaves.Functors.ListHistory

• Mapping over a List with History
  • Operation hmap
  • Alternative Definition of hmap

Tealeaves.Functors.List_Telescoping_General

• Prefix Decoration Operation for the List Functor
  • Accumulator-Based Specification
  • Map-Based Specification
  • Equivalence
  • Examples
  • Rewriting Laws
• The Z Comonad (Categorical)
  • Tactical Support: Folding/Unfolding
  • Functor Instance
  • Operations cojoin_Z and extract_Z
  • Rewriting Laws
  • Naturality
  • Comonad Laws
  • Typeclass Instance
  • decorate_prefix_list as a Right Coaction
• Traversable Functor Instance (Kleisli)
  • Operation traverse_Z
  • Specification for traverse_Z
  • Naturality
  • Interaction with incr and ⦿
  • Typeclass Instance
• Decoration Commutes with Traversals
• Mapdt for list and Z
  • Recursive inlined version
  • Decomposed Version
  • Equivalence of the Definitions
  • Rewriting Laws
  • Rewriting Laws for Z
  • Kleisli composition
• Decorate traversable functor instance
  • Unit law
  • Composition law (Indirect proof)
  • Homomorphism law
  • Typeclass Instance
• Mapd for list
  • Recursive inlined version
  • Decomposed Version
  • Rewriting Laws
• Mapd for Z
  • Recursive inlined version
  • Decomposed Version
  • Rewriting Laws
• Decorated Functor Instance for List
  • Unit law
  • Composition law
• Comonad instance on Z
• Dist instance on Z

Tealeaves.Functors.Vector

• • Properties of vectors
  • Functor instance
  • Traversable instance

Tealeaves.Functors.KStore

• The KStore functor
  • Functor instance
  • Applicative instance

Tealeaves.Functors.VectorRefinement

• Refinement-style vectors
  • Coercing lengths
  • Similarity
  • Notions of equality assuming proof-irrelevance axiom
  • Derived constructors
  • Reversing vectors
  • Inversion/un-consing non-empty vectors
  • Induction
  • Misc
  • to_list
• Functor instance
  • Mapping similar functions over Functors
  • Rewriting rules
• Traversable instance
  • Rewriting rules
  • Relation between Vector_to_list and tolist
  • Traversing over similar vectors
  • Compatibility with map
  • Miscellaneous
  • Traversal laws
  • Traversals and reversals
• SameSetRight
• Elimination principles
• tosubset on Vectors
• Zipping vectors
  • Rewriting Lemmas
  • Roundtrip Properties
  • _sim Properties
  • _sim Properties for n <> m
  • Naturality Properties
  • Diagonal
  • Traversing a Zip by A Relation
  • Generalized zip operation
  • Relating vectors
• Appending Vectors
• Reversing Vectors
• Notations

Tealeaves.Functors.Batch

• mapReduce Rewriting Lemmas
  • mapReduce Rewriting for <⋆>
  • tolist
  • tosubset
  • a ∈ _
• Simultaneous Induction on Two Batches of the Same Shape
• runBatch specialized to monoids
• The length_Batch Operation
  • Rewriting Rules
  • Length is the Same as the Underlying list
  • Length is Preserved By map
  • Length is Preserved by cojoin_Batch
  • Two Same-Shaped Batches Have the Same Length
• Specification for traverse via runBatch
• Batch _ B C is a traversable monad
  • Operation
  • Traversable Monad Laws
• Deconstructing Batch A B C into Shape and Contents
  • Batch_make and Batch_contents
  • Batch_replace_contents
  • Rewriting rules
  • Relating tolist and Batch_contents
  • Rewriting Rules for <⋆>
  • Same Shape Iff Same Batch_make
  • Two Lemmas for shape and length_Batch
  • Same Shape Implies Same Batch_replace_contents
  • Batch_make Equal Iff Batch_replace_contents Equal
  • Similarity Lemmas for Batch_make
  • Similarity Laws for Batch_replace_contents
  • Naturality of Batch_make
  • Naturality of Batch_contents
  • Specification for Batch_replace_contents
  • Replacing Contents Does Not Change length_Batch, shape, or Batch_make
• Lens-like laws
  • Batch is Shapely
• Theory About Batch
  • Misc
• Representation theorems
• Annotating Batch with Proofs of Occurrence
  • Lemmas regarding tosubset
  • Annotation Operation
• runBatch Assuming Proofs of Occurrence

Tealeaves.Adapters.Isomorphisms.BatchtoKStore

• Batch to KStore

Tealeaves.Theory.TraversableFunctor

• Miscellaneous Properties Concerning toBatch
  • Relating tolist and Batch_contents ∘ toBatch
  • Naturality of toBatch
  • Batch_contents ∘ toBatch is Independent of B
  • Equal toBatch Implies Equal tolist
  • Similar shaped toBatch implies similar shapes
• Length of toBatch is polymorphic
• Traversable Functors are Containers
  • Traversable Functors are Shapely
  • Pointwise Reasoning
  • Typeclass Instances
• plength
• Factorizing Terms into shape and contents
  • Operations on Vectors
  • Lemmas regarding trav_make
  • Naturality of trav_contents and trav_make
  • Relating tolist and trav_contents
  • Lens-like laws
  • Lemmas regarding shape and trav_make
  • Lemmas regarding trav_make
  • Representation theorems
  • Corollary: Spec for traverse After Applying trav_make
  • Corollary: Specs for Functor Operations in Terms of Lens Operations
  • Corollary: Specification for shape
  • trav_make is Preserved by shape
  • tosubset is Preserved by trav_contents
• Lemmas about shape
  • Specification for id given two terms with the same shape
• Zipping Terms
  • Operation to Zip Contents of Same-shape Terms
  • Proof Irrelevance
  • Roundtrip Properties
  • Naturality Properties
  • Operation to Zip Same-shape Terms
  • Proof Irrelevance
  • Naturality Properties
  • Traversals over the zip
  • Folding over a Vector of pairs
• Uniqueness

Tealeaves.Theory.TraversableMonad

• Simultaneous Induction on Two Batches of the Same Length
• Theory of Traversable Monads
  • Factoring operations through toBatch
  • Relating toBatch6 with toBatch
  • Naturality of toBatch6
  • Respectfulness properties
  • tosubset is a Homomorphism
  • Monad Homomorphisms

Tealeaves.Theory.DecoratedTraversableFunctor

• Properties of toBatch3
  • Relating toBatch3 with toBatch
  • Factoring mapdt via toBatch3
  • Naturality of toBatch3
• Factoring Operations Through toBatch3
  • Core Operations
  • mapdReduce Through toBatch3
  • toctxlist Through toBatch3
• Respectfulness Properties
  • Purity
  • Characterizing ∈d and mapd
• Shapeliness
• Deconstructing with refinement-type vectors
  • Relating plength and toBatch3
  • mapdt_contents and mapdt_make
  • Relation toctxlist and mapdt_contents
  • _sim Properties
• Miscellaneous
• Lens Laws
  • get-put
  • put-get
  • put-put
• Representation theorems
  • Specialized to option

Tealeaves.Theory.DecoratedTraversableMonad

• Theory of Decorated Traversable Monads
  • Relating toBatch7 to toBatch3 and toBatch6
  • Specification for binddt via toBatch7
  • Naturality of toBatch7
  • Respectfulness for binddt
  • Respectfulness for bindd
• Deriving All Other Typeclass Instances from a DTM

Tealeaves.Theory.LiftRel.TraversableFunctor

• Lifting relations over Traversable functors
  • Related terms have the same shape
  • Related terms have a related zip
• Properties of Relations
• Diagonal

Tealeaves.Theory.LiftRel.DecoratedTraversableFunctor

• Lifting context-sensitive relations over Decorated-Traversable functors

Tealeaves.Functors.List_Telescoping

• Telescoping Decoration for the List Functor
  • The decorate_telescoping_list Operation
  • Alternative Characterization of decorate_telescoping_list
  • Rewriting Rules for decorate_telescoping_list
  • Equivalence
  • Associated mapdt Operation
  • Rewriting Rules for decorate_telescoping_list
  • Typeclass Instance
  • Derived Operation Compatibility
  • Associated toctxlist and toctxset Operations
• Fully Recursive Decoration for the List Functor
  • The decorate_list_full Operation
  • The Associated mapdt_list_full Operation
  • DecoratedTraversableFunctor Typeclass Instance
  • Derived toBatch3 and mapd
  • Compatibility Instances

Tealeaves.Classes.Functor2

• Endofunctors of Two Arguments
  • Operation map2
  • Typeclass
  • Natural Transformations
  • Single-Argument Functor Instances
  • Composition with Single-Argument Functors
  • Strength
• Notations

Tealeaves.Functors.Batch2

• Batch of Two Parameters
  • Functor Instance
  • Applicative Instance
  • Rewriting Principles
  • Applicative Laws
  • Typeclass Instance
  • Operation runBatch2
  • Rewriting rules for runBatch
  • Naturality of runBatch
  • runBatch as an Applicative Homomorphism
• Batch as a Parameterized Comonad
  • Operations extract_Batch and cojoin_Batch
  • Rewriting Principles
  • extract_Batch2 as runBatch (fun A => A) id
  • extract_Batch and cojoin_Batch2 as Applicative Homomorphisms
• Batch as a Parameterized Monad
  • Operations batch and join_Batch

Tealeaves.Classes.Categorical.Monad2

• Monadic Bifunctors

Tealeaves.Classes.Categorical.TraversableFunctor2

• Traversable Functors of Two Arguments
  • Operations
  • Typeclass
  • Other rules for pure
• Notations

Tealeaves.Functors.L

• Z Comonad of Two Arguments
• Dist instance on L

Tealeaves.Classes.Categorical.TraversableMonad2

• Traversable Monadic Bifunctors

Tealeaves.Classes.Categorical.DecoratedFunctorPoly

• shift2
• Poly Decorated functors
  • Operations
  • Typeclass

Tealeaves.Classes.Categorical.DecoratedMonadPoly

• Decorated Monads (Poly)

Tealeaves.Classes.Kleisli.TraversableFunctor2

• • Traverse Poly operation

Tealeaves.Classes.Kleisli.DecoratedFunctorZ

• Functors Decorated by Z Comonad
  • Operation mapdz
  • Kleisli Composition
  • Typeclass
  • Instance for List
  • Instance for Z

Tealeaves.Classes.Kleisli.DecoratedFunctorPoly

• Polymorphically Decorated Functors
  • Operation mapdp
  • Kleisli Composition
  • Typeclass

Tealeaves.Classes.Kleisli.DecoratedMonadPoly

• Polymorphically Decorated Monads
  • Operations binddp
  • Axioms
  • Typeclass

Tealeaves.Classes.Kleisli.DecoratedTraversableFunctorPoly

• Polymorphically Decorated Traversable Functors
  • Operation mapdtp
  • Kleisli Composition
  • Typeclass

Tealeaves.Classes.Kleisli.DecoratedTraversableMonadPoly

• Polymorphically Decorated Traversable Monads
  • Operation substitute
  • Kleisli Composition
  • Typeclass
• Derived Instances
  • Derived Operations

Tealeaves.Adapters.CategoricalToKleisli.DecoratedFunctorZ

• Categorical Z-Decorated Functors to Kleisli Z-Decorated Functors
  • Derived mapdz Operation
  • Derived co-Kleisli Laws

Tealeaves.Adapters.CategoricalToKleisli.DecoratedFunctorPoly

• Kleisli DTMs from Categorical DTMs
  • Derived Operations

Tealeaves.Adapters.CategoricalToKleisli.DecoratedMonadPoly

• Kleisli DTMs from Categorical DTMs
  • Derived Operations
  • Derived Instances

Tealeaves.Adapters.CategoricalToKleisli.DecoratedTraversableFunctorPoly

• Kleisli DTMs from Categorical DTMs
  • Derived Operations

Tealeaves.Adapters.CategoricalToKleisli.DecoratedTraversableMonadPoly

• Kleisli DTMs from Categorical DTMs
  • Derived Operations

Tealeaves.Classes.Multisorted.Multifunctor

• Multisorted Functors
  • Natural Transformations
  • Identity Multisorted Functors at a Some k: K
  • Composition with Ordinary Functors
  • Tensorial Strength
• Single-Sorted Maps: mapk
  • Identity and composition laws for mapk

Tealeaves.Classes.Multisorted.DecoratedTraversableMonad

• Multisorted DTMs
  • Operations
  • Kleisli Composition
  • Typeclasses
  • Operation mapMret
  • Lemmas for Kleisli Composition
  • Purity Law
• Derived Instances
  • Derived Multisorted Operations
  • Rewriting Rules
  • Composition Between mbinddt and Other Operations
  • Composition between Derived Operations
  • Decorated Monad (mbindd)
  • Decorated Traversable Functor (mmapdt)
  • Traversable Monad (mbindt)
  • Heterogeneous Composition Laws
  • Monad (mbind)
  • Decorated Functor (mmapd)
  • Traversable Functor (mmapt)
  • Functor (mmap)

Tealeaves.Functors.Multisorted.Batch

• Multisorted Batch Functor (BatchM)
  • Functor Instance
  • Applicative Instance
  • Functoriality of BatchM
• Operation runBatchM
  • Naturality of runBatchM
  • runBatchM as an Applicative Homomorphism
  • runBatchM commutes with Applicative Homomorphisms
  • Notations

Tealeaves.Adapters.KleisliToCoalgebraic.Multisorted.DTM

• Iterating over a DTM
  • Representing mbinddt with runBatch

Tealeaves.Classes.Multisorted.Theory.Container

• Sorted lists with context
• Shape and Contents
  • Operations
  • Notations
  • Rewriting Rules for filterk
  • Auxiliary Lemmas for constant Applicative Functors
  • Relating ∈m and ∈md
  • Characterizing Membership in List Operations
  • Interaction between tolistmd and mret/mbindd
  • Characterizing Occurrences Post-Operation

Tealeaves.Classes.Multisorted.Theory.Targeted

• Targeted substitution-building combinators: btg and btgd
  • Rewrite Hint registration
  • Derived targeted DTM operations
  • Decorated monad (kbindd)
  • Mixed structure composition laws
  • Decorated functors (kmapd)
  • Monads (kbind)
  • Functors (kmap)
  • Notations
• Characterizing occurrences post-operation (targetted operations)

Tealeaves.Classes.Multisorted.Theory.Foldmap

• Foldmap
  • Operations

Tealeaves.Theory.Multisorted.DecoratedTraversableMonad

• Respectfulness Conditions for mbindd and Derived Operations
  • Identities for tolist and mapReduce
  • Respectfulness for mbindd
  • Respectfulness for mbindd
  • Respectfulness for mmapd
  • Respectfulness for mmap
• Respectfulness for Targeted Operations
  • Respectfulness for kbindd
  • Respectfulness for Heterogeneous Operations
  • Respectfulness for kbind
  • Respectfulness for kmapd
  • Respectfulness for kmap

Tealeaves.Classes.Full.Monad

• Full Kleisli Typeclasses
• Derived Categorical operations
  • Rewriting

Tealeaves.Classes.Full.DecoratedFunctor

• • Full typeclasses

Tealeaves.Classes.Full.DecoratedMonad

Tealeaves.Simplification.Support

• Basic rewriting lemmas
• Simplifying applicative functors
  • Identity applicative
  • Identity maps

Tealeaves.Simplification.Binddt

• Re-infer normalized typeclass instances
• Rewriting with binddt
• Rewriting support lemmas

Tealeaves.Simplification.DeriveDTM

• Deriving DTM laws expressions
  • Proving the first law
  • Proving the second law
  • Proving the third law
  • Proving the fourt law
  • Putting it together

Tealeaves.Simplification.Simplification

Tealeaves.Simplification.MBinddt

• Rewriting with binddt

Tealeaves.Simplification.Tests.Support

Tealeaves.Backends.LN.LN

• Deriving All Other Typeclass Instances from a DTM
• Locally nameless variables
• Locally nameless operations
  • Localized operations
  • Lifted Operations
  • Operation Notations
• Some Tactics
• Basic principles and lemmas
  • Local closure spec
  • Reasoning principles for proving equalities
  • Occurrence analysis lemmas
• Utilities for reasoning at the leaves
  • (In)equalities between leaves
  • subst_loc
  • open_loc
  • close_loc
  • Local reasoning principles for LC
• Free variables
  • Free variables
  • Miscellaneous utilities
• Locally nameless metatheory
  • Occurrence analysis: substitution with contexts
  • Occurrence 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 LN
  • 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
  • Closing 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 LN reduces to an mapkr
  • Opening, followed by closing
  • Opening and local closure
  • Injectivity of opening

Tealeaves.Backends.LN.Simplification

• Simplifying LCn
  • Extra Rewriting Principles
  • Simplifying LCn at the leaves
  • Simplifying LCn
• Simplifying free and FV
• Simplifying open
• Simplifying subst
• Simplifying everything

Tealeaves.Backends.LN.Parallel

• Locally nameless leaves
• Operations for locally nameless
  • Local operations
  • Lifted operations

Tealeaves.Backends.Common.AssocList

• The alist functor
  • Functor instance for alist
  • DT functor instance for alist
• envmap
  • Rewriting principles for envmap
  • Specifications for ∈ and envmap
  • Rewriting principles for ∈
  • Tactical lemmas for ∈
• Domain and range on alists
  • Rewriting lemmas for dom
  • Rewriting lemmas for domset
  • Rewriting lemmas for range
  • Rewriting lemmas for ∈ dom
  • Rewriting lemmas for ∈ domset
  • Elements of range
• Specifications for operations on association lists
  • Specifications for ∈ and dom, domset, range
  • Support for prettifying association lists
  • Tactics for normalizing alists
  • Induction principles for alists
  • 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
• Facts about binds
  • Permutation lemmas
• Tactic support for picking fresh atoms

Tealeaves.Backends.LN

Tealeaves.Backends.Multisorted.LN.LN

• Binders contexts
• Locally nameless variables
• Syntax operations for locally nameless
  • Local operations
  • Lifted operations
  • Notations for operations
  • Identity and equality lemmas for operations
  • Context-sensitive LN analysis of operations
  • Context-agnostic LN analysis of operations
• Specifications for free
  • Characterizations for free and FV
  • free variables after open/close/subst
• Lemmas for local reasoning
  • Lemmas for proving (in)equalities between leaves
  • subst_loc
  • open_loc
  • Tactics for local reasoning
• Metatheory for the subst operation
  • LN analysis with contexts
  • LN analysis 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 LN
  • Substitution by the same variable is the identity
  • Metatheory for close
  • Free variables after variable closing
  • Variable closing and local closure
  • Metatheory for open
  • 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 LN reduces to an kmapd
  • Opening, followed by closing
  • Opening and local closure

Tealeaves.Backends.Multisorted.LN

Tealeaves.Backends.DB.DB

• Closure
  • Level
  • Boolean versions
  • Propositional versions
  • Relating the two
  • Boundedness and closure
• Incrementing/lifting indices
• Cons operation
  • Properties of scons
  • Cons and lifting
• Renaming
  • Properties of level
  • Properties of renaming
  • Renaming and ret
  • Renaming identity
  • Composition of renaming
  • Iterating lifting
  • Relating lift__ren to up__ren
  • Operations with policy
  • Characterizing occurrence
• De Bruijn operations
• Properties of substitution
  • Substitution and ret
  • Substitution and identity
  • Iterated lifting
  • Substitution and composition
  • Substitution and renaming
  • up__sub and lift__spec
  • Characterizing occurrence
• Notations
• Other lemmas

Tealeaves.Backends.DB.Simplification

• Extra lemmas
• Unfolding up
• Simplifying renaming via unfolding
• Simplifying substitution via unfolding
• Simplifying substitution a la Autosubst

Tealeaves.Backends.DB.AutosubstShim

• Autosubst-compatible notations

Tealeaves.Backends.DB

Tealeaves.Misc.PartialBijection

• Partial Bijections
  • Characterizing Partial Bijections
  • Specification
• Partial Bijections with Domain Specifications

Tealeaves.Backends.Adapters.Key

• Miscellaneous lemmas
• Definition of key and main operations
  • Insertion and lookup
  • Well-formedness predicates
• Misc
• Lemmas about key_insert_atom
  • Rewriting
  • Alternative spec
  • Insertion and unique
  • Insertion and getIndex
  • Insertion and key_lookup_ix
  • Properties of getName

Tealeaves.Backends.Adapters.LNtoDB

Tealeaves.Backends.Adapters.DBtoLN

Tealeaves.Backends.Adapters.Roundtrips.LNDB

• • Basic supporting lemmas
  • Totality
  • Roundtrip from LN
  • Roundtrip from DB

Tealeaves.Backends.Common.Names

• Transparent Atoms
• Transparent Atoms Implementation Support
  • Least Strict Upper Bound of a list
  • Testing Membership in a list
  • Computing Maximum Element Not in list
  • Transparent Atoms Implementation
  • Shorthands and notations

Tealeaves.Backends.Common.AtomSet

• Definition of AtomSet type
  • Notations for operations on AtomSet
  • The atoms operation
  • Rewriting rules
  • Relating AtomSet.t and list atom

Tealeaves.Adapters.MonoidHom.DecoratedTraversableMonad

Tealeaves.Adapters.MonoidHom.Categorical

Tealeaves.Adapters.PolyToMono.Categorical.DecoratedFunctor

• Parameterized Decorated Functor to Decorated in Variables
• Parameterized Decorated Functor to Decorated in Binders

Tealeaves.Adapters.PolyToMono.Categorical.TraversableFunctor

• • Single-Argument Traversable Functor Instances

Tealeaves.Adapters.PolyToMono.Categorical.DecoratedMonad

Tealeaves.Adapters.PolyToMono.Categorical.TraversableMonad

• • Single-Argument Traversable Functor Instances

Tealeaves.Adapters.PolyToMono.Categorical.DecoratedTraversableMonad

Tealeaves.Classes.Categorical.DecoratedTraversableFunctorPoly

• Polymorphic Decorated Traversable Functor

Tealeaves.Classes.Categorical.DecoratedTraversableMonadPoly

• Decorated-traversable monads

Tealeaves.Adapters.PolyToMono.PDTM

• Convenient Interface to categorically-defined PDTMs
  • Single-argument Categorical Operations
  • Single-argument Categorical Instances
  • Single-argument Kleisli operations

Tealeaves.Backends.Nominal.Common.Hmap

• The hmap Operation
  • Rewriting Rules for hmap
  • Preservation of length
  • An Induction Rule for hmap
• Relating History to the Prefix: hadapt
  • Rewriting Rules
  • Rewriting Rules
• Folding with context AND history

Tealeaves.Backends.Nominal.Common.Binding

• The Logic of Variable Binding
  • get_binding Operation
  • get_binding Examples
  • get_binding Specification
  • Rewriting Principles
  • Proof of Specification
  • Supporting Lemmas on list
  • Inverse of Specification

Tealeaves.Backends.Nominal.Common.Freshening

• Freshen an Entire List
  • Examples
• Local Definition of Assigning Unique Names to a list
  • historyToName
  • Rewriting Principles for historyToName
  • Freshness for historyToName
• Assign Unique Names to a list
  • Assign Names to an Arbitrary list
  • Basic Properties of assignNames
  • Rewriting Principles for assignNames
  • Freshness for assignNames_loc and assignNames

Tealeaves.Backends.Nominal.FV

• Nominal Free Variables

Tealeaves.Backends.Nominal.Barendregt

Tealeaves.Backends.Nominal.Alpha

• Alpha Equivalence
  • Local Definition of Alpha Equivalence
  • Alpha Equivalence
  • Alpha Equivalence
  • Alpha Reasoning Principles

Tealeaves.Backends.Adapters.NominaltoLN

• Nominal to Locally Translation

Tealeaves.Backends.Adapters.LNtoNominal

• Converting a depth to (list unit) binding context
• Locally Nameless to Nominal

Tealeaves.Examples.Lambda.Confluence

Tealeaves.Examples.Lambda.MapWithPolicyDemo

Tealeaves.Examples.JAR.TranslateDemo

Tealeaves.Examples.STLC.Syntax

Tealeaves.Examples.STLC.CompatTest

• Language definition
  • Instantiate Tealeaves

Tealeaves.Examples.STLC.SyntaxCategorical

Tealeaves.Examples.STLC.TypeSoundness

• Inversion lemmas
• Misc lemmas

Tealeaves.Simplification.Tests.STLC_Binddt

• Simplification tests for categorical operations
  • binddt and ret
  • Binddt
  • Bindd
  • Bind
  • Mapdt
  • Mapd
  • Map

Tealeaves.Simplification.Tests.STLC_Container

• Simplification tests for derived operations
  • Rewriting lemmas for mapdReduce
  • Rewriting lemmas for ∈d
  • Rewriting lemmas for mapReduce
  • Rewriting lemmas for tolist, toset, ∈

Tealeaves.Simplification.Tests.STLC_LN

• • Rewriting lemmas for LC
  • Rewriting lemmas for free, freeset
  • Rewriting lemmas for open
  • Rewriting lemmas for subst

Tealeaves.Simplification.Tests.STLC_DB

• Simplification Tests for the De Bruijn Backend
  • Rewriting Lemmas for rename
  • Rewriting Lemmas for subst

Tealeaves.Examples.VariadicLet.Terms

• Language definition

Tealeaves.Examples.VariadicLet.Instances.Simple

• • Rewriting Laws
  • Point-free Rewriting Laws

Tealeaves.Examples.VariadicLet.Instances.Tele

Tealeaves.Examples.VariadicLet.Instances.LetRec

Tealeaves.Examples.VariadicLet.Demo

Tealeaves.Examples.SystemF.Syntax

• The index K
• System F syntax and typeclass instances
  • Notations
  • Example expressions
  • binddt operations
  • Example computations
  • Demo of opening operation
• Proofs of the DTM axioms
  • Helper lemmas for proving DTM axioms
  • mbinddt_mret
  • mbinddt_mbinddt
  • mbinddt_morphism
  • mbinddt_comp_mret
  • DTPreModule instances
• System F type system and operational rules
  • Contexts and well-formedness predicates
  • Typing judgments
  • Values and reduction rules

Tealeaves.Examples.SystemF.Contexts

• Tactical support
• Structural lemmas for scoped
• Infrastructural lemmas for contexts and well-formedness predicates
  • General properties of ok_kind_ctx
  • Tactical support for ok_kind_ctx
  • General properties of ok_type
  • Structural properties of ok_type Δ τ in Δ
  • General properties of ok_type_ctx
  • Tactical support for ok_type_ctx
  • Structural properties in Δ in ok_type_ctx Δ Γ.
  • Structural properties of ok_term Δ Γ t in Δ
  • Structural properties of ok_term Δ Γ t in Γ

Tealeaves.Examples.SystemF.TypeSoundness

• Properties of the typing judgment Δ ; Γ ⊢ t : τ
  • Structural properties Δ ; Γ ⊢ t : τ in Δ
  • Properties of Δ ; Γ ⊢ t : τ in Γ
  • Properties in τ of (Δ ; Γ ⊢ t : τ
  • Properties in t of (Δ ; Γ ⊢ t : τ
• Progress and preservation

Tealeaves.Simplification.Tests.SystemF_Binddt

• • mbinddt
  • mbindd
  • mbind
  • mmapdt
  • mmapd
  • mapReducemd
  • mapReducem
  • Forallmd

Tealeaves.Simplification.Tests.SystemF_Targeted

• • kbindd
  • kbind
  • kmapdt
  • mapReducekd
  • Forallkd
  • mapReducek

Tealeaves.Simplification.Tests.SystemF_LN

• • open
  • LCn
  • LC
  • subst
  • free
  • FV
  • scoped

Tealeaves.Examples.LambdaNominal.Syntax

• Language definition
  • Notations and automation

Tealeaves.Examples.LambdaNominal.Categorical

Tealeaves.Examples.LambdaNominal.TypeclassTesting

Tealeaves.Examples.LambdaNominal.Demo

Tealeaves.Examples.LambdaNominal.RawUnguarded

Tealeaves.Examples.RecBag.Syntax