Stream: Coq users

Topic: Decimal notation in 8.14

view this post on Zulip Yannick Forster (Nov 09 2021 at 12:07):

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).

yields 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

view this post on Zulip Jason Gross (Nov 09 2021 at 14:19):

Try importing NArith rather than BinNums?

view this post on Zulip Pierre Roux (Nov 09 2021 at 15:12):

or at the very least BinNatDef (included in NArith)

Last updated: Oct 01 2023 at 19:01 UTC