From bdec4c8799168f4edfb9f29a318d7fcaf7cb440f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 8 Jan 2014 16:53:08 -0800
Subject: [PATCH] refactor(builtin/Nat): mark constants as opaque

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/builtin/Nat.lean      |   4 ++++
 src/builtin/obj/Nat.olean | Bin 15289 -> 15347 bytes
 2 files changed, 4 insertions(+)

diff --git a/src/builtin/Nat.lean b/src/builtin/Nat.lean
index bfb1963ff..d3612f71b 100644
--- a/src/builtin/Nat.lean
+++ b/src/builtin/Nat.lean
@@ -237,6 +237,10 @@ theorem le::antisym {a b : Nat} (H1 : a ≤ b) (H2 : b ≤ a) : a = b
           ...  =  a  + w1 : { symm L2 }
           ...  =  b       : Hw1
 
+set::opaque add true
+set::opaque mul true
+set::opaque le true
+set::opaque id true
 set::opaque ge true
 set::opaque lt true
 set::opaque gt true
diff --git a/src/builtin/obj/Nat.olean b/src/builtin/obj/Nat.olean
index c5df55a1e5206436592593298db6f5917b196923..e07e061551ec3f8209bbcf52167699ce40d7199e 100644
GIT binary patch
delta 59
scmdm4{<(ZZv$cL=N(uv`e?cMx3j+|a=a%Lmb8}LWd6_8;lPjzp0od;iSO5S3

delta 11
ScmexdzO#Hov-RY?)@A@FlLg8E