1. Geb
  2. Prototypes
  3. Computability
  4. BitTree
Imports
/- Copyright (c) 2026 Terence Rokop. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Terence Rokop -/ module public import Geb.Prototypes.Computability.BitTree.Encoding public import Geb.Prototypes.Computability.BitTree.Bound public import Geb.Prototypes.Computability.BitTree.BinaryMachine public import Geb.Prototypes.Computability.BitTree.Examples public import Geb.Prototypes.Computability.BitTree.Elias
set_option doc.verso true

Binary trees with bitstring leaves

The encoding, unified recognizer, correctness proofs and machine resource bounds.