From 0f5087bea45be49e105727d6cee4194598474fee Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 5 Jul 2011 04:13:33 +0000
Subject: Back from Oregon commit. powerpc/*: better compilation of some
 comparisons; revised asmgenproof1. common/*: added Mem.storebytes; used to
 give semantics to memcpy builtin.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1679 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 lib/Integers.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'lib/Integers.v')

diff --git a/lib/Integers.v b/lib/Integers.v
index 30f692a..6e7a6cb 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -167,6 +167,11 @@ Definition divu (x y: int) : int :=
 Definition modu (x y: int) : int :=
   repr (Zmod (unsigned x) (unsigned y)).
 
+Definition add_carry (x y cin: int): int :=
+  if zlt (unsigned x + unsigned y + unsigned cin) modulus
+  then zero
+  else one.
+
 (** For bitwise operations, we need to convert between Coq integers [Z]
   and their bit-level representations.  Bit-level representations are
   represented as characteristic functions, that is, functions [f]
@@ -746,6 +751,11 @@ Proof.
   rewrite Zplus_0_r. apply repr_unsigned.
 Qed.
 
+Theorem add_zero_l: forall x, add zero x = x.
+Proof.
+  intros. rewrite add_commut. apply add_zero.
+Qed.
+
 Theorem add_assoc: forall x y z, add (add x y) z = add x (add y z).
 Proof.
   intros; unfold add.
-- 
cgit v1.2.3