diff options
Diffstat (limited to 'theories/PArith/BinPosDef.v')
-rw-r--r-- | theories/PArith/BinPosDef.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index 4f8d9ee27..fcc12ab45 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -18,7 +18,7 @@ Require Export BinNums. -(** Postfix notation for positive numbers, allowing to mimic +(** Postfix notation for positive numbers, which allows mimicking the position of bits in a big-endian representation. For instance, we can write [1~1~0] instead of [(xO (xI xH))] for the number 6 (which is 110 in binary notation). @@ -557,4 +557,4 @@ Fixpoint of_succ_nat (n:nat) : positive := | S x => succ (of_succ_nat x) end. -End Pos.
\ No newline at end of file +End Pos. |