From 1c01bd59bef0dd65aa84c15775ded71c382ac430 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 10 Nov 2020 11:59:16 -0800
Subject: [PATCH] chore: add `numBitsEq`

---
 src/Init/System/Platform.lean | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/Init/System/Platform.lean b/src/Init/System/Platform.lean
index d2460204a4..e61ad8a17e 100644
--- a/src/Init/System/Platform.lean
+++ b/src/Init/System/Platform.lean
@@ -9,12 +9,20 @@ import Init.Data.Nat.Basic
 namespace System
 namespace Platform
 
-@[extern "lean_system_platform_nbits"] constant getNumBits : Unit → Nat
+@[extern "lean_system_platform_nbits"] constant getNumBits : Unit → { n : Nat // n = 32 ∨ n = 64 } :=
+  fun _ => ⟨64, Or.inr rfl⟩ -- inhabitant
+
 @[extern "lean_system_platform_windows"] constant getIsWindows : Unit → Bool
 @[extern "lean_system_platform_osx"] constant getIsOSX : Unit → Bool
 
-def numBits : Nat := getNumBits ()
+def numBits : Nat := getNumBits () $.val
+
+theorem numBitsEq : numBits = 32 ∨ numBits = 64 :=
+  getNumBits () $.property
+
 def isWindows : Bool := getIsWindows ()
+
+
 def isOSX : Bool := getIsOSX ()
 
 end Platform