ITree.Basics.Tacs

ITree.Basics.Basics

• General-purpose definitions
  • Parametric functions
  • Common monads and transformers.
  • Loop operator

ITree.Basics.HeterogeneousRelations

• Heterogeneous relations
  • Relations for morphisms/parametricity
  • Relations for morphisms/parametricity
  • subrelationH

ITree.Basics.CategoryOps

• Category operations
  • Low-level infrastructure
  • Categories
  • Bifunctors
  • Notations with explicit objects
  • Core notations
  • Derived constructions
  • Iteration, fixed points
  • Automatic solver of reassociating sums

ITree.Basics.CategoryFunctor

• Definition of a functor

ITree.Basics.CategoryTheory

• Category theory
  • Categories
  • Mono-, Epi-, Iso- morphisms
  • Opposite
  • Dagger
  • Bifunctors
  • Coproducts
  • Products
  • Monoidal categories
  • Symmetric monoidal categories

ITree.Basics.CategoryFacts

• General facts about categories
  • Isomorphisms
  • Categories
  • Bifunctors
  • Coproducts

ITree.Basics.Category

• Generic library for categories (reexports the three other modules)

ITree.Basics.CategorySub

• Full subcategories

ITree.Basics.Function

• The Category of Functions
  • The sum coproduct.

ITree.Basics.FunctionFacts

• Theorems for ITree.Basics.Function

ITree.Basics.CategoryRelations

ITree.EqmR.EqmRMonad

• EqmR Monad laws and associated typeclasses
• EqmR_OK : Well-formedness properties of EqmR.
• Image : the set of possible return values of a monad

ITree.Basics.CategoryKleisli

• Kleisli category

ITree.Basics.CategoryKleisliFacts

ITree.EqmR.EqmRMonadH

• Relations over different monads

ITree.EqmR.EqmRMonadT

• Relational reasoning over monad transformers

ITree.Core.ITreeDefinition

• Interaction trees: core definitions
  • The type of interaction trees
  • Main operations on itree
  • Notations
  • Instances
  • Tactics
  • Compute with fuel

ITree.Eq.Shallow

• Shallow equivalence
  • observing: Lift relations through observe.
  • Unfolding lemmas for bind
  • going: Lift relations through go.

ITree.Eq.Paco2

ITree.Eq.Eq

• Strong bisimulation
  • Coinductive reasoning with Paco
  • Properties of relations
  • Eta-expansion
  • Equations for core combinators
  • Tactics

ITree.Eq.UpToTaus

• Equivalence up to taus
  • gpaco

ITree.Eq.SimUpToTaus

• Simulation up to taus

ITree.Eq.EqAxiom

• Strong bisimulation is propositional equality

ITree.Eq

• Equivalences for interaction trees

ITree.EqmR.Monads.ITree_weak

ITree.EqmR.Monads.ITree_strong

ITree.Core.KTree

• The category of continuation trees (KTrees)
  • Categorical operations

ITree.Core.KTreeFacts

• Facts about aloop and loop
  • ITree.aloop
  • iter

ITree.Indexed.Sum

• Sums of indexed types

ITree.Indexed.Relation

• Relations on indexed types

ITree.Indexed.Function

• The Category of Indexed Functions

ITree.Indexed.FunctionFacts

• Theorems for ITree.Indexed.Function

ITree.Core.Subevent

• Extensible effects
  • Subevents
  • Triggerable Monads
  • Over: injection for handlers over sums of events
  • Instances for Automatic Injection
  • Automatic solver for associating subevents

ITree.EqmR.Monads.ID

• EqmR-related laws for the identity monad.

ITree.EqmR.Monads.State

• EqmR-related laws for the state monad.

ITree.EqmR.Monads.StateT

• EqmR-related laws for the state monad transformer.

ITree.EqmR.Monads.Error

• EqmR-related laws for the error monad.

ITree.EqmR.Monads.ErrorT

• EqmR-related laws for the error monad transformer.

ITree.EqmR.Monads.Prop

• • Nondeterminism monad.

ITree.Basics.MonadState

• Iterative laws for state monad

ITree.Basics.MonadFail

• Iterative laws for failure monad

ITree.Interp.Recursion

• General recursion

ITree.Interp.Handler

• Event handlers
  • Handler combinators
  • Category instances

ITree.Interp.Interp

• Interpretable Monads
  • Translate
• Interpret

ITree.Interp.TranslateFacts

• Theorems about Interp.translate

ITree.Interp.HFunctor

• Higher-order functors
  • Higher-order functors
  • Higher-order functor laws
  • Higher-order functor laws for Iterative Monads
  • Nesting HFunctors

ITree.Interp.InterpFacts

• Reasoning principles for interpretable layered monads
• interp and constructors

ITree.Interp.Traces

• ITrees as sets of traces

ITree.Events.State

• State

ITree.Events.Reader

• Reader

ITree.Events.Writer

• Writer

ITree.Events.Exception

• Exception event

ITree.Events.Nondeterminism

• Nondeterminism
  • Empty nondeterminism

ITree.Events.Map

• Mutable map

ITree.Events.MapDefault

• Mutable map whose lookup operation provides a default value.

ITree.Events.MapDefaultFacts

• Mutable map whose lookup operation provides a default value.

ITree.Events.Concurrency

• Concurrency

ITree.Events.Dependent

• Dependently-typed events

ITree.Events

• Standard event types
  • State
  • Reader
  • Writer
  • Exception
  • Nondeterminism
  • Map
  • Concurrency
  • Dependent

ITree.ITree

• Main module

ITree.ITreeFacts

• Main module with theorems