From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- theories/ZArith/BinIntDef.v | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) (limited to 'theories/ZArith/BinIntDef.v') diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v index db4de0b9..8cb62622 100644 --- a/theories/ZArith/BinIntDef.v +++ b/theories/ZArith/BinIntDef.v @@ -14,6 +14,10 @@ Require Import BinPos BinNat. Local Open Scope Z_scope. +Local Notation "0" := Z0. +Local Notation "1" := (Zpos 1). +Local Notation "2" := (Zpos 2). + (***********************************************************) (** * Binary Integers, Definitions of Operations *) (***********************************************************) @@ -53,7 +57,7 @@ Definition succ_double x := Definition pred_double x := match x with - | 0 => -1 + | 0 => neg 1 | neg p => neg p~1 | pos p => pos (Pos.pred_double p) end. @@ -104,7 +108,7 @@ Definition succ x := x + 1. (** ** Predecessor *) -Definition pred x := x + -1. +Definition pred x := x + neg 1. (** ** Subtraction *) @@ -171,7 +175,7 @@ Definition sgn z := match z with | 0 => 0 | pos p => 1 - | neg p => -1 + | neg p => neg 1 end. (** Boolean equality and comparisons *) @@ -635,4 +639,9 @@ Definition lxor a b := | neg a, neg b => of_N (N.lxor (Pos.pred_N a) (Pos.pred_N b)) end. +Numeral Notation Z of_int to_int : Z_scope. + End Z. + +(** Re-export the notation for those who just [Import BinIntDef] *) +Numeral Notation Z Z.of_int Z.to_int : Z_scope. -- cgit v1.2.3