max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: System.Platform.numBits inequalities (#6247)

Browse source 
This PR adds the theorems `numBits_pos`, `le_numBits`, `numBits_le` ,
which make proving inequalities about `System.Platform.numBits` easier.
This commit is contained in:
Mac Malone 2024-11-28 16:20:47 -05:00 • committed by GitHub
parent 6d495586a1
commit 827062f807
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Init/System/Platform.lean
View file

@ -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