Documentation

LeanPool.Lean4Itree

Coinductive Interaction Trees using QPFs #

Source: arxiv:1906.00046, doi:10.1145/3371119 Authors: Paul Mure, Joonhyup Lee Status: verified Main declarations: Lean4Itree.ITree, Lean4Itree.ITree.ieq_iff_eq, Lean4Itree.plfp_acc Tags: coinduction, interaction-trees, monads, qpf, semantics MSC: 68Q55, 18C50, 68N18