ITree.Simple

• Simplified interface
  • Core definitions
  • Interpreters, handlers
  • Equational theory

ITree.ITree

• Main module

ITree.ITreeFacts

• Main module with theorems

ITree.Axioms

• Axioms used in the ITree library.

ITree.Basics.Tacs

ITree.Basics.Basics

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

ITree.Basics.HeterogeneousRelations

• • Relations for morphisms/parametricity
  • Relations for morphisms/parametricity
  • subrelationH

ITree.Basics.Category

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

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.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
  • Products

ITree.Basics.CategorySub

• Full subcategories

ITree.Basics.CategoryFunctor

• Definition of a functor

ITree.Basics.CategoryRelations

ITree.Basics.Monad

• Monad laws and associated typeclasses

ITree.Basics.MonadProp

ITree.Basics.MonadState

ITree.Basics.CategoryKleisli

• Kleisli category

ITree.Basics.CategoryKleisliFacts

ITree.Basics.Function

• The Category of Functions
  • The sum coproduct.
  • The pair product.
  • Cartesian closure.

ITree.Basics.FunctionFacts

• Theorems for ITree.Basics.Function

ITree.Core.ITreeDefinition

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

ITree.Core.KTree

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

ITree.Core.KTreeFacts

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

ITree.Core.Subevent

• Extensible effects

ITree.Core.ITreeMonad

ITree.Eq

• Equivalences for interaction trees

ITree.Eq.Paco2

ITree.Eq.Shallow

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

ITree.Eq.Eqit

• 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.EuttExtras

• More facts about eutt

ITree.Eq.Rutt

• Relation up to tau

ITree.Props.Leaf

• Leaves of an Interaction Tree
  • Leaves of itrees

ITree.Props.Finite

• Finite Interaction Tree
  • Finite computations as Interaction Trees
• any_finite is non-empty Leaf
• Counterexamples

ITree.Props.HasPost

• Unary interpretation for eutt: a traditional program logic

ITree.Props.Infinite

• Infiniteness of ITrees
  • Infinite *

ITree.Props.Cofinite

• Relations between infiniteness and finiteness

ITree.Props.EuttNoRet

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.Interp.Interp

• Monadic interpretations of interaction trees
  • Translate
  • Interpret

ITree.Interp.TranslateFacts

• Theorems about Interp.translate

ITree.Interp.InterpFacts

• Theorems about interp
  • interp and constructors
  • interp properness
  • Composition of interp

ITree.Interp.Handler

• Event handlers
  • Handler combinators
  • Category instances

ITree.Interp.HandlerFacts

• Theorems for ITree.Interp.Handler

ITree.Interp.Recursion

• General recursion

ITree.Interp.RecursionFacts

• Properties of Recursion.mrec and Recursion.rec.

ITree.Interp.Traces

• ITrees as sets of traces

ITree.Events

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

ITree.Events.State

• State

ITree.Events.StateFacts

• Theorems about State effects

ITree.Events.Reader

• Reader

ITree.Events.Writer

• Writer

ITree.Events.Exception

• Exception event

ITree.Events.ExceptionFacts

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.FailFacts

• Theorems about Failure effects

ITree.Extra.IForest

• IForest: Sets of itrees

ITree.Extra.ITrace.ITraceDefinition

ITree.Extra.ITrace.ITraceFacts

ITree.Extra.ITrace.ITracePrefix

ITree.Extra.ITrace.ITraceBind

ITree.Extra.ITrace.ITracePreds

ITree.Extra.Dijkstra.DijkstraMonad

• Dijkstra monad hierarchy
  • Ordered monads
  • Specification monads
  • Effect observations
  • Dijkstra monads

ITree.Extra.Dijkstra.IterRel

ITree.Extra.Dijkstra.PureITreeBasics

ITree.Extra.Dijkstra.PureITreeDijkstra

ITree.Extra.Dijkstra.DelaySpecMonad

ITree.Extra.Dijkstra.StateSpecT

ITree.Extra.Dijkstra.StateDelaySpec

ITree.Extra.Dijkstra.TracesIT

ITree.Extra.Dijkstra.ITreeDijkstra

ITree.Extra.Dijkstra.StateIOTrace

ITree.Extra.Secure.Labels

ITree.Extra.Secure.StrongBisimProper

ITree.Extra.Secure.SecureEqHalt

ITree.Extra.Secure.SecureEqHaltProgInsens

ITree.Extra.Secure.SecureEqEuttHalt

ITree.Extra.Secure.SecureEqEuttTrans

ITree.Extra.Secure.SecureEqWcompat

ITree.Extra.Secure.SecureEqBind

ITree.Extra.Secure.SecureEqProgInsens

ITree.Extra.Secure.SecureEqProgInsensFacts

ITree.Extra.Secure.SecureStateHandler

ITree.Extra.Secure.SecureStateHandlerPi