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

Notation "'Ox' a" := (Z.of_N (hex a)).

Goal Ox"41" = 65%Z.
(* Goal: @eq Z (Z.of_N (hex (String (Ascii.Ascii false false true 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.
