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 2022-07-09 16:19:10 -07:00
parent aa52eebcdc
commit 63067b896a
25 changed files with 1796 additions and 1244 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
stage0/src/Init/Data/Array/Basic.lean generated
View file

@ -41,15 +41,15 @@ def singleton (v : α) : Array α :=
def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
a[i.toNat]
instance : GetElem (Array α) USize α fun xs i => LT.lt i.toNat xs.size where
getElem xs i h := xs.uget i h
def back [Inhabited α] (a : Array α) : α :=
a.get! (a.size - 1)
def get? (a : Array α) (i : Nat) : Option α :=
if h : i < a.size then some a[i] else none
abbrev getOp? (self : Array α) (idx : Nat) : Option α :=
self.get? idx
def back? (a : Array α) : Option α :=
a.get? (a.size - 1)

6
stage0/src/Init/Data/Array/Subarray.lean generated
View file

@ -29,9 +29,6 @@ def get (s : Subarray α) (i : Fin s.size) : α :=
exact Nat.add_lt_of_lt_sub this
s.as[s.start + i.val]
abbrev getOp (self : Subarray α) (idx : Fin self.size) : α :=
self.get idx
instance : GetElem (Subarray α) Nat α fun xs i => i < xs.size where
getElem xs i h := xs.get ⟨i, h⟩
@ -41,9 +38,6 @@ instance : GetElem (Subarray α) Nat α fun xs i => i < xs.size where
abbrev get! [Inhabited α] (s : Subarray α) (i : Nat) : α :=
getD s i default
abbrev getOp! [Inhabited α] (self : Subarray α) (idx : Nat) : α :=
self.get! idx
def popFront (s : Subarray α) : Subarray α :=
if h : s.start < s.stop then
{ s with start := s.start + 1, h₁ := Nat.le_of_lt_succ (Nat.add_lt_add_right h 1) }

5
stage0/src/Init/Data/ByteArray/Basic.lean generated
View file

@ -39,7 +39,7 @@ def size : (@& ByteArray) → Nat
@[extern "lean_byte_array_uget"]
def uget : (a : @& ByteArray) → (i : USize) → i.toNat < a.size → UInt8
| ⟨bs⟩, i, h => bs.uget i h
| ⟨bs⟩, i, h => bs[i]
@[extern "lean_byte_array_get"]
def get! : (@& ByteArray) → (@& Nat) → UInt8
@ -49,9 +49,6 @@ def get! : (@& ByteArray) → (@& Nat) → UInt8
def get : (a : @& ByteArray) → (@& Fin a.size) → UInt8
| ⟨bs⟩, i => bs.get i
@[inline] def getOp (self : ByteArray) (idx : Nat) : UInt8 :=
self.get! idx
instance : GetElem ByteArray Nat UInt8 fun xs i => LT.lt i xs.size where
getElem xs i h := xs.get ⟨i, h⟩

5
stage0/src/Init/Data/FloatArray/Basic.lean generated
View file

@ -39,7 +39,7 @@ def size : (@& FloatArray) → Nat
@[extern "lean_float_array_uget"]
def uget : (a : @& FloatArray) → (i : USize) → i.toNat < a.size → Float
| ⟨ds⟩, i, h => ds.uget i h
| ⟨ds⟩, i, h => ds[i]
@[extern "lean_float_array_fget"]
def get : (ds : @& FloatArray) → (@& Fin ds.size) → Float
@ -55,9 +55,6 @@ def get? (ds : FloatArray) (i : Nat) : Option Float :=
else
none
@[inline] def getOp (self : FloatArray) (idx : Nat) : Float :=
self.get! idx
instance : GetElem FloatArray Nat Float fun xs i => LT.lt i xs.size where
getElem xs i h := xs.get ⟨i, h⟩

6
stage0/src/Init/Data/String/Basic.lean generated
View file

