From 827062f807cd869709fb71d5d04a00ff10320be3 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Thu, 28 Nov 2024 16:20:47 -0500 Subject: [PATCH] feat: `System.Platform.numBits` inequalities (#6247) This PR adds the theorems `numBits_pos`, `le_numBits`, `numBits_le` , which make proving inequalities about `System.Platform.numBits` easier. --- src/Init/System/Platform.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/Init/System/Platform.lean b/src/Init/System/Platform.lean index 9db2b508f4..062532123e 100644 --- a/src/Init/System/Platform.lean +++ b/src/Init/System/Platform.lean @@ -23,5 +23,14 @@ def isEmscripten : Bool := getIsEmscripten () /-- The LLVM target triple of the current platform. Empty if missing at Lean compile time. -/ def target : String := getTarget () +theorem numBits_pos : 0 < numBits := by + cases numBits_eq <;> next h => simp [h] + +theorem le_numBits : 32 ≤ numBits := by + cases numBits_eq <;> next h => simp [h] + +theorem numBits_le : numBits ≤ 64 := by + cases numBits_eq <;> next h => simp [h] + end Platform end System