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-13 16:32:05 -08:00
parent ffc4abed32
commit 646f2bdefe
16 changed files with 303 additions and 191 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
stage0/src/CMakeLists.txt generated
View file

@ -311,6 +311,14 @@ find_package(PythonInterp)
include_directories(${CMAKE_BINARY_DIR}/include)
# libleancpp and the stdlib libraries are cyclically dependent. This works by default on macOS, which also doesn't like
# the linker flags necessary on other platforms.
if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
set(LEANC_STATIC_LINKER_FLAGS "-lleancpp -lInit -lStd -lLean")
else()
set(LEANC_STATIC_LINKER_FLAGS "-Wl,--start-group -lleancpp -lInit -lStd -lLean -Wl,--end-group")
endif()
if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
set(LEANC_SHARED_LINKER_FLAGS "${LEANC_SHARED_LINKER_FLAGS} -fPIC")
endif()

2
stage0/src/Init/Data/Char/Basic.lean generated
View file

@ -30,7 +30,7 @@ instance (a b : Char) : Decidable (a ≤ b) :=
abbrev isValidCharNat (n : Nat) : Prop :=
n < 0xd800 ∨ (0xdfff < n ∧ n < 0x110000)
theorem isValidUInt32 (n : Nat) (h : isValidCharNat n) : n < uint32Sz := by
theorem isValidUInt32 (n : Nat) (h : isValidCharNat n) : n < UInt32.size := by
match h with
| Or.inl h =>
apply Nat.ltTrans h

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

@ -111,7 +111,7 @@ instance (a b : UInt16) : Decidable (a ≤ b) := UInt16.decLe a b
@[extern "lean_uint32_of_nat"]
def UInt32.ofNat (n : @& Nat) : UInt32 := ⟨Fin.ofNat n⟩
@[extern "lean_uint32_of_nat"]
def UInt32.ofNat' (n : Nat) (h : n < uint32Sz) : UInt32 := ⟨⟨n, h⟩⟩
def UInt32.ofNat' (n : Nat) (h : n < UInt32.size) : UInt32 := ⟨⟨n, h⟩⟩
abbrev Nat.toUInt32 := UInt32.ofNat
@[extern c inline "#1 + #2"]
def UInt32.add (a b : UInt32) : UInt32 := ⟨a.val + b.val⟩
@ -215,7 +215,7 @@ def UInt64.decLe (a b : UInt64) : Decidable (a ≤ b) :=
instance (a b : UInt64) : Decidable (a < b) := UInt64.decLt a b
instance (a b : UInt64) : Decidable (a ≤ b) := UInt64.decLe a b
theorem usizeSzGt0 : usizeSz > 0 :=
theorem usizeSzGt0 : USize.size > 0 :=
Nat.posPowOfPos System.Platform.numBits (Nat.zeroLtSucc _)
@[extern "lean_usize_of_nat"]

12
stage0/src/Init/Fix.lean generated
View file