@ -66,9 +66,6 @@ private def utf8GetAux? : List Char → Pos → Pos → Option Char
def get? : (@& String) → (@& Pos) → Option Char
| ⟨s⟩, p => utf8GetAux? s 0 p
abbrev getOp? (self : String) (idx : Pos) : Option Char :=
self.get? idx
/--
Similar to `get`, but produces a panic error message if `p` is not a valid `String.Pos`.
-/
@ -77,9 +74,6 @@ def get! (s : @& String) (p : @& Pos) : Char :=
match s with
| ⟨s⟩ => utf8GetAux s 0 p
abbrev getOp! (self : String) (idx : Pos) : Char :=
self.get! idx
private def utf8SetAux (c' : Char) : List Char → Pos → Pos → List Char
| [], _, _ => []
| c::cs, i, p =>

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

@ -1269,12 +1269,6 @@ def Array.get {α : Type u} (a : @& Array α) (i : @& Fin a.size) : α :=
def Array.get! {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
Array.getD a i default
abbrev Array.getOp {α : Type u} (self : Array α) (idx : Fin self.size) : α :=
self.get idx
abbrev Array.getOp! {α : Type u} [Inhabited α] (self : Array α) (idx : Nat) : α :=
self.get! idx
instance : GetElem (Array α) Nat α fun xs i => LT.lt i xs.size where
getElem xs i h := xs.get ⟨i, h⟩
@ -1917,10 +1911,6 @@ def getArg (stx : Syntax) (i : Nat) : Syntax :=
| Syntax.node _ _ args => args.getD i Syntax.missing
| _ => Syntax.missing
-- Add `stx[i]` as sugar for `stx.getArg i`
@[inline] def getOp (self : Syntax) (idx : Nat) : Syntax :=
self.getArg idx
instance : GetElem Syntax Nat Syntax fun _ _ => True where
getElem stx i _ := stx.getArg i

6
stage0/src/Lean/Elab/Term.lean generated
View file

@ -375,9 +375,9 @@ builtin_initialize termElabAttribute : KeyedDeclsAttribute TermElab ← mkTermEl
/--
Auxiliary datatatype for presenting a Lean lvalue modifier.
We represent a unelaborated lvalue as a `Syntax` (or `Expr`) and `List LVal`.
Example: `a.foo[i].1` is represented as the `Syntax` `a` and the list
`[LVal.fieldName "foo", LVal.getOp i, LVal.fieldIdx 1]`.
Recall that the notation `a[i]` is not just for accessing arrays in Lean. -/
Example: `a.foo.1` is represented as the `Syntax` `a` and the list
`[LVal.fieldName "foo", LVal.fieldIdx 1]`.
-/
inductive LVal where
| fieldIdx (ref : Syntax) (i : Nat)
/- Field `suffix?` is for producing better error messages because `x.y` may be a field access or a hierachical/composite name.

15
stage0/src/Std/Data/HashMap.lean generated
View file

@ -38,7 +38,7 @@ def mkIdx {n : Nat} (h : n > 0) (u : USize) : { u : USize // u.toNat < n } :=
@[inline] def reinsertAux (hashFn : α → UInt64) (data : HashMapBucket α β) (a : α) (b : β) : HashMapBucket α β :=
let ⟨i, h⟩ := mkIdx data.property (hashFn a |>.toUSize)
data.update i (AssocList.cons a b (data.val.uget i h)) h
data.update i (AssocList.cons a b data.val[i]) h
@[inline] def foldBucketsM {δ : Type w} {m : Type w → Type w} [Monad m] (data : HashMapBucket α β) (d : δ) (f : δ → α → β → m δ) : m δ :=
data.val.foldlM (init := d) fun d b => b.foldlM f d
@ -62,20 +62,20 @@ def findEntry? [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option (
match m with
| ⟨_, buckets⟩ =>
let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
(buckets.val.uget i h).findEntry? a
buckets.val[i].findEntry? a
set_option linter.unusedVariables false in
def find? [beq : BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option β :=
match m with
| ⟨_, buckets⟩ =>
let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
(buckets.val.uget i h).find? a
buckets.val[i].find? a
def contains [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Bool :=
match m with
| ⟨_, buckets⟩ =>
let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
(buckets.val.uget i h).contains a
buckets.val[i].contains a
def moveEntries [Hashable α] (i : Nat) (source : Array (AssocList α β)) (target : HashMapBucket α β) : HashMapBucket α β :=
if h : i < source.size then
@ -100,7 +100,7 @@ set_option linter.unusedVariables false in
match m with
| ⟨size, buckets⟩ =>
let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
let bkt := buckets.val.uget i h
let bkt := buckets.val[i]
if bkt.contains a then
(⟨size, buckets.update i (bkt.replace a b) h⟩, true)
else
@ -115,7 +115,7 @@ def erase [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : HashMapImp α
match m with
| ⟨ size, buckets ⟩ =>
let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
let bkt := buckets.val.uget i h
let bkt := buckets.val[i]
if bkt.contains a then ⟨size - 1, buckets.update i (bkt.erase a) h⟩
else m
@ -178,9 +178,6 @@ def insert' (m : HashMap α β) (a : α) (b : β) : HashMap α β × Bool :=
| some b => b
| none => panic! "key is not in the map"
@[inline] def getOp (self : HashMap α β) (idx : α) : Option β :=
self.find? idx
instance : GetElem (HashMap α β) α (Option β) fun _ _ => True where
getElem m k _ := m.find? k

10
stage0/src/Std/Data/HashSet.lean generated
View file

@ -32,7 +32,7 @@ def mkIdx {n : Nat} (h : n > 0) (u : USize) : { u : USize // u.toNat < n } :=
@[inline] def reinsertAux (hashFn : α → UInt64) (data : HashSetBucket α) (a : α) : HashSetBucket α :=
let ⟨i, h⟩ := mkIdx data.property (hashFn a |>.toUSize)
data.update i (a :: data.val.uget i h) h
data.update i (a :: data.val[i]) h
@[inline] def foldBucketsM {δ : Type w} {m : Type w → Type w} [Monad m] (data : HashSetBucket α) (d : δ) (f : δ → α → m δ) : m δ :=
data.val.foldlM (init := d) fun d as => as.foldlM f d
@ -50,13 +50,13 @@ def find? [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : Option α :=
match m with
| ⟨_, buckets⟩ =>
let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
(buckets.val.uget i h).find? (fun a' => a == a')
buckets.val[i].find? (fun a' => a == a')
def contains [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : Bool :=
match m with
| ⟨_, buckets⟩ =>
let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
(buckets.val.uget i h).contains a
buckets.val[i].contains a
def moveEntries [Hashable α] (i : Nat) (source : Array (List α)) (target : HashSetBucket α) : HashSetBucket α :=
if h : i < source.size then
@ -81,7 +81,7 @@ def insert [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α :
match m with
| ⟨size, buckets⟩ =>
let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
let bkt := buckets.val.uget i h
let bkt := buckets.val[i]
if bkt.contains a
then ⟨size, buckets.update i (bkt.replace a a) h⟩
else
@ -95,7 +95,7 @@ def erase [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α :=
match m with
| ⟨ size, buckets ⟩ =>
let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
let bkt := buckets.val.uget i h
let bkt := buckets.val[i]
if bkt.contains a then ⟨size - 1, buckets.update i (bkt.erase a) h⟩
else m

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

@ -63,9 +63,6 @@ def get! [Inhabited α] (t : PersistentArray α) (i : Nat) : α :=
else
getAux t.root (USize.ofNat i) t.shift
def getOp [Inhabited α] (self : PersistentArray α) (idx : Nat) : α :=
self.get! idx
-- TODO: remove [Inhabited α]
instance [Inhabited α] : GetElem (PersistentArray α) Nat α fun as i => i < as.size where
getElem xs i _ := xs.get! i

3
stage0/src/Std/Data/PersistentHashMap.lean generated
View file

@ -146,9 +146,6 @@ partial def findAux [BEq α] : Node α β → USize → α → Option β
def find? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → Option β
| { root := n, .. }, k => findAux n (hash k |>.toUSize) k
@[inline] def getOp {_ : BEq α} {_ : Hashable α} (self : PersistentHashMap α β) (idx : α) : Option β :=
self.find? idx
instance {_ : BEq α} {_ : Hashable α} : GetElem (PersistentHashMap α β) α (Option β) fun _ _ => True where
getElem m i _ := m.find? i

50
stage0/stdlib/Init/Data/Array/Basic.c generated
View file

@ -19,6 +19,7 @@ LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Array_concatMap___spec__
LEAN_EXPORT lean_object* l_Array_forM(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_findM_x3f(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_findSomeRevM_x3f_find___at_Array_findRevM_x3f___spec__1___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_instGetElemArrayUSizeLtNatInstLTNatToNatSize___closed__1;
LEAN_EXPORT lean_object* l_Array_takeWhile___rarg___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Array_getEvenElems___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_getMax_x3f___rarg(lean_object*, lean_object*);
@ -45,7 +46,6 @@ LEAN_EXPORT lean_object* l_Array_mkArray___boxed(lean_object*, lean_object*, lea
LEAN_EXPORT lean_object* l_Array_findSome_x3f___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Array_findSomeM_x3f___spec__1___rarg___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapIdxM(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_getOp_x3f(lean_object*);
static lean_object* l___aux__Init__Data__Array__Basic______macroRules__term_x23_x5b___x2c_x5d__1___closed__14;
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_allDiffAux___rarg___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_split(lean_object*);
@ -125,7 +125,6 @@ LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at_Array_contains___spec__1___rarg(
static lean_object* l_term_x23_x5b___x2c_x5d___closed__1;
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Array_findSome_x3f___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_anyM_loop___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_getOp_x3f___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_map___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Array_findIdxM_x3f___spec__1___rarg___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_findRev_x3f___rarg(lean_object*, lean_object*);
@ -184,6 +183,7 @@ LEAN_EXPORT lean_object* l_Array_mapIdx(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_getLit___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_toListLitAux___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forIn_loop___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_instGetElemArrayUSizeLtNatInstLTNatToNatSize(lean_object*);
LEAN_EXPORT lean_object* l_Array_getLit(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Array_isPrefixOf___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldrMUnsafe_fold___at_Array_foldr___spec__1(lean_object*, lean_object*);
@ -576,7 +576,6 @@ LEAN_EXPORT lean_object* l_Array_foldrMUnsafe_fold___at_Array_forRevM___spec__2_
LEAN_EXPORT lean_object* l_Array_any___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Array_findSomeM_x3f___spec__1___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldrMUnsafe_fold___at_Array_foldr___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_getOp_x3f___rarg___boxed(lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldr(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Array_filterMap___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -674,6 +673,23 @@ lean_dec(x_2);
return x_6;
}
}
static lean_object* _init_l_Array_instGetElemArrayUSizeLtNatInstLTNatToNatSize___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Array_uget___boxed), 4, 1);
lean_closure_set(x_1, 0, lean_box(0));
return x_1;
}
}
LEAN_EXPORT lean_object* l_Array_instGetElemArrayUSizeLtNatInstLTNatToNatSize(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Array_instGetElemArrayUSizeLtNatInstLTNatToNatSize___closed__1;
return x_2;
}
}
LEAN_EXPORT lean_object* l_Array_back___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -745,32 +761,6 @@ lean_dec(x_1);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Array_getOp_x3f___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Array_get_x3f___rarg(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Array_getOp_x3f(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Array_getOp_x3f___rarg___boxed), 2, 0);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Array_getOp_x3f___rarg___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Array_getOp_x3f___rarg(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Array_back_x3f___rarg(lean_object* x_1) {
_start:
{
@ -9771,6 +9761,8 @@ if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Array_instEmptyCollectionArray___closed__1 = _init_l_Array_instEmptyCollectionArray___closed__1();
lean_mark_persistent(l_Array_instEmptyCollectionArray___closed__1);
l_Array_instGetElemArrayUSizeLtNatInstLTNatToNatSize___closed__1 = _init_l_Array_instGetElemArrayUSizeLtNatInstLTNatToNatSize___closed__1();
lean_mark_persistent(l_Array_instGetElemArrayUSizeLtNatInstLTNatToNatSize___closed__1);
l_Array_swapAt_x21___rarg___closed__1 = _init_l_Array_swapAt_x21___rarg___closed__1();
lean_mark_persistent(l_Array_swapAt_x21___rarg___closed__1);
l_Array_swapAt_x21___rarg___closed__2 = _init_l_Array_swapAt_x21___rarg___closed__2();

71
stage0/stdlib/Init/Data/Array/Subarray.c generated
View file

@ -50,7 +50,6 @@ static lean_object* l_Array_term_____x5b___x3a___x5d___closed__1;
static lean_object* l_instReprSubarray___rarg___closed__12;
size_t lean_usize_sub(size_t, size_t);
static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a_x5d__1___closed__22;
LEAN_EXPORT lean_object* l_Subarray_getOp_x21___rarg___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Subarray_anyM___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldrMUnsafe_fold___at_Subarray_foldr___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a___x5d__1___closed__16;
@ -137,7 +136,6 @@ LEAN_EXPORT lean_object* l_Subarray_all(lean_object*);
static lean_object* l_instReprSubarray___rarg___closed__6;
LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Subarray_allM___spec__1___rarg___lambda__1(lean_object*, uint8_t);
LEAN_EXPORT lean_object* l_Subarray_foldr___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Subarray_getOp___rarg___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_ofSubarray(lean_object*);
static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a_x5d__1___closed__13;
static lean_object* l_Array_term_____x5b___x3a___x5d___closed__24;
@ -164,7 +162,6 @@ LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Subarray_all___spec__1(lean
LEAN_EXPORT lean_object* l_Subarray_foldrM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_term_____x5b___x3a___x5d___closed__7;
static lean_object* l_Array_term_____x5b_x3a___x5d___closed__1;
LEAN_EXPORT lean_object* l_Subarray_getOp(lean_object*);
static lean_object* l_Array_term_____x5b___x3a___x5d___closed__20;
static lean_object* l_instReprSubarray___rarg___closed__5;
LEAN_EXPORT lean_object* l_instAppendSubarray___rarg(lean_object*, lean_object*);
@ -188,7 +185,6 @@ LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Subarray_allM___spec__1___r
LEAN_EXPORT lean_object* l_Subarray_instForInSubarray(lean_object*, lean_object*, lean_object*);
static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a___x5d__1___closed__4;
static lean_object* l_Array_term_____x5b_x3a___x5d___closed__6;
LEAN_EXPORT lean_object* l_Subarray_getOp___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Subarray_forInUnsafe___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_instToStringSubarray___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldrMUnsafe_fold___at_Subarray_forRevM___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -202,7 +198,6 @@ static lean_object* l_instReprSubarray___rarg___closed__10;
LEAN_EXPORT lean_object* l_Subarray_forM___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_ofSubarray___rarg(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Subarray_getOp_x21___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l_instReprSubarray___rarg___closed__8;
LEAN_EXPORT uint8_t l_Subarray_all___rarg(lean_object*, lean_object*);
static lean_object* l_instReprSubarray___rarg___closed__4;
@ -236,7 +231,6 @@ static lean_object* l_instReprSubarray___rarg___closed__13;
static lean_object* l_Array_term_____x5b___x3a___x5d___closed__18;
static lean_object* l_Array_term_____x5b___x3a___x5d___closed__5;
static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a___x5d__1___closed__11;
LEAN_EXPORT lean_object* l_Subarray_getOp_x21(lean_object*);
LEAN_EXPORT lean_object* l_Subarray_size___rarg(lean_object*);
static lean_object* l_Array___aux__Init__Data__Array__Subarray______macroRules__Array__term_____x5b___x3a___x5d__1___closed__12;
LEAN_EXPORT lean_object* l_Subarray_allM(lean_object*, lean_object*);
@ -309,32 +303,6 @@ lean_dec(x_1);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Subarray_getOp___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Subarray_get___rarg(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Subarray_getOp(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Subarray_getOp___rarg___boxed), 2, 0);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Subarray_getOp___rarg___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Subarray_getOp___rarg(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Subarray_instGetElemSubarrayNatLtInstLTNatSize___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -439,45 +407,6 @@ lean_dec(x_1);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Subarray_getOp_x21___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; uint8_t x_5;
x_4 = l_Subarray_size___rarg(x_2);
x_5 = lean_nat_dec_lt(x_3, x_4);
lean_dec(x_4);
if (x_5 == 0)
{
lean_inc(x_1);
return x_1;
}
else
{
lean_object* x_6;
x_6 = l_Subarray_get___rarg(x_2, x_3);
return x_6;
}
}
}
LEAN_EXPORT lean_object* l_Subarray_getOp_x21(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Subarray_getOp_x21___rarg___boxed), 3, 0);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Subarray_getOp_x21___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Subarray_getOp_x21___rarg(x_1, x_2, x_3);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Subarray_popFront___rarg(lean_object* x_1) {
_start:
{

25
stage0/stdlib/Init/Data/ByteArray/Basic.c generated
View file

@ -52,7 +52,6 @@ LEAN_EXPORT lean_object* l_ByteArray_foldlMUnsafe_fold___rarg___lambda__1___boxe
LEAN_EXPORT lean_object* l_ByteArray_empty;
LEAN_EXPORT lean_object* l_ByteArray_foldlM_loop(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ByteArray_getOp___boxed(lean_object*, lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ByteArray_extract(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ByteArray_foldlMUnsafe___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -106,7 +105,6 @@ lean_object* lean_panic_fn(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ByteArray_isEmpty___boxed(lean_object*);
lean_object* lean_byte_array_fset(lean_object*, lean_object*, uint8_t);
LEAN_EXPORT lean_object* l_ByteArray_findIdx_x3f___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_ByteArray_getOp(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ByteArray_extract___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ByteArray_forInUnsafe_loop___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ByteArray_append(lean_object*, lean_object*);
@ -248,25 +246,6 @@ x_4 = lean_box(x_3);
return x_4;
}
}
LEAN_EXPORT uint8_t l_ByteArray_getOp(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3;
x_3 = lean_byte_array_get(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_ByteArray_getOp___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l_ByteArray_getOp(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
}
}
LEAN_EXPORT uint8_t l_ByteArray_instGetElemByteArrayNatUInt8LtInstLTNatSize(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -1408,7 +1387,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_ByteArray_toUInt64LE_x21___closed__4;
x_2 = l_ByteArray_toUInt64LE_x21___closed__5;
x_3 = lean_unsigned_to_nat(194u);
x_3 = lean_unsigned_to_nat(191u);
x_4 = lean_unsigned_to_nat(2u);
x_5 = l_ByteArray_toUInt64LE_x21___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -1499,7 +1478,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_ByteArray_toUInt64LE_x21___closed__4;
x_2 = l_ByteArray_toUInt64BE_x21___closed__1;
x_3 = lean_unsigned_to_nat(206u);
x_3 = lean_unsigned_to_nat(203u);
x_4 = lean_unsigned_to_nat(2u);
x_5 = l_ByteArray_toUInt64LE_x21___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

21
stage0/stdlib/Init/Data/FloatArray/Basic.c generated
View file

@ -88,7 +88,6 @@ LEAN_EXPORT lean_object* l_FloatArray_foldlMUnsafe_fold___rarg___lambda__1___box
lean_object* lean_mk_empty_float_array(lean_object*);
LEAN_EXPORT lean_object* l_FloatArray_forInUnsafe(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_FloatArray_foldlMUnsafe_fold___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_FloatArray_getOp___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_FloatArray_foldlMUnsafe___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_FloatArray_get_x3f___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_FloatArray_foldlMUnsafe_fold___at_FloatArray_foldl___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -96,7 +95,6 @@ LEAN_EXPORT lean_object* l_List_toStringAux___at_instToStringFloatArray___spec__
double lean_float_array_get(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_FloatArray_uset___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_float_array_fset(lean_object*, lean_object*, double);
LEAN_EXPORT double l_FloatArray_getOp(lean_object*, lean_object*);
double lean_float_array_uget(lean_object*, size_t);
static lean_object* l_List_toString___at_instToStringFloatArray___spec__1___closed__3;
LEAN_EXPORT lean_object* l_FloatArray_forInUnsafe_loop___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -252,25 +250,6 @@ lean_dec(x_1);
return x_3;
}
}
LEAN_EXPORT double l_FloatArray_getOp(lean_object* x_1, lean_object* x_2) {
_start:
{
double x_3;
x_3 = lean_float_array_get(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_FloatArray_getOp___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
double x_3; lean_object* x_4;
x_3 = l_FloatArray_getOp(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box_float(x_3);
return x_4;
}
}
LEAN_EXPORT double l_FloatArray_instGetElemFloatArrayNatFloatLtInstLTNatSize(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{

53
stage0/stdlib/Init/Data/String/Basic.c generated
View file

@ -53,7 +53,6 @@ LEAN_EXPORT uint8_t l_String_anyAux_loop(lean_object*, lean_object*, lean_object
LEAN_EXPORT lean_object* l_String_revPosOf(lean_object*, uint32_t);
LEAN_EXPORT lean_object* l_Substring_toString___boxed(lean_object*);
LEAN_EXPORT lean_object* l_String_offsetOfPosAux(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_getOp_x21___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_Pos_min(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_anyAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_modify(lean_object*, lean_object*, lean_object*);
@ -126,7 +125,6 @@ LEAN_EXPORT lean_object* l_Nat_repeat_loop___at_String_pushn___spec__1___boxed(l
LEAN_EXPORT lean_object* l_Substring_prevn(lean_object*, lean_object*, lean_object*);
uint8_t l_instDecidableNot___rarg(uint8_t);
LEAN_EXPORT uint8_t l_String_contains(lean_object*, uint32_t);
LEAN_EXPORT lean_object* l_String_getOp_x3f___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Substring_next(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_atEnd___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_Iterator_forward(lean_object*, lean_object*);
@ -149,7 +147,6 @@ LEAN_EXPORT lean_object* l_String_capitalize(lean_object*);
LEAN_EXPORT lean_object* l_Substring_nextn___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_Iterator_pos___boxed(lean_object*);
LEAN_EXPORT lean_object* l_String_isNat___lambda__1___boxed(lean_object*);
LEAN_EXPORT uint32_t l_String_getOp_x21(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_join(lean_object*);
LEAN_EXPORT lean_object* l_String_revPosOfAux(lean_object*, uint32_t, lean_object*);
LEAN_EXPORT lean_object* l_String_Iterator_nextn(lean_object*, lean_object*);
@ -187,11 +184,10 @@ LEAN_EXPORT lean_object* l_String_instSizeOfIterator___boxed(lean_object*);
LEAN_EXPORT lean_object* l_String_splitOn___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_Iterator_prevn(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_foldl(lean_object*);
LEAN_EXPORT uint8_t l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1703_(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1690_(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_foldr___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Substring_beq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_endsWith___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_getOp_x3f(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_Iterator_next(lean_object*);
LEAN_EXPORT lean_object* l_Substring_nextn(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Substring_front___boxed(lean_object*);
@ -292,9 +288,9 @@ LEAN_EXPORT lean_object* l_String_Pos_min___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_foldr(lean_object*);
LEAN_EXPORT lean_object* l_String_Iterator_setCurr___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Substring_posOf(lean_object*, uint32_t);
LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1690____boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_Iterator_remainingBytes(lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__Substring_takeWhileAux___at_String_nextUntil___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1703____boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Substring_toString(lean_object*);
LEAN_EXPORT lean_object* l_Substring_foldr___rarg___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_substrEq___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -529,24 +525,6 @@ lean_dec(x_1);
return x_3;
}
}
LEAN_EXPORT lean_object* l_String_getOp_x3f(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_string_utf8_get_opt(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_String_getOp_x3f___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_String_getOp_x3f(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
LEAN_EXPORT lean_object* l_String_get_x21___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -558,25 +536,6 @@ x_4 = lean_box_uint32(x_3);
return x_4;
}
}
LEAN_EXPORT uint32_t l_String_getOp_x21(lean_object* x_1, lean_object* x_2) {
_start:
{
uint32_t x_3;
x_3 = lean_string_utf8_get_bang(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_String_getOp_x21___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint32_t x_3; lean_object* x_4;
x_3 = l_String_getOp_x21(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box_uint32(x_3);
return x_4;
}
}
LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_utf8SetAux(uint32_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
@ -1818,7 +1777,7 @@ lean_dec(x_1);
return x_3;
}
}
LEAN_EXPORT uint8_t l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1703_(lean_object* x_1, lean_object* x_2) {
LEAN_EXPORT uint8_t l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1690_(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7;
@ -1841,11 +1800,11 @@ return x_9;
}
}
}
LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1703____boxed(lean_object* x_1, lean_object* x_2) {
LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1690____boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1703_(x_1, x_2);
x_3 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1690_(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
@ -1856,7 +1815,7 @@ LEAN_EXPORT uint8_t l_String_instDecidableEqIterator(lean_object* x_1, lean_obje
_start:
{
uint8_t x_3;
x_3 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1703_(x_1, x_2);
x_3 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1690_(x_1, x_2);
return x_3;
}
}

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

@ -224,7 +224,6 @@ static lean_object* l_Lean_Name_instAppendName___closed__1;
lean_object* lean_nat_add(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_get___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_and(uint8_t, uint8_t);
LEAN_EXPORT lean_object* l_Array_getOp_x21(lean_object*);
LEAN_EXPORT lean_object* l_monadFunctorRefl(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Prelude_0__Lean_extractMainModule(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ReaderT_instMonadReaderT(lean_object*, lean_object*);
@ -408,7 +407,6 @@ LEAN_EXPORT lean_object* l_Lean_Macro_throwErrorAt___rarg(lean_object*, lean_obj
LEAN_EXPORT lean_object* l_False_elim___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_instInhabitedList(lean_object*);
LEAN_EXPORT lean_object* l_instMonadWithReaderOf(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_getOp(lean_object*);
static lean_object* l_Lean_numLitKind___closed__2;
LEAN_EXPORT lean_object* l_Lean_Syntax_isMissing___boxed(lean_object*);
static lean_object* l_Lean_PrettyPrinter_instMonadQuotationUnexpandM___closed__2;
@ -435,7 +433,6 @@ LEAN_EXPORT lean_object* l_instMonadExcept___rarg(lean_object*);
LEAN_EXPORT lean_object* l_instHSubPos___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_instMonadStateOf___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_instHMod___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_getOp_x21___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_panic___at___private_Init_Prelude_0__Lean_assembleParts___spec__1(lean_object*);
LEAN_EXPORT lean_object* l_decEq___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_interpolatedStrKind___closed__2;
@ -513,7 +510,6 @@ static lean_object* l_Lean_nullKind___closed__2;
LEAN_EXPORT lean_object* l_Lean_Syntax_matchesIdent___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_MonadExcept_instOrElse(lean_object*, lean_object*);
static lean_object* l_EStateM_instMonadEStateM___closed__5;
LEAN_EXPORT lean_object* l_Array_getOp___rarg___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_data___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Macro_expandMacro_x3f(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_inferInstanceAs___rarg(lean_object*);
@ -681,7 +677,6 @@ static lean_object* l_Char_ofNat___closed__1;
LEAN_EXPORT lean_object* l_instHAddPosString(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Option_map___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_EStateM_instInhabitedEStateM___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_getOp_x21___rarg___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Function_const(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Char_ofNat___boxed(lean_object*);
LEAN_EXPORT lean_object* l_ReaderT_map(lean_object*, lean_object*);
@ -693,7 +688,6 @@ LEAN_EXPORT lean_object* l_EStateM_instInhabitedResult(lean_object*, lean_object
LEAN_EXPORT lean_object* l_instLEFin___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Option_map(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_instLENat;
LEAN_EXPORT lean_object* l_Array_getOp___rarg(lean_object*, lean_object*);
uint8_t lean_uint8_of_nat(lean_object*);
LEAN_EXPORT lean_object* l_Fin_decLe___rarg___boxed(lean_object*, lean_object*);
static lean_object* l_Lean_Macro_instMonadQuotationMacroM___closed__4;
@ -747,7 +741,6 @@ LEAN_EXPORT lean_object* l_ReaderT_bind___at_Lean_Macro_instMonadRefMacroM___spe
LEAN_EXPORT lean_object* l_id(lean_object*);
LEAN_EXPORT uint8_t l_instDecidableEqBool(uint8_t, uint8_t);
static lean_object* l___private_Init_Prelude_0__Lean_assembleParts___closed__1;
LEAN_EXPORT lean_object* l_Lean_Syntax_getOp___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Macro_instInhabitedMethods;
LEAN_EXPORT lean_object* l_Lean_Syntax_getOptional_x3f___boxed(lean_object*);
LEAN_EXPORT lean_object* l_instHOrElse___rarg(lean_object*, lean_object*, lean_object*);
@ -812,7 +805,6 @@ LEAN_EXPORT lean_object* l_Applicative_seqLeft___default___rarg(lean_object*, le
LEAN_EXPORT lean_object* l_Lean_MonadRef_mkInfoFromRefPos___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_TSyntaxArray_mkImpl(lean_object*);
static lean_object* l___private_Init_Prelude_0__Lean_eraseMacroScopesAux___closed__1;
LEAN_EXPORT lean_object* l_Lean_Syntax_getOp(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mk___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_instHAndThen___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_instDecidableLtPosInstLTPos___boxed(lean_object*, lean_object*);
@ -4122,58 +4114,6 @@ lean_dec(x_3);
return x_5;
}
}
LEAN_EXPORT lean_object* l_Array_getOp___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_array_fget(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Array_getOp(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Array_getOp___rarg___boxed), 2, 0);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Array_getOp___rarg___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Array_getOp___rarg(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Array_getOp_x21___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_array_get(x_1, x_2, x_3);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Array_getOp_x21(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Array_getOp_x21___rarg___boxed), 3, 0);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Array_getOp_x21___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Array_getOp_x21___rarg(x_1, x_2, x_3);
lean_dec(x_3);
lean_dec(x_2);
return x_4;
}
}
LEAN_EXPORT lean_object* l_instGetElemArrayNatLtInstLTNatSize___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -7846,24 +7786,6 @@ lean_dec(x_1);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Lean_Syntax_getOp(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_Syntax_getArg(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Lean_Syntax_getOp___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_Syntax_getOp(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Lean_Syntax_instGetElemSyntaxNatTrue(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{

26
stage0/stdlib/Lean/Data/Parsec.c generated
View file

@ -70,7 +70,7 @@ LEAN_EXPORT lean_object* l_Lean_Parsec_instMonadParsec;
LEAN_EXPORT lean_object* l_Lean_Parsec_pstring(lean_object*, lean_object*);
static lean_object* l_Lean_Parsec_instMonadParsec___closed__7;
LEAN_EXPORT lean_object* l_Lean_Parsec_instInhabitedParsec___rarg(lean_object*);
uint8_t l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1703_(lean_object*, lean_object*);
uint8_t l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1690_(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parsec_many1(lean_object*);
lean_object* l_String_Iterator_next(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parsec_peek_x21(lean_object*);
@ -1146,7 +1146,7 @@ if (x_9 == 0)
lean_object* x_10; lean_object* x_11; uint8_t x_12;
x_10 = lean_ctor_get(x_4, 0);
x_11 = lean_ctor_get(x_4, 1);
x_12 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1703_(x_3, x_10);
x_12 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1690_(x_3, x_10);
if (x_12 == 0)
{
lean_dec(x_3);
@ -1172,7 +1172,7 @@ x_16 = lean_ctor_get(x_4, 1);
lean_inc(x_16);
lean_inc(x_15);
lean_dec(x_4);
x_17 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1703_(x_3, x_15);
x_17 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1690_(x_3, x_15);
if (x_17 == 0)
{
lean_object* x_18;
@ -1317,7 +1317,7 @@ if (x_10 == 0)
lean_object* x_11; lean_object* x_12; uint8_t x_13;
x_11 = lean_ctor_get(x_5, 0);
x_12 = lean_ctor_get(x_5, 1);
x_13 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1703_(x_4, x_11);
x_13 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1690_(x_4, x_11);
if (x_13 == 0)
{
lean_dec(x_4);
@ -1343,7 +1343,7 @@ x_17 = lean_ctor_get(x_5, 1);
lean_inc(x_17);
lean_inc(x_16);
lean_dec(x_5);
x_18 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1703_(x_4, x_16);
x_18 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1690_(x_4, x_16);
if (x_18 == 0)
{
lean_object* x_19;
@ -1500,7 +1500,7 @@ if (x_14 == 0)
lean_object* x_15; lean_object* x_16; uint8_t x_17;
x_15 = lean_ctor_get(x_9, 0);
x_16 = lean_ctor_get(x_9, 1);
x_17 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1703_(x_3, x_15);
x_17 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1690_(x_3, x_15);
if (x_17 == 0)
{
lean_dec(x_3);
@ -1525,7 +1525,7 @@ x_19 = lean_ctor_get(x_9, 1);
lean_inc(x_19);
lean_inc(x_18);
lean_dec(x_9);
x_20 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1703_(x_3, x_18);
x_20 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1690_(x_3, x_18);
if (x_20 == 0)
{
lean_object* x_21;
@ -1559,7 +1559,7 @@ if (x_23 == 0)
lean_object* x_24; lean_object* x_25; uint8_t x_26;
x_24 = lean_ctor_get(x_4, 0);
x_25 = lean_ctor_get(x_4, 1);
x_26 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1703_(x_3, x_24);
x_26 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1690_(x_3, x_24);
if (x_26 == 0)
{
lean_dec(x_3);
@ -1584,7 +1584,7 @@ x_28 = lean_ctor_get(x_4, 1);
lean_inc(x_28);
lean_inc(x_27);
lean_dec(x_4);
x_29 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1703_(x_3, x_27);
x_29 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1690_(x_3, x_27);
if (x_29 == 0)
{
lean_object* x_30;
@ -1759,7 +1759,7 @@ if (x_14 == 0)
lean_object* x_15; lean_object* x_16; uint8_t x_17;
x_15 = lean_ctor_get(x_9, 0);
x_16 = lean_ctor_get(x_9, 1);
x_17 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1703_(x_3, x_15);
x_17 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1690_(x_3, x_15);
if (x_17 == 0)
{
lean_dec(x_3);
@ -1784,7 +1784,7 @@ x_19 = lean_ctor_get(x_9, 1);
lean_inc(x_19);
lean_inc(x_18);
lean_dec(x_9);
x_20 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1703_(x_3, x_18);
x_20 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1690_(x_3, x_18);
if (x_20 == 0)
{
lean_object* x_21;
@ -1818,7 +1818,7 @@ if (x_23 == 0)
lean_object* x_24; lean_object* x_25; uint8_t x_26;
x_24 = lean_ctor_get(x_4, 0);
x_25 = lean_ctor_get(x_4, 1);
x_26 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1703_(x_3, x_24);
x_26 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1690_(x_3, x_24);
if (x_26 == 0)
{
lean_dec(x_3);
@ -1843,7 +1843,7 @@ x_28 = lean_ctor_get(x_4, 1);
lean_inc(x_28);
lean_inc(x_27);
lean_dec(x_4);
x_29 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1703_(x_3, x_27);
x_29 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1690_(x_3, x_27);
if (x_29 == 0)
{
lean_object* x_30;

560
stage0/stdlib/Lean/Data/Xml/Parser.c generated
View file

File diff suppressed because it is too large Load diff

14
stage0/stdlib/Lean/Server/FileWorker/WidgetRequests.c generated
View file

@ -45,7 +45,6 @@ LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Wid
lean_object* lean_name_mk_string(lean_object*, lean_object*);
uint8_t lean_usize_dec_eq(size_t, size_t);
lean_object* lean_array_uget(lean_object*, size_t);
lean_object* l___private_Lean_Widget_InteractiveDiagnostic_0__Lean_Widget_toJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveDiagnostic___hyg_517____rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_io_error_to_string(lean_object*);
lean_object* l___private_Lean_Widget_InteractiveGoal_0__Lean_Widget_toJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveGoal___hyg_414____rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Widget_instInhabitedInfoPopup___closed__1;
@ -120,7 +119,6 @@ LEAN_EXPORT lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_Widg
LEAN_EXPORT lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1272_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_411_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1961____spec__3(lean_object*, lean_object*);
lean_object* l___private_Lean_Widget_TaggedText_0__Lean_Widget_toJsonTaggedText____x40_Lean_Widget_TaggedText___hyg_582____rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Widget_getInteractiveDiagnostics___spec__1(lean_object*, lean_object*, size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_instRpcEncodingInfoPopupRpcEncodingPacket___rarg___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_411____spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -128,6 +126,7 @@ LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_instRpcEncodingGetG
static lean_object* l_Lean_Server_registerBuiltinRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_411____spec__1___lambda__1___closed__1;
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Widget_getInteractiveDiagnostics___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_411____spec__2(lean_object*, lean_object*);
lean_object* l___private_Lean_Widget_InteractiveDiagnostic_0__Lean_Widget_toJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveDiagnostic___hyg_532____rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_instToJsonRpcEncodingPacket__7___rarg(lean_object*, lean_object*);
static lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_411____spec__2___closed__24;
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonLineRange____x40_Lean_Data_Lsp_Extra___hyg_1865_(lean_object*);
@ -183,6 +182,7 @@ static lean_object* l_Lean_Widget_instToJsonGetInteractiveDiagnosticsParams___cl
LEAN_EXPORT lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_toJsonRpcEncodingPacket____x40_Lean_Server_FileWorker_WidgetRequests___hyg_689____rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_instRpcEncodingInfoPopupRpcEncodingPacket___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_instRpcEncodingGetGoToLocationParamsRpcEncodingPacket___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Widget_TaggedText_0__Lean_Widget_toJsonTaggedText____x40_Lean_Widget_TaggedText___hyg_594____rarg(lean_object*, lean_object*);
lean_object* l_Lean_Widget_instRpcEncodingInteractiveGoalsRpcEncodingPacket___rarg(lean_object*);
lean_object* l_Lean_Server_instRpcEncoding___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_instRpcEncodingInfoPopupRpcEncodingPacket___rarg___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*);
@ -284,6 +284,7 @@ static lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x4
LEAN_EXPORT lean_object* l_Lean_Widget_instRpcEncodingMsgToInteractiveRpcEncodingPacket___rarg___lambda__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1234____spec__2___closed__2;
LEAN_EXPORT lean_object* l_Lean_Widget_instRpcEncodingGetGoToLocationParamsRpcEncodingPacket___rarg___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
lean_object* l___private_Lean_Widget_InteractiveDiagnostic_0__Lean_Widget_toJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveDiagnostic___hyg_1642____rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1961____lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonRpcEncodingPacket____x40_Lean_Server_FileWorker_WidgetRequests___hyg_569____rarg___closed__2;
lean_object* lean_io_initializing(lean_object*);
@ -316,7 +317,6 @@ LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_instRpcEncodingInfo
LEAN_EXPORT lean_object* l_Lean_Widget_instRpcEncodingGetGoToLocationParamsRpcEncodingPacket___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Info_lctx(lean_object*);
static lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1272____spec__2___closed__4;
lean_object* l___private_Lean_Widget_InteractiveDiagnostic_0__Lean_Widget_toJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveDiagnostic___hyg_1627____rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonRpcEncodingPacket____x40_Lean_Server_FileWorker_WidgetRequests___hyg_93____rarg___closed__1;
static lean_object* l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1253____spec__2___closed__3;
LEAN_EXPORT lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_toJsonRpcEncodingPacket____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1744____rarg(lean_object*, lean_object*, lean_object*);
@ -1010,7 +1010,7 @@ _start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_411____spec__2___closed__14;
x_2 = lean_alloc_closure((void*)(l___private_Lean_Widget_TaggedText_0__Lean_Widget_toJsonTaggedText____x40_Lean_Widget_TaggedText___hyg_582____rarg), 2, 1);
x_2 = lean_alloc_closure((void*)(l___private_Lean_Widget_TaggedText_0__Lean_Widget_toJsonTaggedText____x40_Lean_Widget_TaggedText___hyg_594____rarg), 2, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
@ -1134,7 +1134,7 @@ x_2 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_
x_3 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_411____spec__2___closed__26;
x_4 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_411____spec__2___closed__16;
x_5 = l_Lean_Lsp_instToJsonRpcRef;
x_6 = lean_alloc_closure((void*)(l___private_Lean_Widget_InteractiveDiagnostic_0__Lean_Widget_toJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveDiagnostic___hyg_517____rarg), 6, 5);
x_6 = lean_alloc_closure((void*)(l___private_Lean_Widget_InteractiveDiagnostic_0__Lean_Widget_toJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveDiagnostic___hyg_532____rarg), 6, 5);
lean_closure_set(x_6, 0, x_1);
lean_closure_set(x_6, 1, x_2);
lean_closure_set(x_6, 2, x_3);
@ -1148,7 +1148,7 @@ _start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_411____spec__2___closed__27;
x_2 = lean_alloc_closure((void*)(l___private_Lean_Widget_TaggedText_0__Lean_Widget_toJsonTaggedText____x40_Lean_Widget_TaggedText___hyg_582____rarg), 2, 1);
x_2 = lean_alloc_closure((void*)(l___private_Lean_Widget_TaggedText_0__Lean_Widget_toJsonTaggedText____x40_Lean_Widget_TaggedText___hyg_594____rarg), 2, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
@ -4369,7 +4369,7 @@ x_4 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_
x_5 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_411____spec__2___closed__28;
x_6 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1547____spec__2___closed__4;
x_7 = l_Lean_Server_wrapRpcProcedure___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1547____spec__2___closed__5;
x_8 = lean_alloc_closure((void*)(l___private_Lean_Widget_InteractiveDiagnostic_0__Lean_Widget_toJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveDiagnostic___hyg_1627____rarg), 8, 7);
x_8 = lean_alloc_closure((void*)(l___private_Lean_Widget_InteractiveDiagnostic_0__Lean_Widget_toJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveDiagnostic___hyg_1642____rarg), 8, 7);
lean_closure_set(x_8, 0, x_1);
lean_closure_set(x_8, 1, x_2);
lean_closure_set(x_8, 2, x_3);

849
stage0/stdlib/Lean/Widget/InteractiveDiagnostic.c generated
View file

File diff suppressed because it is too large Load diff

1142
stage0/stdlib/Lean/Widget/TaggedText.c generated
View file

File diff suppressed because it is too large Load diff

28
stage0/stdlib/Std/Data/HashMap.c generated
View file

@ -34,7 +34,6 @@ LEAN_EXPORT lean_object* l_Std_HashMapImp_reinsertAux(lean_object*, lean_object*
LEAN_EXPORT lean_object* l_Std_HashMap_find_x21(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashMap_toList(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashMap_contains___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashMap_getOp___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_AssocList_foldlM___at_Std_HashMapImp_foldBuckets___spec__1___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashMapImp_forBucketsM(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashMapImp_erase___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -65,7 +64,6 @@ LEAN_EXPORT lean_object* l_Std_AssocList_foldlM___at_Std_HashMapImp_fold___spec_
LEAN_EXPORT lean_object* l_Std_HashMap_numBuckets___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashMapImp_forBucketsM___spec__1___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashMap_instInhabitedHashMap___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashMap_getOp(lean_object*, lean_object*);
lean_object* l_Std_AssocList_erase___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashMapImp_reinsertAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashMapImp_contains(lean_object*, lean_object*);
@ -211,7 +209,6 @@ LEAN_EXPORT lean_object* l_Std_HashMap_foldM___rarg(lean_object*, lean_object*,
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashMap_toArray___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_AssocList_foldlM___at_Std_HashMap_toArray___spec__1___rarg___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashMapImp_forBucketsM___spec__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashMap_getOp___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashMapImp_findEntry_x3f(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashMapImp_forBucketsM___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashMapImp_forM___spec__1___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -2310,31 +2307,6 @@ lean_dec(x_4);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Std_HashMap_getOp___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_Std_HashMapImp_find_x3f___rarg(x_1, x_2, x_3, x_4);
return x_5;
}
}
LEAN_EXPORT lean_object* l_Std_HashMap_getOp(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Std_HashMap_getOp___rarg___boxed), 4, 0);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Std_HashMap_getOp___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_Std_HashMap_getOp___rarg(x_1, x_2, x_3, x_4);
lean_dec(x_3);
return x_5;
}
}
LEAN_EXPORT lean_object* l_Std_HashMap_instGetElemHashMapOptionTrue___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{

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

@ -83,7 +83,6 @@ LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_PersistentArray_toAr
LEAN_EXPORT lean_object* l_Std_PersistentArray_foldlM___at_Std_PersistentArray_toArray___spec__1___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldrMUnsafe_fold___at_Std_PersistentArray_foldr___spec__5(lean_object*, lean_object*);
lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentArray_getOp___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlFromMAux___at_Std_PersistentArray_append___spec__2___rarg(lean_object*, size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Array_findSomeRevM_x3f_find___at_Std_PersistentArray_findSomeRev_x3f___spec__4(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentArray_forMAux(lean_object*, lean_object*);
@ -122,7 +121,6 @@ LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_PersistentArray_appe
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_PersistentArray_collectStats___spec__1(lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentArray_append(lean_object*);
LEAN_EXPORT lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlMAux___at_Std_PersistentArray_filter___spec__3___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentArray_getOp(lean_object*);
LEAN_EXPORT lean_object* l_Array_findSomeRevM_x3f_find___at_Std_PersistentArray_findSomeRev_x3f___spec__5___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
@ -415,7 +413,6 @@ LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_PersistentArray_filt
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_PersistentArray_append___spec__8___rarg(lean_object*, size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlMAux___at_Std_PersistentArray_foldl___spec__10(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentArray_foldlM___at_Std_PersistentArray_append___spec__1(lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentArray_getOp___rarg___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentArray_findSomeRevM_x3f___at_Std_PersistentArray_findSomeRev_x3f___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_PersistentArray_toArray___spec__4___rarg(lean_object*, size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Std_PersistentArray_any___spec__5(lean_object*);
@ -1129,31 +1126,6 @@ lean_dec(x_3);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Std_PersistentArray_getOp___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Std_PersistentArray_get_x21___rarg(x_1, x_2, x_3);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Std_PersistentArray_getOp(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Std_PersistentArray_getOp___rarg___boxed), 3, 0);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Std_PersistentArray_getOp___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Std_PersistentArray_getOp___rarg(x_1, x_2, x_3);
lean_dec(x_3);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Std_PersistentArray_instGetElemPersistentArrayNatLtInstLTNatSize___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{

20
stage0/stdlib/Std/Data/PersistentHashMap.c generated
View file

@ -96,7 +96,6 @@ lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_PersistentHashMap_find_x21___rarg___closed__2;
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_instInhabitedEntry(lean_object*, lean_object*, lean_object*);
lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_getOp(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_findAux(lean_object*, lean_object*);
static lean_object* l_Std_PersistentHashMap_Stats_toString___closed__4;
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_isUnaryEntries(lean_object*, lean_object*);
@ -136,7 +135,6 @@ LEAN_EXPORT lean_object* l_Std_PersistentHashMap_findEntry_x3f___rarg(lean_objec
static lean_object* l_Std_PersistentHashMap_Stats_toString___closed__3;
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAux___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_PersistentHashMap_instInhabitedNode___closed__1;
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_getOp___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
static size_t l_Std_PersistentHashMap_insertAux___rarg___closed__1;
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_size___default;
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_containsAux___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -1428,22 +1426,6 @@ x_3 = lean_alloc_closure((void*)(l_Std_PersistentHashMap_find_x3f___rarg), 4, 0)
return x_3;
}
}
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_getOp___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_Std_PersistentHashMap_find_x3f___rarg(x_1, x_2, x_3, x_4);
return x_5;
}
}
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_getOp(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Std_PersistentHashMap_getOp___rarg), 4, 0);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_instGetElemPersistentHashMapOptionTrue___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
@ -1527,7 +1509,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Std_PersistentHashMap_find_x21___rarg___closed__1;
x_2 = l_Std_PersistentHashMap_find_x21___rarg___closed__2;
x_3 = lean_unsigned_to_nat(161u);
x_3 = lean_unsigned_to_nat(158u);
x_4 = lean_unsigned_to_nat(14u);
x_5 = l_Std_PersistentHashMap_find_x21___rarg___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);