The file https://coq.inria.fr/library/Coq.Numbers.BinNums.html says
Numbers in N will also be denoted using a decimal notation; e.g. 6%N will abbreviate Npos (xO (xI xH)). But under
8.14 for me
Require Import BinNums. Open Scope N_scope. Check ((6%N) : N).
The term "6" has type "nat" while it is expected to have type "N".. Am I doing something wrong? This might be related to
Removed: Decimal-only number notations which were deprecated in 8.12. (#13842, by Pierre Roux). in the changelog, but maybe not
Try importing NArith rather than BinNums?
or at the very least BinNatDef (included in NArith)
Last updated: Feb 06 2023 at 13:03 UTC