@ -13,7 +13,7 @@ def bfix1 {α β : Type u} (base : α → β) (rec : (α → β) → α → β)
@[extern c inline "lean_fixpoint(#4, #5)"]
def fixCore1 {α β : Type u} (base : @& (α → β)) (rec : (α → β) → α → β) : α → β :=
bfix1 base rec usizeSz
bfix1 base rec USize.size
@[inline] def fixCore {α β : Type u} (base : @& (α → β)) (rec : (α → β) → α → β) : α → β :=
fixCore1 base rec
@ -30,7 +30,7 @@ def bfix2 {α₁ α₂ β : Type u} (base : α₁ → α₂ → β) (rec : (α
@[extern c inline "lean_fixpoint2(#5, #6, #7)"]
def fixCore2 {α₁ α₂ β : Type u} (base : α₁ → α₂ → β) (rec : (α₁ → α₂ → β) → α₁ → α₂ → β) : α₁ → α₂ → β :=
bfix2 base rec usizeSz
bfix2 base rec USize.size
@[inline] def fix2 {α₁ α₂ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → β) → α₁ → α₂ → β) : α₁ → α₂ → β :=
fixCore2 (fun _ _ => arbitrary β) rec
@ -41,7 +41,7 @@ def bfix3 {α₁ α₂ α₃ β : Type u} (base : α₁ → α₂ → α₃ →
@[extern c inline "lean_fixpoint3(#6, #7, #8, #9)"]
def fixCore3 {α₁ α₂ α₃ β : Type u} (base : α₁ → α₂ → α₃ → β) (rec : (α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) : α₁ → α₂ → α₃ → β :=
bfix3 base rec usizeSz
bfix3 base rec USize.size
@[inline] def fix3 {α₁ α₂ α₃ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) : α₁ → α₂ → α₃ → β :=
fixCore3 (fun _ _ _ => arbitrary β) rec
@ -52,7 +52,7 @@ def bfix4 {α₁ α₂ α₃ α₄ β : Type u} (base : α₁ → α₂ → α
@[extern c inline "lean_fixpoint4(#7, #8, #9, #10, #11)"]
def fixCore4 {α₁ α₂ α₃ α₄ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → β) (rec : (α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) : α₁ → α₂ → α₃ → α₄ → β :=
bfix4 base rec usizeSz
bfix4 base rec USize.size
@[inline] def fix4 {α₁ α₂ α₃ α₄ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) : α₁ → α₂ → α₃ → α₄ → β :=
fixCore4 (fun _ _ _ _ => arbitrary β) rec
@ -63,7 +63,7 @@ def bfix5 {α₁ α₂ α₃ α₄ α₅ β : Type u} (base : α₁ → α₂
@[extern c inline "lean_fixpoint5(#8, #9, #10, #11, #12, #13)"]
def fixCore5 {α₁ α₂ α₃ α₄ α₅ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) : α₁ → α₂ → α₃ → α₄ → α₅ → β :=
bfix5 base rec usizeSz
bfix5 base rec USize.size
@[inline] def fix5 {α₁ α₂ α₃ α₄ α₅ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) : α₁ → α₂ → α₃ → α₄ → α₅ → β :=
fixCore5 (fun _ _ _ _ _ => arbitrary β) rec
@ -74,7 +74,7 @@ def bfix6 {α₁ α₂ α₃ α₄ α₅ α₆ β : Type u} (base : α₁ → α
@[extern c inline "lean_fixpoint6(#9, #10, #11, #12, #13, #14, #15)"]
def fixCore6 {α₁ α₂ α₃ α₄ α₅ α₆ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) : α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β :=
bfix6 base rec usizeSz
bfix6 base rec USize.size
@[inline] def fix6 {α₁ α₂ α₃ α₄ α₅ α₆ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) : α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β :=
fixCore6 (fun _ _ _ _ _ _ => arbitrary β) rec

75
stage0/src/Init/Prelude.lean generated
View file

@ -596,9 +596,14 @@ instance {n} : HasLessEq (Fin n) := ⟨Fin.le⟩
instance Fin.decLt {n} (a b : Fin n) : Decidable (Less a b) := Nat.decLt ..
instance Fin.decLe {n} (a b : Fin n) : Decidable (LessEq a b) := Nat.decLe ..
def uint8Sz : Nat := 256
def UInt8.size : Nat := 256
structure UInt8 :=
(val : Fin uint8Sz)
(val : Fin UInt8.size)
@[extern "lean_uint8_of_nat"]
def UInt8.ofNatCore (n : @& Nat) (h : Less n UInt8.size) : UInt8 := {
val := { val := n, isLt := h }
}
set_option bootstrap.gen_matcher_code false in
@[extern c inline "#1 == #2"]
@ -610,12 +615,17 @@ def UInt8.decEq (a b : UInt8) : Decidable (Eq a b) :=
instance : DecidableEq UInt8 := UInt8.decEq
instance : Inhabited UInt8 := {
default := { val := { val := 0, isLt := decide! } }
default := UInt8.ofNatCore 0 decide!
}
def uint16Sz : Nat := 65536
def UInt16.size : Nat := 65536
structure UInt16 :=
(val : Fin uint16Sz)
(val : Fin UInt16.size)
@[extern "lean_uint16_of_nat"]
def UInt16.ofNatCore (n : @& Nat) (h : Less n UInt16.size) : UInt16 := {
val := { val := n, isLt := h }
}
set_option bootstrap.gen_matcher_code false in
@[extern c inline "#1 == #2"]
@ -627,12 +637,17 @@ def UInt16.decEq (a b : UInt16) : Decidable (Eq a b) :=
instance : DecidableEq UInt16 := UInt16.decEq
instance : Inhabited UInt16 := {
default := { val := { val := 0, isLt := decide! } }
default := UInt16.ofNatCore 0 decide!
}
def uint32Sz : Nat := 4294967296
def UInt32.size : Nat := 4294967296
structure UInt32 :=
(val : Fin uint32Sz)
(val : Fin UInt32.size)
@[extern "lean_uint32_of_nat"]
def UInt32.ofNatCore (n : @& Nat) (h : Less n UInt32.size) : UInt32 := {
val := { val := n, isLt := h }
}
@[extern "lean_uint32_to_nat"]
def UInt32.toNat (n : UInt32) : Nat := n.val.val
@ -647,7 +662,7 @@ def UInt32.decEq (a b : UInt32) : Decidable (Eq a b) :=
instance : DecidableEq UInt32 := UInt32.decEq
instance : Inhabited UInt32 := {
default := { val := { val := 0, isLt := decide! } }
default := UInt32.ofNatCore 0 decide!
}
def UInt32.lt (a b : UInt32) : Prop := Less a.val b.val
@ -671,15 +686,15 @@ def UInt32.decLe (a b : UInt32) : Decidable (LessEq a b) :=
instance (a b : UInt32) : Decidable (Less a b) := UInt32.decLt a b
instance (a b : UInt32) : Decidable (LessEq a b) := UInt32.decLe a b
@[extern "lean_uint32_of_nat"]
def UInt32.ofNatCore (n : @& Nat) (h : Less n uint32Sz) : UInt32 := {
def UInt64.size : Nat := 18446744073709551616
structure UInt64 :=
(val : Fin UInt64.size)
@[extern "lean_uint64_of_nat"]
def UInt64.ofNatCore (n : @& Nat) (h : Less n UInt64.size) : UInt64 := {
val := { val := n, isLt := h }
}
def uint64Sz : Nat := 18446744073709551616
structure UInt64 :=
(val : Fin uint64Sz)
set_option bootstrap.gen_matcher_code false in
@[extern c inline "#1 == #2"]
def UInt64.decEq (a b : UInt64) : Decidable (Eq a b) :=
@ -690,19 +705,24 @@ def UInt64.decEq (a b : UInt64) : Decidable (Eq a b) :=
instance : DecidableEq UInt64 := UInt64.decEq
instance : Inhabited UInt64 := {
default := { val := { val := 0, isLt := decide! } }
default := UInt64.ofNatCore 0 decide!
}
def usizeSz : Nat := pow 2 System.Platform.numBits
def USize.size : Nat := pow 2 System.Platform.numBits
theorem usizeSzEq : Or (Eq usizeSz 4294967296) (Eq usizeSz 18446744073709551616) :=
theorem usizeSzEq : Or (Eq USize.size 4294967296) (Eq USize.size 18446744073709551616) :=
show Or (Eq (pow 2 System.Platform.numBits) 4294967296) (Eq (pow 2 System.Platform.numBits) 18446744073709551616) from
match System.Platform.numBits, System.Platform.numBitsEq with
| _, Or.inl rfl => Or.inl (decide! : (Eq (pow 2 32) (4294967296:Nat)))
| _, Or.inr rfl => Or.inr (decide! : (Eq (pow 2 64) (18446744073709551616:Nat)))
structure USize :=
(val : Fin usizeSz)
(val : Fin USize.size)
@[extern "lean_usize_of_nat"]
def USize.ofNatCore (n : @& Nat) (h : Less n USize.size) : USize := {
val := { val := n, isLt := h }
}
set_option bootstrap.gen_matcher_code false in
@[extern c inline "#1 == #2"]
@ -714,24 +734,19 @@ def USize.decEq (a b : USize) : Decidable (Eq a b) :=
instance : DecidableEq USize := USize.decEq
instance : Inhabited USize := {
default := { val := { val := 0, isLt := match usizeSz, usizeSzEq with | _, Or.inl rfl => decide! | _, Or.inr rfl => decide! } }
default := USize.ofNatCore 0 (match USize.size, usizeSzEq with | _, Or.inl rfl => decide! | _, Or.inr rfl => decide!)
}
@[extern "lean_usize_of_nat"]
def USize.ofNat32 (n : @& Nat) (h : Less n 4294967296) : USize := {
val := {
val := n,
isLt := match usizeSz, usizeSzEq with
isLt := match USize.size, 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 : Less n usizeSz) : USize := {
val := { val := n, isLt := h }
}
abbrev Nat.isValidChar (n : Nat) : Prop :=
Or (Less n 0xd800) (And (Less 0xdfff n) (Less n 0x110000))
@ -744,10 +759,10 @@ structure Char :=
(val : UInt32)
(valid : val.isValidChar)
private theorem validCharIsUInt32 {n : Nat} (h : n.isValidChar) : Less n uint32Sz :=
private theorem validCharIsUInt32 {n : Nat} (h : n.isValidChar) : Less n UInt32.size :=
match h with
| Or.inl h => Nat.ltTrans h (decide! : Less 55296 uint32Sz)
| Or.inr ⟨_, h⟩ => Nat.ltTrans h (decide! : Less 1114112 uint32Sz)
| Or.inl h => Nat.ltTrans h (decide! : Less 55296 UInt32.size)
| Or.inr ⟨_, h⟩ => Nat.ltTrans h (decide! : Less 1114112 UInt32.size)
@[extern "lean_uint32_of_nat"]
private def Char.ofNatAux (n : Nat) (h : n.isValidChar) : Char :=
@ -1366,7 +1381,7 @@ def mkStr (p : Name) (s : String) : Name :=
@[export lean_name_mk_numeral]
def mkNum (p : Name) (v : Nat) : Name :=
Name.num p v (mixHash (hash p) (dite (Less v usizeSz) (fun h => USize.ofNatCore v h) (fun _ => USize.ofNat32 17 decide!)))
Name.num p v (mixHash (hash p) (dite (Less v USize.size) (fun h => USize.ofNatCore v h) (fun _ => USize.ofNat32 17 decide!)))
def mkSimple (s : String) : Name :=
mkStr Name.anonymous s

2
stage0/src/Lean/Compiler/IR/EmitC.lean generated
View file

@ -474,7 +474,7 @@ def quoteString (s : String) : String :=
def emitNumLit (t : IRType) (v : Nat) : M Unit := do
if t.isObj then
if v < uint32Sz then
if v < UInt32.size then
emit "lean_unsigned_to_nat("; emit v; emit "u)"
else
emit "lean_cstr_to_nat(\""; emit v; emit "\")"

4
stage0/src/Lean/Data/Json/Parser.lean generated
View file

@ -203,7 +203,7 @@ def num : Quickparse JsonNumber := do
if c? = some '.' then
skip
let (n, d) ← natNumDigits
if d > usizeSz then fail "too many decimals"
if d > USize.size then fail "too many decimals"
let mantissa' := res.mantissa * (10^d : Nat) + n
let exponent' := res.exponent + d
pure $ JsonNumber.mk mantissa' exponent'
@ -220,7 +220,7 @@ def num : Quickparse JsonNumber := do
else do
if c = '+' then skip
let n ← natMaybeZero
if n > usizeSz then fail "exp too large"
if n > USize.size then fail "exp too large"
pure (res.shiftl n)
else
pure res

2
stage0/src/Std/Data/PersistentArray.lean generated
View file

@ -129,7 +129,7 @@ def mkNewTail (t : PersistentArray α) : PersistentArray α :=
shift := t.shift + initShift,
tailOff := t.size }
def tooBig : Nat := usizeSz / 8
def tooBig : Nat := USize.size / 8
def push (t : PersistentArray α) (a : α) : PersistentArray α :=
let r := { t with tail := t.tail.push a, size := t.size + 1 }

4
stage0/src/bin/leanc.in generated
View file

@ -16,9 +16,7 @@ bindir=$(dirname $0)
cflags=("-I$bindir/../include")
ldflags=("-L$bindir/../lib/lean" "-lgmp" @LEANC_EXTRA_FLAGS@)
# static linker flags
# NOTE: libleancpp and libInit are cyclically dependent
ldflags_ext=("-lleancpp" "-lInit" "-lStd" "-lLean" "-lleancpp" "-lInit" "-lStd" "-lLean" "-lStd")
ldflags_ext=(@LEANC_STATIC_LINKER_FLAGS@)
for arg in "$@"; do
# passed -shared ~> switch to shared linker flags
[[ $arg == "-shared" ]] && ldflags_ext=(@LEANC_SHARED_LINKER_FLAGS@)

240
stage0/stdlib/Init/Prelude.c generated
View file

@ -34,7 +34,7 @@ lean_object* l_EStateM_tryCatch(lean_object*, lean_object*, lean_object*);
lean_object* l_UInt32_decLe___boxed(lean_object*, lean_object*);
lean_object* l___private_Init_Prelude_0__String_utf8ByteSizeAux_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_erase_macro_scopes(lean_object*);
lean_object* l_Init_Prelude___instance__32;
uint64_t l_Init_Prelude___instance__32;
lean_object* l_withTheReader(lean_object*, lean_object*);
lean_object* l_Nat_sub___boxed(lean_object*, lean_object*);
lean_object* l_Functor_mapConst___default(lean_object*);
@ -74,6 +74,7 @@ lean_object* l_String_mk___boxed(lean_object*);
lean_object* l_Nat_decEq_match__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_read___at_Lean_Macro_Init_Prelude___instance__79___spec__1(lean_object*, lean_object*);
lean_object* l_getModify___rarg___lambda__1(lean_object*, lean_object*);
uint64_t lean_uint64_of_nat(lean_object*);
lean_object* l_EStateM_Init_Prelude___instance__63___closed__6;
lean_object* l_String_utf8ByteSize_match__1(lean_object*);
lean_object* l_Lean_Name_Init_Prelude___instance__70;
@ -90,7 +91,8 @@ lean_object* l_Lean_Macro_Init_Prelude___instance__80___lambda__1___boxed(lean_o
lean_object* l_Lean_Syntax_getKind_match__1(lean_object*);
lean_object* l_ReaderT_Init_Prelude___instance__49___closed__1;
lean_object* l_Init_Prelude___instance__6(lean_object*, lean_object*);
lean_object* l_Init_Prelude___instance__32___closed__1;
lean_object* l_UInt64_size___closed__1;
uint64_t l_Init_Prelude___instance__32___closed__1;
lean_object* l_ReaderT_map___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_Init_Prelude___instance__51___rarg___lambda__8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_withRef___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -108,6 +110,7 @@ lean_object* l_Lean_Macro_Init_Prelude___instance__79___closed__4;
lean_object* l_Lean_Macro_Init_Prelude___instance__80___closed__1;
lean_object* l_List_foldl___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_EStateM_run(lean_object*, lean_object*, lean_object*);
lean_object* l_UInt8_size;
lean_object* l_EStateM_Init_Prelude___instance__63___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getKind_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Init_Prelude___instance__44___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -155,6 +158,7 @@ lean_object* l_Lean_addMacroScope_match__2___rarg___boxed(lean_object*, lean_obj
lean_object* l_Lean_Init_Prelude___instance__72;
lean_object* l_Init_Prelude___instance__8(lean_object*);
lean_object* l_Lean_Macro_withFreshMacroScope(lean_object*);
lean_object* l_USize_size___closed__1;
lean_object* l_Init_Prelude___instance__16;
lean_object* l_ReaderT_lift___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Init_Prelude___instance__54___rarg(lean_object*, lean_object*);
@ -185,7 +189,6 @@ lean_object* l_Applicative_seqRight___default___rarg___closed__1;
lean_object* l_cond_match__1___rarg(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_readThe___rarg___boxed(lean_object*);
lean_object* l_Lean_Macro_Context_currRecDepth___default;
lean_object* l_uint64Sz___closed__1;
lean_object* l_Applicative_seqRight___default(lean_object*);
lean_object* l_Init_Prelude___instance__38(lean_object*);
lean_object* l_EStateM_adaptExcept(lean_object*, lean_object*, lean_object*, lean_object*);
@ -193,15 +196,15 @@ lean_object* lean_string_utf8_byte_size(lean_object*);
lean_object* l_cond___rarg(uint8_t, lean_object*, lean_object*);
lean_object* l_List_hasDecEq_match__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_adapt___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_UInt8_ofNatCore___boxed(lean_object*, lean_object*);
lean_object* l_False_elim(lean_object*, uint8_t);
lean_object* l_Init_Prelude___instance__43___rarg___boxed(lean_object*);
lean_object* l_cond_match__1(lean_object*, lean_object*);
lean_object* l_Init_Prelude___instance__34;
size_t l_Init_Prelude___instance__34;
lean_object* l_EStateM_dummySave___boxed(lean_object*, lean_object*);
lean_object* l_Lean_nameLitKind;
lean_object* l_cond(lean_object*);
lean_object* l_EStateM_dummyRestore(lean_object*);
lean_object* l_uint64Sz;
lean_object* l_Applicative_map___default___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Init_Prelude___instance__74;
uint8_t l_Init_Prelude___instance__33(size_t, size_t);
@ -245,7 +248,7 @@ lean_object* l_Lean_addMacroScope_match__1(lean_object*);
lean_object* l_EStateM_Init_Prelude___instance__65(lean_object*, lean_object*);
lean_object* l_getThe___rarg(lean_object*);
lean_object* l___private_Init_Prelude_0__Lean_extractMacroScopesAux(lean_object*, lean_object*);
lean_object* l_Init_Prelude___instance__24;
uint16_t l_Init_Prelude___instance__24;
uint8_t l_Lean_Name_hasMacroScopes(lean_object*);
lean_object* l_Init_Prelude___instance__48___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Init_Prelude___instance__59___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
@ -319,7 +322,6 @@ lean_object* l_Init_Prelude___instance__18_match__1___boxed(lean_object*, lean_o
uint32_t l_Char_utf8Size___closed__2;
lean_object* l_Lean_replaceRef_match__1(lean_object*);
lean_object* l_EStateM_Init_Prelude___instance__63___closed__3;
lean_object* l_uint16Sz;
lean_object* l_Init_Prelude___instance__12___closed__1;
lean_object* l_modify(lean_object*, lean_object*);
lean_object* l_Lean_Init_Prelude___instance__69___closed__1;
@ -333,7 +335,7 @@ lean_object* l_Init_Prelude___instance__45___rarg(lean_object*);
lean_object* l_Lean_firstFrontendMacroScope___closed__1;
lean_object* l_Lean_replaceRef(lean_object*, lean_object*);
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
lean_object* l_Init_Prelude___instance__24___closed__1;
uint16_t l_Init_Prelude___instance__24___closed__1;
uint8_t l_UInt32_decLt(uint32_t, uint32_t);
lean_object* l_Lean_numLitKind___closed__1;
lean_object* l_List_hasDecEq_match__2___rarg___boxed(lean_object*, lean_object*, lean_object*);
@ -377,7 +379,7 @@ lean_object* l_ReaderT_bind(lean_object*, lean_object*);
lean_object* l_Init_Prelude___instance__35___boxed(lean_object*, lean_object*);
lean_object* l_Init_Prelude___instance__11;
lean_object* l_EStateM_modifyGet(lean_object*, lean_object*, lean_object*);
lean_object* l_Init_Prelude___instance__22___closed__1;
uint8_t l_Init_Prelude___instance__22___closed__1;
lean_object* l_Array_mkEmpty___boxed(lean_object*, lean_object*);
lean_object* l_EStateM_nonBacktrackable___closed__1;
lean_object* l_Lean_choiceKind;
@ -391,7 +393,7 @@ lean_object* l_Init_Prelude___instance__2(lean_object*, lean_object*);
lean_object* l_Lean_Macro_Init_Prelude___instance__80___closed__4;
lean_object* l_Init_Prelude___instance__11___closed__1;
size_t lean_usize_of_nat(lean_object*);
lean_object* l_Init_Prelude___instance__26___closed__1;
uint32_t l_Init_Prelude___instance__26___closed__1;
lean_object* l_ReaderT_Init_Prelude___instance__50___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_read___rarg(lean_object*, lean_object*);
lean_object* l_inferInstance___rarg___boxed(lean_object*);
@ -413,6 +415,7 @@ lean_object* l_EStateM_nonBacktrackable___closed__2;
lean_object* l_Lean_Macro_withIncRecDepth_match__1___rarg(uint8_t, lean_object*, lean_object*);
lean_object* l_Init_Prelude___instance__13;
lean_object* l_ReaderT_Init_Prelude___instance__51___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_UInt16_size;
lean_object* l_Lean_Syntax_getHeadInfo_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_UInt32_ofNatCore___boxed(lean_object*, lean_object*);
lean_object* l_decEq(lean_object*);
@ -454,6 +457,7 @@ uint8_t l_or(uint8_t, uint8_t);
lean_object* l_Monad_map___default(lean_object*);
lean_object* l_ReaderT_bind___at_Lean_Macro_Init_Prelude___instance__79___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_add___boxed(lean_object*, lean_object*);
lean_object* l_UInt64_ofNatCore___boxed(lean_object*, lean_object*);
lean_object* l_Lean_nullKind___closed__1;
lean_object* l_Lean_SourceInfo_pos___default;
lean_object* l_Init_Prelude___instance__57___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -470,7 +474,6 @@ lean_object* l_ReaderT_Init_Prelude___instance__49(lean_object*, lean_object*);
lean_object* l_Nat_decEq_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getArgs_match__1(lean_object*);
lean_object* l_Lean_SourceInfo_leading___default;
lean_object* l_uint8Sz;
lean_object* l_UInt16_decEq___boxed(lean_object*, lean_object*);
lean_object* l_typedExpr___rarg(lean_object*);
lean_object* l_Init_Prelude___instance__15;
@ -486,7 +489,7 @@ lean_object* l_Init_Prelude___instance__55___rarg(lean_object*);
lean_object* l_Lean_replaceRef___boxed(lean_object*, lean_object*);
lean_object* l_Lean_extractMacroScopes_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_read(lean_object*, lean_object*);
lean_object* l_Init_Prelude___instance__34___closed__1;
size_t l_Init_Prelude___instance__34___closed__1;
lean_object* l_Lean_Syntax_getHeadInfo_loop(lean_object*, lean_object*);
lean_object* l_Eq_ndrec___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_and___boxed(lean_object*, lean_object*);
@ -509,7 +512,7 @@ uint8_t l_UInt32_decEq(uint32_t, uint32_t);
lean_object* l___private_Init_Prelude_0__Lean_extractMainModule_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_EStateM_nonBacktrackable___closed__3;
lean_object* l___private_Init_Prelude_0__Lean_eraseMacroScopesAux(lean_object*);
lean_object* l_Init_Prelude___instance__26;
uint32_t l_Init_Prelude___instance__26;
lean_object* l_Init_Prelude___instance__27;
lean_object* l_Lean_Syntax_setKind_match__1(lean_object*);
lean_object* l_Init_Prelude___instance__12;
@ -531,7 +534,7 @@ lean_object* l_Init_Prelude___instance__7(lean_object*, lean_object*);
lean_object* l_Monad_seqRight___default___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_mk(lean_object*, lean_object*);
lean_object* l___private_Init_Prelude_0__Lean_eraseMacroScopesAux_match__2(lean_object*);
lean_object* l_Init_Prelude___instance__22;
uint8_t l_Init_Prelude___instance__22;
lean_object* l_tryCatchThe(lean_object*, lean_object*);
lean_object* l_String_bsize(lean_object*);
lean_object* l_Init_Prelude___instance__39___boxed(lean_object*, lean_object*);
@ -546,7 +549,6 @@ lean_object* l_Lean_Macro_withIncRecDepth(lean_object*);
lean_object* l_Lean_Name_append_match__1(lean_object*);
lean_object* l_and_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Macro_withIncRecDepth_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_usizeSz___closed__1;
lean_object* l_ReaderT_Init_Prelude___instance__50___rarg(lean_object*);
lean_object* l___private_Init_Prelude_0__Char_ofNatAux___boxed(lean_object*, lean_object*);
lean_object* l_EStateM_adaptExcept___rarg(lean_object*, lean_object*, lean_object*);
@ -607,7 +609,6 @@ lean_object* l_Init_Prelude___instance__35_match__1___boxed(lean_object*, lean_o
lean_object* lean_nat_mul(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getPos(lean_object*);
lean_object* l_throwThe___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_uint32Sz;
lean_object* l_UInt32_decEq___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Name_append_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_cast(lean_object*, lean_object*, lean_object*);
@ -618,12 +619,14 @@ lean_object* l_EStateM_set___rarg(lean_object*, lean_object*);
lean_object* l_List_foldl___at_Lean_MacroScopesView_review___spec__1(lean_object*, lean_object*);
lean_object* l_ReaderT_pure___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Decidable_decide___rarg___boxed(lean_object*);
lean_object* l_USize_size;
lean_object* l_Lean_Name_hasMacroScopes_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_EStateM_orElse(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_cond___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Macro_Init_Prelude___instance__80___lambda__2(lean_object*, lean_object*);
lean_object* l_getModify___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
lean_object* l_Char_ofNat___closed__1;
lean_object* l_Function_const(lean_object*, lean_object*);
lean_object* l_Lean_Init_Prelude___instance__74___closed__2;
lean_object* l_ReaderT_map(lean_object*, lean_object*);
@ -636,6 +639,7 @@ lean_object* l_ReaderT_Init_Prelude___instance__51___rarg___lambda__6(lean_objec
lean_object* l_EStateM_Init_Prelude___instance__63___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_hasDecEq_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_getOp___rarg(lean_object*, lean_object*, lean_object*);
uint8_t lean_uint8_of_nat(lean_object*);
lean_object* l_Fin_decLe___rarg___boxed(lean_object*, lean_object*);
lean_object* l_modifyGetThe(lean_object*, lean_object*, lean_object*);
lean_object* l_cond_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -643,12 +647,14 @@ lean_object* l_List_hasDecEq_match__3(lean_object*, lean_object*);
lean_object* l_Lean_Init_Prelude___instance__73;
lean_object* l___private_Init_Prelude_0__Lean_eraseMacroScopesAux___boxed(lean_object*);
lean_object* l_Init_Prelude___instance__55(lean_object*, lean_object*);
lean_object* l_UInt16_ofNatCore___boxed(lean_object*, lean_object*);
lean_object* l_Init_Prelude___instance__6_match__1(lean_object*, lean_object*);
lean_object* l_Lean_Macro_Init_Prelude___instance__79___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* lean_array_data(lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
lean_object* l_Init_Prelude___instance__29___boxed(lean_object*, lean_object*);
size_t lean_usize_mix_hash(size_t, size_t);
lean_object* l_UInt32_size;
lean_object* l_List_hasDecEq_match__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_USize_ofNatCore___boxed(lean_object*, lean_object*);
lean_object* l_MonadExcept_orelse(lean_object*, lean_object*);
@ -675,7 +681,6 @@ lean_object* l_Init_Prelude___instance__8_match__1(lean_object*, lean_object*);
lean_object* l_or_match__1(lean_object*);
lean_object* l_id(lean_object*);
lean_object* l_Init_Prelude___instance__41(lean_object*, lean_object*);
lean_object* l_usizeSz;
lean_object* l___private_Init_Prelude_0__Lean_assembleParts___closed__1;
lean_object* l_Lean_Syntax_getOp___boxed(lean_object*, lean_object*);
lean_object* l_Init_Prelude___instance__59(lean_object*, lean_object*);
@ -708,6 +713,7 @@ lean_object* l___private_Init_Prelude_0__Lean_eraseMacroScopesAux_match__1___rar
lean_object* l_ReaderT_Init_Prelude___instance__51___rarg___lambda__7(lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_pure(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getHeadInfo_loop___boxed(lean_object*, lean_object*);
uint16_t lean_uint16_of_nat(lean_object*);
lean_object* l_Array_sz___boxed(lean_object*, lean_object*);
lean_object* l_ReaderT_lift___rarg(lean_object*, lean_object*);
lean_object* l_ReaderT_Init_Prelude___instance__51(lean_object*, lean_object*);
@ -722,6 +728,7 @@ lean_object* l_Monad_seq___default___rarg___lambda__1(lean_object*, lean_object*
lean_object* l_Init_Prelude___instance__42___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_Init_Prelude___instance__71___closed__1;
lean_object* l_Array_mkEmpty_match__1___rarg(lean_object*, lean_object*);
lean_object* l_UInt64_size;
lean_object* l_EStateM_Init_Prelude___instance__65___closed__2;
lean_object* l_EStateM_Init_Prelude___instance__66___rarg(lean_object*);
lean_object* l_Init_Prelude___instance__37(lean_object*);
@ -2412,7 +2419,7 @@ lean_dec(x_1);
return x_2;
}
}
static lean_object* _init_l_uint8Sz() {
static lean_object* _init_l_UInt8_size() {
_start:
{
lean_object* x_1;
@ -2420,6 +2427,16 @@ x_1 = lean_unsigned_to_nat(256u);
return x_1;
}
}
lean_object* l_UInt8_ofNatCore___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = lean_uint8_of_nat(x_1);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
}
}
lean_object* l_UInt8_decEq___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -2454,25 +2471,24 @@ x_6 = lean_box(x_5);
return x_6;
}
}
static lean_object* _init_l_Init_Prelude___instance__22___closed__1() {
static uint8_t _init_l_Init_Prelude___instance__22___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
lean_object* x_1; uint8_t x_2;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
x_2 = lean_uint8_of_nat(x_1);
return x_2;
}
}
static lean_object* _init_l_Init_Prelude___instance__22() {
static uint8_t _init_l_Init_Prelude___instance__22() {
_start:
{
lean_object* x_1;
uint8_t x_1;
x_1 = l_Init_Prelude___instance__22___closed__1;
return x_1;
}
}
static lean_object* _init_l_uint16Sz() {
static lean_object* _init_l_UInt16_size() {
_start:
{
lean_object* x_1;
@ -2480,6 +2496,16 @@ x_1 = lean_unsigned_to_nat(65536u);
return x_1;
}
}
lean_object* l_UInt16_ofNatCore___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint16_t x_3; lean_object* x_4;
x_3 = lean_uint16_of_nat(x_1);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
}
}
lean_object* l_UInt16_decEq___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -2514,25 +2540,24 @@ x_6 = lean_box(x_5);
return x_6;
}
}
static lean_object* _init_l_Init_Prelude___instance__24___closed__1() {
static uint16_t _init_l_Init_Prelude___instance__24___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
lean_object* x_1; uint16_t x_2;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
x_2 = lean_uint16_of_nat(x_1);
return x_2;
}
}
static lean_object* _init_l_Init_Prelude___instance__24() {
static uint16_t _init_l_Init_Prelude___instance__24() {
_start:
{
lean_object* x_1;
uint16_t x_1;
x_1 = l_Init_Prelude___instance__24___closed__1;
return x_1;
}
}
static lean_object* _init_l_uint32Sz() {
static lean_object* _init_l_UInt32_size() {
_start:
{
lean_object* x_1;
@ -2540,6 +2565,16 @@ x_1 = lean_cstr_to_nat("4294967296");
return x_1;
}
}
lean_object* l_UInt32_ofNatCore___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint32_t x_3; lean_object* x_4;
x_3 = lean_uint32_of_nat(x_1);
lean_dec(x_1);
x_4 = lean_box_uint32(x_3);
return x_4;
}
}
lean_object* l_UInt32_toNat___boxed(lean_object* x_1) {
_start:
{
@ -2584,20 +2619,19 @@ x_6 = lean_box(x_5);
return x_6;
}
}
static lean_object* _init_l_Init_Prelude___instance__26___closed__1() {
static uint32_t _init_l_Init_Prelude___instance__26___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
lean_object* x_1; uint32_t x_2;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
x_2 = lean_uint32_of_nat(x_1);
return x_2;
}
}
static lean_object* _init_l_Init_Prelude___instance__26() {
static uint32_t _init_l_Init_Prelude___instance__26() {
_start:
{
lean_object* x_1;
uint32_t x_1;
x_1 = l_Init_Prelude___instance__26___closed__1;
return x_1;
}
@ -2686,17 +2720,7 @@ x_6 = lean_box(x_5);
return x_6;
}
}
lean_object* l_UInt32_ofNatCore___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint32_t x_3; lean_object* x_4;
x_3 = lean_uint32_of_nat(x_1);
lean_dec(x_1);
x_4 = lean_box_uint32(x_3);
return x_4;
}
}
static lean_object* _init_l_uint64Sz___closed__1() {
static lean_object* _init_l_UInt64_size___closed__1() {
_start:
{
lean_object* x_1;
@ -2704,14 +2728,24 @@ x_1 = lean_cstr_to_nat("18446744073709551616");
return x_1;
}
}
static lean_object* _init_l_uint64Sz() {
static lean_object* _init_l_UInt64_size() {
_start:
{
lean_object* x_1;
x_1 = l_uint64Sz___closed__1;
x_1 = l_UInt64_size___closed__1;
return x_1;
}
}
lean_object* l_UInt64_ofNatCore___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint64_t x_3; lean_object* x_4;
x_3 = lean_uint64_of_nat(x_1);
lean_dec(x_1);
x_4 = lean_box_uint64(x_3);
return x_4;
}
}
lean_object* l_UInt64_decEq___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -2746,25 +2780,24 @@ x_6 = lean_box(x_5);
return x_6;
}
}
static lean_object* _init_l_Init_Prelude___instance__32___closed__1() {
static uint64_t _init_l_Init_Prelude___instance__32___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
lean_object* x_1; uint64_t x_2;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
x_2 = lean_uint64_of_nat(x_1);
return x_2;
}
}
static lean_object* _init_l_Init_Prelude___instance__32() {
static uint64_t _init_l_Init_Prelude___instance__32() {
_start:
{
lean_object* x_1;
uint64_t x_1;
x_1 = l_Init_Prelude___instance__32___closed__1;
return x_1;
}
}
static lean_object* _init_l_usizeSz___closed__1() {
static lean_object* _init_l_USize_size___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -2774,14 +2807,24 @@ x_3 = lean_nat_pow(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_usizeSz() {
static lean_object* _init_l_USize_size() {
_start:
{
lean_object* x_1;
x_1 = l_usizeSz___closed__1;
x_1 = l_USize_size___closed__1;
return x_1;
}
}
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* l_USize_decEq___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -2816,20 +2859,19 @@ x_6 = lean_box(x_5);
return x_6;
}
}
static lean_object* _init_l_Init_Prelude___instance__34___closed__1() {
static size_t _init_l_Init_Prelude___instance__34___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
lean_object* x_1; size_t x_2;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
x_2 = lean_usize_of_nat(x_1);
return x_2;
}
}
static lean_object* _init_l_Init_Prelude___instance__34() {
static size_t _init_l_Init_Prelude___instance__34() {
_start:
{
lean_object* x_1;
size_t x_1;
x_1 = l_Init_Prelude___instance__34___closed__1;
return x_1;
}
@ -2844,16 +2886,6 @@ 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* l___private_Init_Prelude_0__Char_ofNatAux___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -2863,6 +2895,16 @@ x_4 = lean_box_uint32(x_3);
return x_4;
}
}
static lean_object* _init_l_Char_ofNat___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* l_Char_ofNat(lean_object* x_1) {
_start:
{
@ -2878,7 +2920,7 @@ if (x_5 == 0)
{
lean_object* x_6;
lean_dec(x_1);
x_6 = l_Init_Prelude___instance__26___closed__1;
x_6 = l_Char_ofNat___closed__1;
return x_6;
}
else
@ -2890,7 +2932,7 @@ if (x_8 == 0)
{
lean_object* x_9;
lean_dec(x_1);
x_9 = l_Init_Prelude___instance__26___closed__1;
x_9 = l_Char_ofNat___closed__1;
return x_9;
}
else
@ -6690,7 +6732,7 @@ _start:
{
size_t x_3; lean_object* x_4; uint8_t x_5;
x_3 = l_Lean_Name_hash(x_1);
x_4 = l_usizeSz;
x_4 = l_USize_size;
x_5 = lean_nat_dec_lt(x_2, x_4);
if (x_5 == 0)
{
@ -10446,44 +10488,36 @@ l_System_Platform_numBits___closed__1 = _init_l_System_Platform_numBits___closed
lean_mark_persistent(l_System_Platform_numBits___closed__1);
l_System_Platform_numBits = _init_l_System_Platform_numBits();
lean_mark_persistent(l_System_Platform_numBits);
l_uint8Sz = _init_l_uint8Sz();
lean_mark_persistent(l_uint8Sz);
l_UInt8_size = _init_l_UInt8_size();
lean_mark_persistent(l_UInt8_size);
l_Init_Prelude___instance__22___closed__1 = _init_l_Init_Prelude___instance__22___closed__1();
lean_mark_persistent(l_Init_Prelude___instance__22___closed__1);
l_Init_Prelude___instance__22 = _init_l_Init_Prelude___instance__22();
lean_mark_persistent(l_Init_Prelude___instance__22);
l_uint16Sz = _init_l_uint16Sz();
lean_mark_persistent(l_uint16Sz);
l_UInt16_size = _init_l_UInt16_size();
lean_mark_persistent(l_UInt16_size);
l_Init_Prelude___instance__24___closed__1 = _init_l_Init_Prelude___instance__24___closed__1();
lean_mark_persistent(l_Init_Prelude___instance__24___closed__1);
l_Init_Prelude___instance__24 = _init_l_Init_Prelude___instance__24();
lean_mark_persistent(l_Init_Prelude___instance__24);
l_uint32Sz = _init_l_uint32Sz();
lean_mark_persistent(l_uint32Sz);
l_UInt32_size = _init_l_UInt32_size();
lean_mark_persistent(l_UInt32_size);
l_Init_Prelude___instance__26___closed__1 = _init_l_Init_Prelude___instance__26___closed__1();
lean_mark_persistent(l_Init_Prelude___instance__26___closed__1);
l_Init_Prelude___instance__26 = _init_l_Init_Prelude___instance__26();
lean_mark_persistent(l_Init_Prelude___instance__26);
l_Init_Prelude___instance__27 = _init_l_Init_Prelude___instance__27();
lean_mark_persistent(l_Init_Prelude___instance__27);
l_Init_Prelude___instance__28 = _init_l_Init_Prelude___instance__28();
lean_mark_persistent(l_Init_Prelude___instance__28);
l_uint64Sz___closed__1 = _init_l_uint64Sz___closed__1();
lean_mark_persistent(l_uint64Sz___closed__1);
l_uint64Sz = _init_l_uint64Sz();
lean_mark_persistent(l_uint64Sz);
l_UInt64_size___closed__1 = _init_l_UInt64_size___closed__1();
lean_mark_persistent(l_UInt64_size___closed__1);
l_UInt64_size = _init_l_UInt64_size();
lean_mark_persistent(l_UInt64_size);
l_Init_Prelude___instance__32___closed__1 = _init_l_Init_Prelude___instance__32___closed__1();
lean_mark_persistent(l_Init_Prelude___instance__32___closed__1);
l_Init_Prelude___instance__32 = _init_l_Init_Prelude___instance__32();
lean_mark_persistent(l_Init_Prelude___instance__32);
l_usizeSz___closed__1 = _init_l_usizeSz___closed__1();
lean_mark_persistent(l_usizeSz___closed__1);
l_usizeSz = _init_l_usizeSz();
lean_mark_persistent(l_usizeSz);
l_USize_size___closed__1 = _init_l_USize_size___closed__1();
lean_mark_persistent(l_USize_size___closed__1);
l_USize_size = _init_l_USize_size();
lean_mark_persistent(l_USize_size);
l_Init_Prelude___instance__34___closed__1 = _init_l_Init_Prelude___instance__34___closed__1();
lean_mark_persistent(l_Init_Prelude___instance__34___closed__1);
l_Init_Prelude___instance__34 = _init_l_Init_Prelude___instance__34();
lean_mark_persistent(l_Init_Prelude___instance__34);
l_Char_ofNat___closed__1 = _init_l_Char_ofNat___closed__1();
lean_mark_persistent(l_Char_ofNat___closed__1);
l_Char_utf8Size___closed__1 = _init_l_Char_utf8Size___closed__1();
l_Char_utf8Size___closed__2 = _init_l_Char_utf8Size___closed__2();
l_Char_utf8Size___closed__3 = _init_l_Char_utf8Size___closed__3();

8
stage0/stdlib/Lean/Compiler/ConstFolding.c generated
View file

@ -42,6 +42,7 @@ lean_object* l_Lean_Compiler_NumScalarTypeInfo_size___default___boxed(lean_objec
lean_object* l_Lean_Compiler_foldCharOfNat___closed__1;
lean_object* l_Lean_Compiler_foldUIntSub___lambda__1(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Compiler_natFoldFns___closed__15;
extern lean_object* l_UInt64_size___closed__1;
lean_object* l_Lean_Compiler_foldCharOfNat___closed__2;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_874____closed__6;
lean_object* l_Lean_Compiler_NumScalarTypeInfo_ofNatFn___default(lean_object*);
@ -70,6 +71,7 @@ lean_object* l_Lean_Compiler_natFoldFns___closed__19;
lean_object* l_Lean_Compiler_foldNatDecLe___closed__2;
lean_object* l_Lean_Compiler_preUIntBinFoldFns___closed__9;
lean_object* l_Lean_Compiler_foldUIntSub___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_USize_size___closed__1;
lean_object* l_Lean_Compiler_NumScalarTypeInfo_size___default(lean_object*);
lean_object* l_Lean_Compiler_foldUIntSub___closed__1;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_1547____closed__7;
@ -89,7 +91,6 @@ lean_object* l_Lean_Compiler_foldUIntAdd___lambda__1___boxed(lean_object*, lean_
lean_object* l_Lean_Compiler_numScalarTypes___closed__1;
lean_object* l_Lean_Compiler_natFoldFns___closed__31;
lean_object* l_Lean_Compiler_foldNatMul___boxed(lean_object*);
extern lean_object* l_uint64Sz___closed__1;
lean_object* l_Lean_Compiler_binFoldFns___closed__2;
lean_object* l_Lean_Compiler_NumScalarTypeInfo_toNatFn___default___closed__1;
lean_object* l_Lean_Compiler_uintFoldToNatFns;
@ -258,7 +259,6 @@ lean_object* l_Lean_Compiler_mkNatLt(lean_object*, lean_object*);
lean_object* l_Lean_mkApp(lean_object*, lean_object*);
lean_object* l_Lean_Compiler_mkUIntLit(lean_object*, lean_object*);
lean_object* l_List_map___at_Lean_Compiler_uintBinFoldFns___spec__1___boxed(lean_object*, lean_object*);
extern lean_object* l_usizeSz___closed__1;
lean_object* l_Lean_Compiler_foldBinUInt___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_append(lean_object*, lean_object*);
lean_object* l_Lean_Compiler_mkNatLe___closed__1;
@ -598,7 +598,7 @@ x_1 = lean_unsigned_to_nat(64u);
x_2 = l_Lean_Compiler_numScalarTypes___closed__13;
x_3 = l_Lean_Compiler_numScalarTypes___closed__14;
x_4 = l_Lean_Compiler_numScalarTypes___closed__15;
x_5 = l_uint64Sz___closed__1;
x_5 = l_UInt64_size___closed__1;
x_6 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_6, 0, x_1);
lean_ctor_set(x_6, 1, x_2);
@ -654,7 +654,7 @@ x_1 = l_System_Platform_numBits;
x_2 = l_Lean_Compiler_numScalarTypes___closed__18;
x_3 = l_Lean_Compiler_numScalarTypes___closed__19;
x_4 = l_Lean_Compiler_numScalarTypes___closed__20;
x_5 = l_usizeSz___closed__1;
x_5 = l_USize_size___closed__1;
x_6 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_6, 0, x_1);
lean_ctor_set(x_6, 1, x_2);

4
stage0/stdlib/Lean/Compiler/IR/EmitC.c generated
View file

@ -498,7 +498,6 @@ lean_object* l_Lean_IR_EmitC_emitApp(lean_object*, lean_object*, lean_object*, l
lean_object* l_List_forM___at_Lean_IR_EmitC_emitFnDecls___spec__3___closed__2;
lean_object* l_Nat_forM_loop___at_Lean_IR_EmitC_emitArgs___spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_foldM_loop___at_Lean_IR_EmitC_emitSimpleExternalCall___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_uint32Sz;
lean_object* l_Nat_foldM_loop___at_Lean_IR_EmitC_emitSimpleExternalCall___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_IR_EmitC_emitTag(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_EmitC_emitDecl(lean_object*, lean_object*, lean_object*);
@ -542,6 +541,7 @@ lean_object* l_Lean_IR_EmitC_emitSProj_match__1(lean_object*);
lean_object* l_Lean_IR_EmitC_emitFullApp_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_EmitC_emitFileHeader___closed__12;
extern lean_object* l___kind_term____x40_Init_Notation___hyg_2679____closed__2;
extern lean_object* l_UInt32_size;
lean_object* l_Nat_forM_loop___at_Lean_IR_EmitC_emitFnDeclAux___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_EmitC_getJPParams___closed__1;
lean_object* lean_ir_find_env_decl(lean_object*, lean_object*);
@ -9462,7 +9462,7 @@ return x_9;
else
{
lean_object* x_10; uint8_t x_11;
x_10 = l_uint32Sz;
x_10 = l_UInt32_size;
x_11 = lean_nat_dec_lt(x_2, x_10);
if (x_11 == 0)
{

10
stage0/stdlib/Lean/Data/Json/Parser.c generated
View file

@ -130,6 +130,7 @@ lean_object* lean_nat_mul(lean_object*, lean_object*);
lean_object* l_Lean_Lean_Data_Json_Parser___instance__1(lean_object*);
lean_object* l_Lean_Json_Parser_escapedChar___boxed__const__8;
lean_object* l_UInt32_decEq___boxed(lean_object*, lean_object*);
extern lean_object* l_USize_size;
lean_object* l_Lean_Quickparse_Lean_Data_Json_Parser___instance__2___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Quickparse_bind(lean_object*, lean_object*);
lean_object* l_Lean_Quickparse_Lean_Data_Json_Parser___instance__2___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*);
@ -149,7 +150,6 @@ lean_object* l_Lean_Json_Parser_num___lambda__3___closed__3;
extern lean_object* l_stdNext___closed__7;
lean_object* l_Lean_Json_Parser_num___lambda__6___boxed(lean_object*, lean_object*);
lean_object* lean_int_add(lean_object*, lean_object*);
extern lean_object* l_usizeSz;
lean_object* l_Lean_Json_Parser_natCore(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Quickparse_peek_x21(lean_object*);
lean_object* l_Lean_Json_parse_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -2974,7 +2974,7 @@ x_20 = lean_ctor_get(x_17, 0);
x_21 = lean_ctor_get(x_19, 0);
lean_inc(x_21);
lean_dec(x_19);
x_22 = l_usizeSz;
x_22 = l_USize_size;
x_23 = lean_nat_dec_lt(x_22, x_21);
if (x_23 == 0)
{
@ -3007,7 +3007,7 @@ lean_dec(x_17);
x_29 = lean_ctor_get(x_27, 0);
lean_inc(x_29);
lean_dec(x_27);
x_30 = l_usizeSz;
x_30 = l_USize_size;
x_31 = lean_nat_dec_lt(x_30, x_29);
if (x_31 == 0)
{
@ -3461,7 +3461,7 @@ lean_inc(x_33);
x_34 = lean_ctor_get(x_31, 1);
lean_inc(x_34);
lean_dec(x_31);
x_35 = l_usizeSz;
x_35 = l_USize_size;
x_36 = lean_nat_dec_lt(x_35, x_34);
if (x_36 == 0)
{
@ -3498,7 +3498,7 @@ lean_inc(x_42);
x_43 = lean_ctor_get(x_40, 1);
lean_inc(x_43);
lean_dec(x_40);
x_44 = l_usizeSz;
x_44 = l_USize_size;
x_45 = lean_nat_dec_lt(x_44, x_43);
if (x_45 == 0)
{

88
stage0/stdlib/Lean/Expr.c generated
View file

@ -35,7 +35,7 @@ lean_object* l_Lean_Expr_bindingDomain_x21___boxed(lean_object*);
uint8_t l_Lean_Expr_isCharLit(lean_object*);
lean_object* l_Lean_Expr_letName_x21(lean_object*);
uint8_t l_Lean_Expr_isNatLit(lean_object*);
extern lean_object* l_Init_Prelude___instance__32;
extern uint64_t l_Init_Prelude___instance__32;
lean_object* l_Lean_mkFreshMVarId___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Expr_updateFn_match__1(lean_object*);
lean_object* l_Lean_BinderInfo_isAuxDecl_match__1___rarg(uint8_t, lean_object*, lean_object*);
@ -80,7 +80,7 @@ lean_object* l_Lean_Expr_isLit___boxed(lean_object*);
lean_object* l_Lean_Expr_replaceFVars___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_updateLambda_x21___closed__3;
lean_object* l_Lean_Expr_getAppFn_match__1___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Init_Prelude___instance__32___closed__1;
extern uint64_t l_Init_Prelude___instance__32___closed__1;
uint64_t l_UInt64_add(uint64_t, uint64_t);
lean_object* l_Lean_Expr_constName_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_isStringLit_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -451,6 +451,7 @@ lean_object* l_Lean_mkFVar(lean_object*);
lean_object* l_Lean_Expr_getAutoParamTactic_x3f___closed__1;
uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
lean_object* l_Lean_ExprStructEq_Lean_Expr___instance__20___boxed(lean_object*);
lean_object* l_Lean_Expr_mkData___boxed__const__1;
lean_object* l_Lean_MData_empty;
size_t lean_usize_of_nat(lean_object*);
lean_object* l_Lean_mkSimpleThunkType(lean_object*);
@ -471,7 +472,7 @@ lean_object* l_Lean_Lean_Expr___instance__1;
lean_object* lean_expr_update_proj(lean_object*, lean_object*);
lean_object* l_Lean_Level_instantiateParams___at_Lean_Expr_instantiateLevelParamsArray___spec__3(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_looseBVarRange(lean_object*);
lean_object* l_Lean_Lean_Expr___instance__9;
uint64_t l_Lean_Lean_Expr___instance__9;
lean_object* l_Lean_Lean_Expr___instance__1___closed__1;
lean_object* l_Lean_Expr_bvarIdx_x21(lean_object*);
lean_object* l_Lean_Expr_updateProj_x21___closed__2;
@ -487,6 +488,7 @@ lean_object* l_Lean_Expr_updateLambda_x21___closed__1;
lean_object* l_Lean_mkAppN___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Expr_bindingInfo_x21_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_mvarId_x21_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_mkDataForLet___boxed__const__1;
lean_object* l_Lean_Expr_updateProj_x21___closed__1;
lean_object* l_Lean_Lean_Expr___instance__8___closed__1;
lean_object* lean_level_update_imax(lean_object*, lean_object*, lean_object*);
@ -528,6 +530,7 @@ lean_object* l_Lean_Expr_hasMVar___boxed(lean_object*);
lean_object* l_Lean_mkForall___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
lean_object* l_Lean_Expr_constLevels_x21___closed__2;
lean_object* l___private_Lean_Expr_0__Lean_Expr_mkDataCore___boxed__const__1;
lean_object* l_Lean_mkApp(lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppNumArgsAux___boxed(lean_object*, lean_object*);
size_t l_Lean_Literal_hash(lean_object*);
@ -547,6 +550,7 @@ lean_object* l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1;
lean_object* l_Lean_Expr_Data_looseBVarRange___boxed(lean_object*);
lean_object* l_Lean_mkAppRev(lean_object*, lean_object*);
lean_object* l_Lean_Expr_updateConst_x21_match__1(lean_object*);
lean_object* l_Lean_Expr_mkDataForBinder___boxed__const__1;
lean_object* l_Lean_Expr_bvarIdx_x21___closed__1;
lean_object* lean_panic_fn(lean_object*, lean_object*);
uint32_t l_USize_toUInt32(size_t);
@ -1832,10 +1836,10 @@ x_1 = lean_box(0);
return x_1;
}
}
static lean_object* _init_l_Lean_Lean_Expr___instance__9() {
static uint64_t _init_l_Lean_Lean_Expr___instance__9() {
_start:
{
lean_object* x_1;
uint64_t x_1;
x_1 = l_Init_Prelude___instance__32;
return x_1;
}
@ -2156,6 +2160,15 @@ x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_Expr_mkDataCore___boxed__const__1() {
_start:
{
uint64_t x_1; lean_object* x_2;
x_1 = l_Lean_Lean_Expr___instance__9;
x_2 = lean_box_uint64(x_1);
return x_2;
}
}
uint64_t l___private_Lean_Expr_0__Lean_Expr_mkDataCore(size_t x_1, lean_object* x_2, uint8_t x_3, uint8_t x_4, uint8_t x_5, uint8_t x_6, uint8_t x_7, uint8_t x_8) {
_start:
{
@ -2200,9 +2213,9 @@ return x_40;
else
{
lean_object* x_41; lean_object* x_42; lean_object* x_43; uint64_t x_44;
x_41 = l_Lean_Lean_Expr___instance__9;
x_42 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__4;
x_43 = lean_panic_fn(x_41, x_42);
x_41 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__4;
x_42 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___boxed__const__1;
x_43 = lean_panic_fn(x_42, x_41);
x_44 = lean_unbox_uint64(x_43);
lean_dec(x_43);
return x_44;
@ -2271,6 +2284,15 @@ x_3 = x_2 << x_1;
return x_3;
}
}
static lean_object* _init_l_Lean_Expr_mkData___boxed__const__1() {
_start:
{
uint64_t x_1; lean_object* x_2;
x_1 = l_Lean_Lean_Expr___instance__9;
x_2 = lean_box_uint64(x_1);
return x_2;
}
}
uint64_t l_Lean_Expr_mkData(size_t x_1, lean_object* x_2, uint8_t x_3, uint8_t x_4, uint8_t x_5, uint8_t x_6) {
_start:
{
@ -2311,9 +2333,9 @@ return x_34;
else
{
lean_object* x_35; lean_object* x_36; lean_object* x_37; uint64_t x_38;
x_35 = l_Lean_Lean_Expr___instance__9;
x_36 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__4;
x_37 = lean_panic_fn(x_35, x_36);
x_35 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__4;
x_36 = l_Lean_Expr_mkData___boxed__const__1;
x_37 = lean_panic_fn(x_36, x_35);
x_38 = lean_unbox_uint64(x_37);
lean_dec(x_37);
return x_38;
@ -2340,6 +2362,15 @@ x_13 = lean_box_uint64(x_12);
return x_13;
}
}
static lean_object* _init_l_Lean_Expr_mkDataForBinder___boxed__const__1() {
_start:
{
uint64_t x_1; lean_object* x_2;
x_1 = l_Lean_Lean_Expr___instance__9;
x_2 = lean_box_uint64(x_1);
return x_2;
}
}
uint64_t l_Lean_Expr_mkDataForBinder(size_t x_1, lean_object* x_2, uint8_t x_3, uint8_t x_4, uint8_t x_5, uint8_t x_6, uint8_t x_7) {
_start:
{
@ -2382,9 +2413,9 @@ return x_37;
else
{
lean_object* x_38; lean_object* x_39; lean_object* x_40; uint64_t x_41;
x_38 = l_Lean_Lean_Expr___instance__9;
x_39 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__4;
x_40 = lean_panic_fn(x_38, x_39);
x_38 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__4;
x_39 = l_Lean_Expr_mkDataForBinder___boxed__const__1;
x_40 = lean_panic_fn(x_39, x_38);
x_41 = lean_unbox_uint64(x_40);
lean_dec(x_40);
return x_41;
@ -2413,6 +2444,15 @@ x_15 = lean_box_uint64(x_14);
return x_15;
}
}
static lean_object* _init_l_Lean_Expr_mkDataForLet___boxed__const__1() {
_start:
{
uint64_t x_1; lean_object* x_2;
x_1 = l_Lean_Lean_Expr___instance__9;
x_2 = lean_box_uint64(x_1);
return x_2;
}
}
uint64_t l_Lean_Expr_mkDataForLet(size_t x_1, lean_object* x_2, uint8_t x_3, uint8_t x_4, uint8_t x_5, uint8_t x_6, uint8_t x_7) {
_start:
{
@ -2455,9 +2495,9 @@ return x_37;
else
{
lean_object* x_38; lean_object* x_39; lean_object* x_40; uint64_t x_41;
x_38 = l_Lean_Lean_Expr___instance__9;
x_39 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__4;
x_40 = lean_panic_fn(x_38, x_39);
x_38 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__4;
x_39 = l_Lean_Expr_mkDataForLet___boxed__const__1;
x_40 = lean_panic_fn(x_39, x_38);
x_41 = lean_unbox_uint64(x_40);
lean_dec(x_40);
return x_41;
@ -2489,13 +2529,12 @@ return x_15;
static lean_object* _init_l_Lean_Expr_Lean_Expr___instance__11___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; uint64_t x_4;
lean_object* x_1; uint64_t x_2; lean_object* x_3;
x_1 = l_Lean_levelZero;
x_2 = l_Init_Prelude___instance__32___closed__1;
x_3 = lean_alloc_ctor(3, 1, 8);
lean_ctor_set(x_3, 0, x_1);
x_4 = lean_unbox_uint64(x_2);
lean_ctor_set_uint64(x_3, sizeof(void*)*1, x_4);
lean_ctor_set_uint64(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
@ -15706,7 +15745,6 @@ lean_mark_persistent(l_Lean_Lean_Expr___instance__8);
l_Lean_MData_empty = _init_l_Lean_MData_empty();
lean_mark_persistent(l_Lean_MData_empty);
l_Lean_Lean_Expr___instance__9 = _init_l_Lean_Lean_Expr___instance__9();
lean_mark_persistent(l_Lean_Lean_Expr___instance__9);
l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1 = _init_l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1);
l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2 = _init_l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2();
@ -15715,10 +15753,18 @@ l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__3 = _init_l___private_Le
lean_mark_persistent(l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__3);
l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__4 = _init_l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__4();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__4);
l___private_Lean_Expr_0__Lean_Expr_mkDataCore___boxed__const__1 = _init_l___private_Lean_Expr_0__Lean_Expr_mkDataCore___boxed__const__1();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_Expr_mkDataCore___boxed__const__1);
l_Lean_Expr_mkData___closed__1 = _init_l_Lean_Expr_mkData___closed__1();
l_Lean_Expr_mkData___closed__2 = _init_l_Lean_Expr_mkData___closed__2();
l_Lean_Expr_mkData___closed__3 = _init_l_Lean_Expr_mkData___closed__3();
l_Lean_Expr_mkData___closed__4 = _init_l_Lean_Expr_mkData___closed__4();
l_Lean_Expr_mkData___boxed__const__1 = _init_l_Lean_Expr_mkData___boxed__const__1();
lean_mark_persistent(l_Lean_Expr_mkData___boxed__const__1);
l_Lean_Expr_mkDataForBinder___boxed__const__1 = _init_l_Lean_Expr_mkDataForBinder___boxed__const__1();
lean_mark_persistent(l_Lean_Expr_mkDataForBinder___boxed__const__1);
l_Lean_Expr_mkDataForLet___boxed__const__1 = _init_l_Lean_Expr_mkDataForLet___boxed__const__1();
lean_mark_persistent(l_Lean_Expr_mkDataForLet___boxed__const__1);
l_Lean_Expr_Lean_Expr___instance__11___closed__1 = _init_l_Lean_Expr_Lean_Expr___instance__11___closed__1();
lean_mark_persistent(l_Lean_Expr_Lean_Expr___instance__11___closed__1);
l_Lean_Expr_Lean_Expr___instance__11 = _init_l_Lean_Expr_Lean_Expr___instance__11();

27
stage0/stdlib/Lean/Level.c generated
View file

@ -26,7 +26,7 @@ lean_object* l_Array_qsort_sort___at_Lean_Level_normalize___spec__2___boxed(lean
lean_object* l_Lean_Level_isMax___boxed(lean_object*);
lean_object* l_Lean_Level_isSucc_match__1(lean_object*);
extern lean_object* l_Lean_Syntax_strLitToAtom___closed__3;
extern lean_object* l_Init_Prelude___instance__32;
extern uint64_t l_Init_Prelude___instance__32;
lean_object* l_Lean_Level_mvarId_x21___closed__2;
lean_object* l_Lean_Level_dec_match__1(lean_object*);
lean_object* l_Lean_Level_LevelToFormat_Result_format___closed__5;
@ -238,6 +238,7 @@ lean_object* l_Lean_Level_normalize(lean_object*);
uint64_t l_UInt64_shiftLeft(uint64_t, uint64_t);
lean_object* l_Lean_Level_mkNaryMax_match__1(lean_object*);
extern lean_object* l_Lean_Format_paren___closed__2;
lean_object* l_Lean_Level_mkData___boxed__const__1;
lean_object* l_Lean_Level_dec_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Level_updateSucc_x21___closed__2;
lean_object* l_Lean_Level_normLtAux_match__1(lean_object*);
@ -254,7 +255,7 @@ lean_object* l_Nat_imax(lean_object*, lean_object*);
lean_object* l_Lean_Level_depthEx___boxed(lean_object*);
lean_object* lean_level_update_succ(lean_object*, lean_object*);
lean_object* l_Lean_Level_getLevelOffset(lean_object*);
lean_object* l_Lean_Lean_Level___instance__1;
uint64_t l_Lean_Lean_Level___instance__1;
lean_object* l_Lean_Level_updateIMax_x21_match__1(lean_object*);
lean_object* l_Lean_fmt___at_Lean_Level_LevelToFormat_toResult___spec__1(lean_object*);
lean_object* l_Lean_Level_dec___boxed(lean_object*);
@ -351,10 +352,10 @@ lean_dec(x_1);
return x_3;
}
}
static lean_object* _init_l_Lean_Lean_Level___instance__1() {
static uint64_t _init_l_Lean_Lean_Level___instance__1() {
_start:
{
lean_object* x_1;
uint64_t x_1;
x_1 = l_Init_Prelude___instance__32;
return x_1;
}
@ -514,6 +515,15 @@ x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
}
}
static lean_object* _init_l_Lean_Level_mkData___boxed__const__1() {
_start:
{
uint64_t x_1; lean_object* x_2;
x_1 = l_Lean_Lean_Level___instance__1;
x_2 = lean_box_uint64(x_1);
return x_2;
}
}
uint64_t l_Lean_Level_mkData(size_t x_1, lean_object* x_2, uint8_t x_3, uint8_t x_4) {
_start:
{
@ -542,9 +552,9 @@ return x_20;
else
{
lean_object* x_21; lean_object* x_22; lean_object* x_23; uint64_t x_24;
x_21 = l_Lean_Lean_Level___instance__1;
x_22 = l_Lean_Level_mkData___closed__5;
x_23 = lean_panic_fn(x_21, x_22);
x_21 = l_Lean_Level_mkData___closed__5;
x_22 = l_Lean_Level_mkData___boxed__const__1;
x_23 = lean_panic_fn(x_22, x_21);
x_24 = lean_unbox_uint64(x_23);
lean_dec(x_23);
return x_24;
@ -6583,7 +6593,6 @@ res = initialize_Lean_Data_Format(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Lean_Level___instance__1 = _init_l_Lean_Lean_Level___instance__1();
lean_mark_persistent(l_Lean_Lean_Level___instance__1);
l_Lean_Level_mkData___closed__1 = _init_l_Lean_Level_mkData___closed__1();
lean_mark_persistent(l_Lean_Level_mkData___closed__1);
l_Lean_Level_mkData___closed__2 = _init_l_Lean_Level_mkData___closed__2();
@ -6594,6 +6603,8 @@ l_Lean_Level_mkData___closed__4 = _init_l_Lean_Level_mkData___closed__4();
lean_mark_persistent(l_Lean_Level_mkData___closed__4);
l_Lean_Level_mkData___closed__5 = _init_l_Lean_Level_mkData___closed__5();
lean_mark_persistent(l_Lean_Level_mkData___closed__5);
l_Lean_Level_mkData___boxed__const__1 = _init_l_Lean_Level_mkData___boxed__const__1();
lean_mark_persistent(l_Lean_Level_mkData___boxed__const__1);
l_Lean_Level_Lean_Level___instance__3___closed__1 = _init_l_Lean_Level_Lean_Level___instance__3___closed__1();
lean_mark_persistent(l_Lean_Level_Lean_Level___instance__3___closed__1);
l_Lean_Level_Lean_Level___instance__3 = _init_l_Lean_Level_Lean_Level___instance__3();

4
stage0/stdlib/Std/Data/PersistentArray.c generated
View file

@ -479,6 +479,7 @@ lean_object* l_Std_PersistentArray_stats___rarg(lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Array_toPersistentArray___spec__1___rarg(lean_object*, size_t, size_t, lean_object*);
lean_object* l_Std_PersistentArray_forMAux_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlMAux___at_Std_PersistentArray_toList___spec__3(lean_object*);
extern lean_object* l_USize_size;
lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlMAux___at_Std_PersistentArray_filter___spec__10(lean_object*);
lean_object* l_Array_findSomeRevM_x3f_find___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_anyMAux___rarg(lean_object*, lean_object*, lean_object*);
@ -536,7 +537,6 @@ lean_object* l_Std_PersistentArray_push(lean_object*);
lean_object* l_Std_PersistentArray_findSomeM_x3f___at_Std_PersistentArray_findSome_x3f___spec__1(lean_object*, lean_object*);
lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlFromMAux_match__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_findSomeMAux___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_usizeSz;
lean_object* l_Array_foldlMUnsafe_fold___at_Std_PersistentArray_foldl___spec__8___rarg(lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l_Std_PersistentArray_foldlM___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_modifyAux_match__1(lean_object*, lean_object*);
@ -2090,7 +2090,7 @@ static lean_object* _init_l_Std_PersistentArray_tooBig___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_usizeSz;
x_1 = l_USize_size;
x_2 = lean_unsigned_to_nat(8u);
x_3 = lean_nat_div(x_1, x_2);
return x_3;