Require Export bbv.BinNotation.
Require Export bbv.ReservedNotations.
Require Import Coq.ZArith.BinInt.

Notation "'Ob' a" := (Z.of_N (bin a)).

Goal Ob"01000001" = 65%Z.
(* Goal: @eq Z (Z.of_N (bin (String (Ascii.Ascii false false false false true true false false) (String (Ascii.Ascii true false false false true true false false) (String (Ascii.Ascii false false false false true true false false) (String (Ascii.Ascii false false false false true true false false) (String (Ascii.Ascii false false false false true true false false) (String (Ascii.Ascii false false false false true true false false) (String (Ascii.Ascii false false false false true true false false) (String (Ascii.Ascii true false false false true true false false) EmptyString)))))))))) (Zpos (xI (xO (xO (xO (xO (xO xH))))))) *)
Proof. reflexivity. Qed.
