(* Author: Andreas Lochbihler, ETH Zurich Author: Peter Gammie *) section ‹A codatatype of infinite binary trees› theory Cotree imports Main Applicative_Lifting.Applicative "HOL-Library.BNF_Corec" "HOL-Library.Adhoc_Overloading" begin context notes [[bnf_internals]] begin