CODEWITHSUNDEEP
coq
Tony Peterson
Tony Peterson

Reputation: 21192

Why are all numeric literals in Coq showing nat type?

I'm trying to use larger numbers in Coq where the built in Nat type isn't appropriate. So I'm trying to establish particular values with a positive type or N type.

According to the Standard Library documentation for BinNums:

Numbers in positive will also be denoted using a decimal notation; e.g. 6%positive will abbreviate xO (xI xH)

Numbers in N will also be denoted using a decimal notation; e.g. 6%N will abbreviate Npos (xO (xI xH))

But my Coq code is still giving me Nat typed numbers:

From Coq
Require Import BinNums.

Definition sixp := 6%positive.
Definition sixn := 6%N.

Check sixp.
Check sixn.

Results:

sixp
     : nat

sixn
     : nat

Where am I going wrong?

Upvotes: 3

Views: 357

Answers (2)

Anton Trunov
Anton Trunov

Reputation: 15424

From Coq Require Import NArith.

should solve this issue.

The problem here is that BinNums does not export any module that defines the corresponding numerical notation, see here for more detail.

The numerical notations you need are located in BinPosDef and BinNatDef modules and NArith re-exports those.

Upvotes: 3

Tony Peterson
Tony Peterson

Reputation: 21192

I found one way to work around this. Using the AltBinNotations module.

I don't know if there is a better way to do this.

Note: up to Coq 8.8, literals in types positive, N, Z were parsed and printed using a native ML library of arbitrary precision integers named bigint.ml. From 8.9, the default is to parse and print using a Coq library converting sequences of digits, hence reducing the amount of ML code to trust. But this method is slower. This file then gives access to the legacy method, trading efficiency against a larger ML trust base relying on bigint.ml.

From Coq
Require Import BinNums.

From Coq
Require Import AltBinNotations.

Definition sixp : positive := (6%positive).

sixp is defined.

sixp : positive

Upvotes: 1

Related Questions