coinductive A library for implementing co-inductive types in Lean An implementation of (co-inductive) interaction trees in Lean