61 lines
1.4 KiB
Coq
61 lines
1.4 KiB
Coq
(* From https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#number-notations *)
|
|
|
|
Inductive radix2: Set :=
|
|
| x0: radix2
|
|
| x2p0: radix2 -> radix2
|
|
| x2p1: radix2 -> radix2.
|
|
|
|
Print Decimal.
|
|
|
|
Definition of_uint_dec (u : Decimal.uint) : option radix2 :=
|
|
let fix f u := match u with
|
|
| Decimal.Nil => Some x0
|
|
| Decimal.D0 u =>
|
|
match f u with
|
|
| Some u => Some (x2p0 u)
|
|
| None => None
|
|
end
|
|
| Decimal.D1 u =>
|
|
match f u with
|
|
| Some u => Some (x2p1 u)
|
|
| None => None
|
|
end
|
|
| _ => None end in
|
|
f (Decimal.rev u).
|
|
|
|
Definition of_uint (u : Number.uint) : option radix2 :=
|
|
match u with
|
|
| Number.UIntDecimal u => of_uint_dec u
|
|
| Number.UIntHexadecimal _ => None
|
|
end.
|
|
|
|
(* Printing stuff *)
|
|
Definition to_uint_dec (x : radix2) : Decimal.uint :=
|
|
let fix f x :=
|
|
match x with
|
|
| x0 => Decimal.Nil
|
|
| x2p0 x => Decimal.D0 (f x)
|
|
| x2p1 x => Decimal.D1 (f x)
|
|
end in
|
|
Decimal.rev (f x).
|
|
Definition to_uint (x : radix2) : Number.uint := Number.UIntDecimal (to_uint_dec x).
|
|
|
|
Declare Scope radix2_scope.
|
|
Delimit Scope radix2_scope with r2.
|
|
Number Notation radix2 of_uint to_uint : radix2_scope.
|
|
|
|
Check 01%r2.
|
|
(* 01%r2 : radix2 *)
|
|
|
|
Fail Check 02%r2.
|
|
(*
|
|
The command has indeed failed with message:
|
|
Cannot interpret this number as a value of type radix2
|
|
*)
|
|
|
|
Check (x2p1 x0).
|
|
(* 1%r2 : radix2 *)
|
|
|
|
Check (x2p1 (x2p0 x0)).
|
|
(* 01%r2 : radix2 *)
|