1. Geb
  2. Prototypes
  3. Computability
  4. BitTree
  5. Elias
  6. CodeExamples
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 import Geb.Prototypes.Computability.BitTree.Elias.Tree -- shake: keep
set_option doc.verso true

Elias code boundary examples

The calculations check the shifted delta code at its first binary-size boundaries and complete tree decoding at empty, valid and trailing-input cases.

Tags

prefix code, verification

open Geb.BitTree.Eliasexample : encodeNat 0 = [true] := rflexample : encodeNat 1 = [false, true, false, false] := rflexample : encodeNat 2 = [false, true, false, true] := rflexample : encodeNat 3 = [false, true, true, false, false] := rflexample : encode (Geb.BitTree.leaf []) = [false, true] := rflexample : validBool [false, true] = true := rflexample : validBool [] = false := rflexample : validBool [false, true, true] = false := rfl