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

chore: add numBitsEq

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-10 11:59:16 -08:00
parent 2daeb195b5
commit 1c01bd59be
1 changed files with 10 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

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