Require Export bbv.HexNotation.
Require Import bbv.WordScope.

Notation "'Ox' a" := (NToWord _ (hex a)) (at level 50).

Notation "sz ''h' a" := (NToWord sz (hex a)) (at level 50).

Goal 8'h"a" = WO~0~0~0~0~1~0~1~0.
(* Goal: @eq (word (S (S (S (S (S (S (S O)))))))) (natToWord (S (S (S (S (S (S (S O))))))) (bin (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))))))))) (@WS true (S (S (S (S (S (S O)))))) (@WS false (S (S (S (S (S O))))) (@WS false (S (S (S (S O)))) (@WS false (S (S (S O))) (@WS false (S (S O)) (@WS false (S O) (@WS true O WO))))))) *)
Proof. reflexivity. Qed.

Goal Ox"41" = WO~1~0~0~0~0~0~1.
(* Goal: @eq (word (S (S (S (S (S (S (S O)))))))) (natToWord (S (S (S (S (S (S (S O))))))) (bin (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))))))))) (@WS true (S (S (S (S (S (S O)))))) (@WS false (S (S (S (S (S O))))) (@WS false (S (S (S (S O)))) (@WS false (S (S (S O))) (@WS false (S (S O)) (@WS false (S O) (@WS true O WO))))))) *)
Proof. reflexivity. Qed.

Notation "sz ''b' a" := (natToWord sz (bin a)) (at level 50).

Notation "''b' a" := (natToWord _ (bin a)) (at level 50).

Goal 'b"00001010" = WO~0~0~0~0~1~0~1~0.
(* Goal: @eq (word (S (S (S (S (S (S (S O)))))))) (natToWord (S (S (S (S (S (S (S O))))))) (bin (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))))))))) (@WS true (S (S (S (S (S (S O)))))) (@WS false (S (S (S (S (S O))))) (@WS false (S (S (S (S O)))) (@WS false (S (S (S O))) (@WS false (S (S O)) (@WS false (S O) (@WS true O WO))))))) *)
Proof. reflexivity. Qed.

Goal 'b"1000001" = WO~1~0~0~0~0~0~1.
(* Goal: @eq (word (S (S (S (S (S (S (S O)))))))) (natToWord (S (S (S (S (S (S (S O))))))) (bin (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))))))))) (@WS true (S (S (S (S (S (S O)))))) (@WS false (S (S (S (S (S O))))) (@WS false (S (S (S (S O)))) (@WS false (S (S (S O))) (@WS false (S (S O)) (@WS false (S O) (@WS true O WO))))))) *)
Proof. reflexivity. Qed.


