diff options
Diffstat (limited to 'theories/NArith')
| -rw-r--r-- | theories/NArith/BinNat.v | 2 | ||||
| -rw-r--r-- | theories/NArith/BinNatDef.v | 3 |
2 files changed, 5 insertions, 0 deletions
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 5d3ec5abc7..bd27f94abd 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -930,6 +930,8 @@ Bind Scope N_scope with N.t N. (** Exportation of notations *) +Numeral Notation N N.of_uint N.to_uint : N_scope. + Infix "+" := N.add : N_scope. Infix "-" := N.sub : N_scope. Infix "*" := N.mul : N_scope. diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v index 8bbecf9acb..be12fffaaf 100644 --- a/theories/NArith/BinNatDef.v +++ b/theories/NArith/BinNatDef.v @@ -402,6 +402,9 @@ Definition to_uint n := Definition to_int n := Decimal.Pos (to_uint n). +Numeral Notation N of_uint to_uint : N_scope. + End N. +(** Re-export the notation for those who just [Import NatIntDef] *) Numeral Notation N N.of_uint N.to_uint : N_scope. |