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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-10 12:35:22 -08:00
parent bd5c668347
commit 043fa5e16f
2 changed files with 45 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
stage0/src/Init/Data/UInt.lean generated
View file

@ -362,3 +362,24 @@ instance (a b : USize) : Decidable (a ≤ b) := USize.decLe a b
theorem USize.modnLt {m : Nat} : ∀ (u : USize), m > 0 → USize.toNat (u %ₙ m) < m
| ⟨u⟩, h => Fin.modnLt u h
theorem usizeSzEq : usizeSz = 4294967296 ∨ usizeSz = 18446744073709551616 :=
show (2 : Nat) ^ System.Platform.numBits = 4294967296 ∨ (2 : Nat) ^ System.Platform.numBits = 18446744073709551616 from
match System.Platform.numBits, System.Platform.numBitsEq with
| _, Or.inl rfl => Or.inl (decide! : (2 : Nat) ^ 32 = 4294967296)
| _, Or.inr rfl => Or.inr (decide! : (2 : Nat) ^ 64 = 18446744073709551616)
@[extern "lean_usize_of_nat"]
def USize.ofNat32 (n : @& Nat) (h : n < 4294967296) : USize := {
val := {
val := n,
isLt := match usizeSz, usizeSzEq with
| _, Or.inl rfl => h
| _, Or.inr rfl => Nat.ltTrans h (decide! : Less 4294967296 18446744073709551616)
}
}
@[extern "lean_usize_of_nat"]
def USize.ofNatCore (n : @& Nat) (h : n < usizeSz) : USize := {
val := { val := n, isLt := h }
}

24
stage0/stdlib/Init/Data/UInt.c generated
View file

@ -142,6 +142,7 @@ uint8_t l_UInt64_decLt(uint64_t, uint64_t);
uint64_t l_Nat_toUInt64(lean_object*);
lean_object* l_Init_Data_UInt___instance__11___boxed(lean_object*, lean_object*);
uint8_t l_Init_Data_UInt___instance__64(size_t, size_t);
size_t lean_usize_of_nat(lean_object*);
lean_object* l_UInt64_mul___boxed(lean_object*, lean_object*);
lean_object* l_Init_Data_UInt___instance__16;
size_t l_USize_shiftLeft(size_t, size_t);
@ -256,6 +257,7 @@ lean_object* lean_uint64_to_nat(uint64_t);
lean_object* l_Init_Data_UInt___instance__9;
lean_object* l_UInt16_mod___boxed(lean_object*, lean_object*);
lean_object* l_USize_toUInt32___boxed(lean_object*);
lean_object* l_USize_ofNatCore___boxed(lean_object*, lean_object*);
uint32_t l_UInt32_lor(uint32_t, uint32_t);
lean_object* l_Init_Data_UInt___instance__5;
lean_object* l_UInt16_lor___boxed(lean_object*, lean_object*);
@ -293,9 +295,11 @@ uint8_t l_UInt16_decLe(uint16_t, uint16_t);
uint8_t l_UInt32_decLe(uint32_t, uint32_t);
lean_object* l_Init_Data_UInt___instance__12___boxed(lean_object*, lean_object*);
lean_object* l_Init_Data_UInt___instance__17;
lean_object* l_USize_ofNat32___boxed(lean_object*, lean_object*);
lean_object* l_Init_Data_UInt___instance__7___closed__1;
lean_object* lean_uint32_to_nat(uint32_t);
lean_object* l_Init_Data_UInt___instance__55___closed__1;
size_t lean_usize_of_nat(lean_object*);
lean_object* l_Init_Data_UInt___instance__47;
lean_object* l_UInt8_decEq___boxed(lean_object*, lean_object*);
uint8_t l_Init_Data_UInt___instance__26(uint16_t, uint16_t);
@ -2474,6 +2478,26 @@ x_6 = lean_box(x_5);
return x_6;
}
}
lean_object* l_USize_ofNat32___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
size_t x_3; lean_object* x_4;
x_3 = lean_usize_of_nat(x_1);
lean_dec(x_1);
x_4 = lean_box_usize(x_3);
return x_4;
}
}
lean_object* l_USize_ofNatCore___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
size_t x_3; lean_object* x_4;
x_3 = lean_usize_of_nat(x_1);
lean_dec(x_1);
x_4 = lean_box_usize(x_3);
return x_4;
}
}
lean_object* initialize_Init_Data_Fin_Basic(lean_object*);
lean_object* initialize_Init_System_Platform(lean_object*);
static bool _G_initialized = false;