chore: update stage0
This commit is contained in:
parent
7537fa7795
commit
c447db5db9
11 changed files with 968 additions and 964 deletions
16
stage0/src/Init/Control/Lawful.lean
generated
16
stage0/src/Init/Control/Lawful.lean
generated
|
|
@ -44,7 +44,7 @@ attribute [simp] map_pure seq_pure
|
|||
simp [pure_seq]
|
||||
|
||||
class LawfulMonad (m : Type u → Type v) [Monad m] extends LawfulApplicative m : Prop where
|
||||
bind_pure_comp (f : α → β) (x : m α) : x >>= pure ∘ f = f <$> x
|
||||
bind_pure_comp (f : α → β) (x : m α) : x >>= (fun a => pure (f a)) = f <$> x
|
||||
bind_map {α β : Type u} (f : m (α → β)) (x : m α) : f >>= (. <$> x) = f <*> x
|
||||
pure_bind (x : α) (f : α → m β) : pure x >>= f = f x
|
||||
bind_assoc (x : m α) (f : α → m β) (g : β → m γ) : x >>= f >>= g = x >>= fun x => f x >>= g
|
||||
|
|
@ -52,9 +52,9 @@ class LawfulMonad (m : Type u → Type v) [Monad m] extends LawfulApplicative m
|
|||
seq_pure g x := (by rw [← bind_map]; simp [map_pure, bind_pure_comp])
|
||||
seq_assoc x g h := (by
|
||||
-- TODO: support for applying `symm` at `simp` arguments
|
||||
let bind_pure_comp_symm {α β : Type u} (f : α → β) (x : m α) : f <$> x = x >>= pure ∘ f := by
|
||||
have bind_pure_comp_symm {α β : Type u} (f : α → β) (x : m α) : f <$> x = x >>= fun a => pure (f a) := by
|
||||
rw [bind_pure_comp]
|
||||
let bind_map_symm {α β : Type u} (f : m (α → (β : Type u))) (x : m α) : f <*> x = f >>= (. <$> x) := by
|
||||
have bind_map_symm {α β : Type u} (f : m (α → (β : Type u))) (x : m α) : f <*> x = f >>= (. <$> x) := by
|
||||
rw [bind_map]
|
||||
simp[bind_pure_comp_symm, bind_map_symm, bind_assoc, pure_bind])
|
||||
|
||||
|
|
@ -62,7 +62,7 @@ export LawfulMonad (bind_pure_comp bind_map pure_bind bind_assoc)
|
|||
attribute [simp] pure_bind bind_assoc
|
||||
|
||||
@[simp] theorem bind_pure [Monad m] [LawfulMonad m] (x : m α) : x >>= pure = x := by
|
||||
show x >>= pure ∘ id = x
|
||||
show x >>= (fun a => pure (id a)) = x
|
||||
rw [bind_pure_comp, id_map]
|
||||
|
||||
theorem map_eq_pure_bind [Monad m] [LawfulMonad m] (f : α → β) (x : m α) : f <$> x = x >>= fun a => pure (f a) := by
|
||||
|
|
@ -75,11 +75,7 @@ theorem bind_congr [Bind m] {x : m α} {f g : α → m β} (h : ∀ a, f a = g a
|
|||
simp [funext h]
|
||||
|
||||
@[simp] theorem bind_pure_unit [Monad m] [LawfulMonad m] {x : m PUnit} : (x >>= fun _ => pure ⟨⟩) = x := by
|
||||
have : (x >>= fun _ => pure ⟨⟩) = (x >>= pure) := by
|
||||
apply bind_congr; intro u
|
||||
cases u; simp
|
||||
rw [bind_pure] at this
|
||||
assumption
|
||||
rw [bind_pure]
|
||||
|
||||
theorem map_congr [Functor m] {x : m α} {f g : α → β} (h : ∀ a, f a = g a) : (f <$> x : m β) = g <$> x := by
|
||||
simp [funext h]
|
||||
|
|
@ -264,7 +260,7 @@ theorem ext {x y : StateT σ m α} (h : ∀ s, x.run s = y.run s) : x = y :=
|
|||
@[simp] theorem run_modify [Monad m] (f : σ → σ) (s : σ) : (modify f : StateT σ m PUnit).run s = pure (⟨⟩, f s) := rfl
|
||||
|
||||
@[simp] theorem run_modifyGet [Monad m] (f : σ → α × σ) (s : σ) : (modifyGet f : StateT σ m α).run s = pure ((f s).1, (f s).2) := by
|
||||
simp [modifyGet, MonadStateOf.modifyGet, StateT.modifyGet, run]; cases f s <;> rfl
|
||||
simp [modifyGet, MonadStateOf.modifyGet, StateT.modifyGet, run]
|
||||
|
||||
@[simp] theorem run_lift {α σ : Type u} [Monad m] (x : m α) (s : σ) : (StateT.lift x : StateT σ m α).run s = x >>= fun a => pure (a, s) := rfl
|
||||
|
||||
|
|
|
|||
4
stage0/src/Init/Core.lean
generated
4
stage0/src/Init/Core.lean
generated
|
|
@ -16,6 +16,10 @@ def inline {α : Sort u} (a : α) : α := a
|
|||
@[inline] def flip {α : Sort u} {β : Sort v} {φ : Sort w} (f : α → β → φ) : β → α → φ :=
|
||||
fun b a => f a b
|
||||
|
||||
@[simp] theorem Function.const_apply {y : β} {x : α} : const α y x = y := rfl
|
||||
|
||||
@[simp] theorem Function.comp_apply {f : β → δ} {g : α → β} {x : α} : comp f g x = f (g x) := rfl
|
||||
|
||||
/--
|
||||
Thunks are "lazy" values that are evaluated when first accessed using `Thunk.get/map/bind`.
|
||||
The value is then stored and not recomputed for all further accesses. -/
|
||||
|
|
|
|||
4
stage0/src/Init/Prelude.lean
generated
4
stage0/src/Init/Prelude.lean
generated
|
|
@ -9,10 +9,10 @@ universe u v w
|
|||
|
||||
@[inline] def id {α : Sort u} (a : α) : α := a
|
||||
|
||||
abbrev Function.comp {α : Sort u} {β : Sort v} {δ : Sort w} (f : β → δ) (g : α → β) : α → δ :=
|
||||
@[inline] def Function.comp {α : Sort u} {β : Sort v} {δ : Sort w} (f : β → δ) (g : α → β) : α → δ :=
|
||||
fun x => f (g x)
|
||||
|
||||
abbrev Function.const {α : Sort u} (β : Sort v) (a : α) : β → α :=
|
||||
@[inline] def Function.const {α : Sort u} (β : Sort v) (a : α) : β → α :=
|
||||
fun x => a
|
||||
|
||||
set_option checkBinderAnnotations false in
|
||||
|
|
|
|||
2
stage0/src/Lean/Meta/DiscrTree.lean
generated
2
stage0/src/Lean/Meta/DiscrTree.lean
generated
|
|
@ -259,7 +259,7 @@ where
|
|||
step (e : Expr) := do
|
||||
let e ← whnfCore e
|
||||
match (← unfoldDefinition? e) with
|
||||
| some e' => if isBadKey e' then return e else step e'
|
||||
| some e' => if isBadKey e'.getAppFn then return e else step e'
|
||||
| none => return e
|
||||
|
||||
/-- whnf for the discrimination tree module -/
|
||||
|
|
|
|||
6
stage0/stdlib/Lean/Elab/Do.c
generated
6
stage0/stdlib/Lean/Elab/Do.c
generated
|
|
@ -833,7 +833,7 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Do_0__L
|
|||
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_pullExitPointsAux___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__8___closed__10;
|
||||
static lean_object* l_Lean_Elab_Term_Do_ToTerm_breakToTerm___closed__15;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_28245_(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_28248_(lean_object*);
|
||||
static lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doSeqToCode___lambda__1___closed__1;
|
||||
static lean_object* l_Lean_Elab_Term_Do_pullExitPointsAux___lambda__1___closed__9;
|
||||
static lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doSeqToCode___closed__3;
|
||||
|
|
@ -41442,7 +41442,7 @@ x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1);
|
|||
return x_6;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_28245_(lean_object* x_1) {
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_28248_(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3;
|
||||
|
|
@ -43011,7 +43011,7 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Do_elabDo___closed__5);
|
|||
res = l___regBuiltin_Lean_Elab_Term_Do_elabDo(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_28245_(lean_io_mk_world());
|
||||
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_28248_(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
l___regBuiltin_Lean_Elab_Term_expandTermFor___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_expandTermFor___closed__1();
|
||||
|
|
|
|||
68
stage0/stdlib/Lean/Elab/Inductive.c
generated
68
stage0/stdlib/Lean/Elab/Inductive.c
generated
|
|
@ -16,6 +16,7 @@ extern "C" {
|
|||
lean_object* l_List_reverse___rarg(lean_object*);
|
||||
static lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_checkParamsAndResultType___lambda__1___closed__4;
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_elabCtors(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__5;
|
||||
static lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_elabHeaderAux___lambda__2___closed__1;
|
||||
lean_object* lean_expr_update_forall(lean_object*, uint8_t, lean_object*, lean_object*);
|
||||
lean_object* lean_array_set(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -61,7 +62,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Command_mkResultUniverse(lean_object*, lean
|
|||
LEAN_EXPORT lean_object* l_Lean_Elab_Command_instInhabitedElabHeaderResult;
|
||||
static lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_mkInductiveDecl___lambda__2___closed__3;
|
||||
LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_getResultingUniverse___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__5;
|
||||
static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__3;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Command_instInhabitedInductiveView;
|
||||
lean_object* l_Lean_Meta_removeUnused(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_throwUnexpectedInductiveType___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -73,7 +74,6 @@ LEAN_EXPORT lean_object* l_Lean_Meta_forallTelescopeReducing___at___private_Lean
|
|||
lean_object* l_Lean_Expr_ReplaceLevelImpl_replaceUnsafeM_visit(lean_object*, size_t, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_collectUniverses___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_extract___rarg(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__3;
|
||||
static lean_object* l_Lean_Elab_Command_checkValidInductiveModifier___rarg___lambda__1___closed__1;
|
||||
static lean_object* l_List_mapTRAux___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_applyInferMod___spec__1___closed__4;
|
||||
static lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_elabCtors_elabCtorType___closed__2;
|
||||
|
|
@ -86,6 +86,7 @@ extern lean_object* l_Lean_Elab_instInhabitedAttribute;
|
|||
LEAN_EXPORT lean_object* l_List_mapTRAux___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_applyInferMod___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Command_checkValidCtorModifier___rarg___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_withInductiveLocalDecls___spec__1(size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__4;
|
||||
lean_object* lean_mk_cases_on(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_updateParams___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Std_HashMapImp_find_x3f___at_Lean_hasOutParams___spec__2(lean_object*, lean_object*);
|
||||
|
|
@ -111,7 +112,6 @@ LEAN_EXPORT lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_wi
|
|||
static lean_object* l_Std_Range_forIn_loop___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_elabCtors_checkParamOccs___spec__1___closed__3;
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_applyDerivingHandlers___spec__4(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_checkParamsAndResultType___lambda__1___closed__1;
|
||||
static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__2;
|
||||
LEAN_EXPORT lean_object* l_List_mapTRAux___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_applyInferMod___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_expr_instantiate1(lean_object*, lean_object*);
|
||||
lean_object* l_Array_toSubarray___rarg(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -122,6 +122,7 @@ static lean_object* l_Lean_Elab_Command_instInhabitedCtorView___closed__3;
|
|||
lean_object* lean_array_get_size(lean_object*);
|
||||
static lean_object* l_List_mapTRAux___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_applyInferMod___spec__1___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_throwUnexpectedInductiveType___spec__1(lean_object*);
|
||||
static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__2;
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_elabHeaderAux___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_List_forM___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_collectUsed___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Command_accLevelAtCtor___closed__1;
|
||||
|
|
@ -134,7 +135,6 @@ static lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_throwUn
|
|||
LEAN_EXPORT lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_mkInductiveDecl___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Level_getOffsetAux(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_mkIndFVar2Const(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__4;
|
||||
lean_object* l_Std_mkHashSetImp___rarg(lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_checkNumParams___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_elabCtors_checkParamOccs___lambda__2___closed__1;
|
||||
|
|
@ -184,6 +184,7 @@ static lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_checkPa
|
|||
LEAN_EXPORT lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_mkTypeFor___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Command_checkResultingUniverse___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Command_checkValidCtorModifier___rarg(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__6;
|
||||
lean_object* l_Lean_throwError___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Command_instInhabitedElabHeaderResult___closed__3;
|
||||
lean_object* l_Std_HashMap_insert___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -193,6 +194,7 @@ lean_object* l___private_Lean_Expr_0__Lean_Expr_getAppArgsAux(lean_object*, lean
|
|||
LEAN_EXPORT lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_mkInductiveDecl___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Command_checkResultingUniverse___closed__2;
|
||||
lean_object* lean_mk_ibelow(lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__1;
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_withInductiveLocalDecls_loop___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_runTermElabM___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_mkSizeOfInstances(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -218,7 +220,6 @@ static lean_object* l_Lean_Elab_Command_instInhabitedElabHeaderResult___closed__
|
|||
LEAN_EXPORT lean_object* l_List_mapTRAux___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_updateResultingUniverse___spec__1___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_updateResultingUniverse___spec__2___lambda__1___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_mkInductiveDecl___lambda__3___boxed(lean_object**);
|
||||
LEAN_EXPORT lean_object* l_List_mapM___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_updateParams___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__1;
|
||||
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingImp___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_List_mapM___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_replaceIndFVarsWithConsts___spec__2___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_mkInductiveDecl___lambda__2___closed__4;
|
||||
|
|
@ -396,7 +397,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_el
|
|||
static lean_object* l_Lean_Elab_Command_instInhabitedElabHeaderResult___closed__9;
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_eqvFirstTypeResult___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_List_mapM___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_elabCtors___spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178_(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179_(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_5_(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_mkIBelow___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_mkAuxConstructions___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Command_tmpIndParam___closed__3;
|
||||
|
|
@ -512,7 +513,6 @@ lean_object* lean_expr_update_app(lean_object*, lean_object*, lean_object*);
|
|||
LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at_Lean_Elab_Command_accLevelAtCtor___spec__2(lean_object*, lean_object*, size_t, size_t);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Command_checkValidCtorModifier___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_levelOne;
|
||||
static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__6;
|
||||
uint8_t lean_level_eq(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_mkInductiveDecl___spec__2(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Command_checkValidCtorModifier___rarg___lambda__1___closed__1;
|
||||
|
|
@ -8895,7 +8895,7 @@ lean_dec(x_2);
|
|||
return x_12;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__1() {
|
||||
static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -8903,17 +8903,17 @@ x_1 = lean_mk_string("bootstrap");
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__2() {
|
||||
static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = lean_box(0);
|
||||
x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__1;
|
||||
x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__1;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__3() {
|
||||
static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -8921,17 +8921,17 @@ x_1 = lean_mk_string("inductiveCheckResultingUniverse");
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__4() {
|
||||
static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__4() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__2;
|
||||
x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__3;
|
||||
x_1 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__2;
|
||||
x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__3;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__5() {
|
||||
static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__5() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -8939,13 +8939,13 @@ x_1 = lean_mk_string("by default the `inductive/structure commands report an err
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__6() {
|
||||
static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__6() {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_1 = 1;
|
||||
x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__1;
|
||||
x_3 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__5;
|
||||
x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__1;
|
||||
x_3 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__5;
|
||||
x_4 = lean_box(x_1);
|
||||
x_5 = lean_alloc_ctor(0, 3, 0);
|
||||
lean_ctor_set(x_5, 0, x_4);
|
||||
|
|
@ -8954,12 +8954,12 @@ lean_ctor_set(x_5, 2, x_3);
|
|||
return x_5;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178_(lean_object* x_1) {
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179_(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
||||
x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__4;
|
||||
x_3 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__6;
|
||||
x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__4;
|
||||
x_3 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__6;
|
||||
x_4 = l_Lean_Option_register___at_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_6____spec__1(x_2, x_3, x_1);
|
||||
return x_4;
|
||||
}
|
||||
|
|
@ -17737,21 +17737,21 @@ l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_updateResultingUniverse___l
|
|||
lean_mark_persistent(l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_updateResultingUniverse___lambda__2___closed__5);
|
||||
l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_updateResultingUniverse___lambda__2___closed__6 = _init_l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_updateResultingUniverse___lambda__2___closed__6();
|
||||
lean_mark_persistent(l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_updateResultingUniverse___lambda__2___closed__6);
|
||||
l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__1 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__1();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__1);
|
||||
l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__2 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__2();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__2);
|
||||
l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__3 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__3();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__3);
|
||||
l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__4 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__4();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__4);
|
||||
l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__5 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__5();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__5);
|
||||
l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__6 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__6();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178____closed__6);
|
||||
l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__1 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__1();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__1);
|
||||
l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__2 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__2();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__2);
|
||||
l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__3 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__3();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__3);
|
||||
l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__4 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__4();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__4);
|
||||
l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__5 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__5();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__5);
|
||||
l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__6 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__6();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179____closed__6);
|
||||
l_Lean_Elab_Command_bootstrap_inductiveCheckResultingUniverse___closed__1 = _init_l_Lean_Elab_Command_bootstrap_inductiveCheckResultingUniverse___closed__1();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_bootstrap_inductiveCheckResultingUniverse___closed__1);
|
||||
res = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4178_(lean_io_mk_world());
|
||||
res = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Inductive___hyg_4179_(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
l_Lean_Elab_Command_bootstrap_inductiveCheckResultingUniverse = lean_io_result_get_value(res);
|
||||
lean_mark_persistent(l_Lean_Elab_Command_bootstrap_inductiveCheckResultingUniverse);
|
||||
|
|
|
|||
6
stage0/stdlib/Lean/Elab/StructInst.c
generated
6
stage0/stdlib/Lean/Elab/StructInst.c
generated
|
|
@ -120,7 +120,7 @@ LEAN_EXPORT lean_object* l_List_mapTRAux___at___private_Lean_Elab_StructInst_0__
|
|||
static lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_getStructName___rarg___closed__5;
|
||||
lean_object* l_Lean_addTrace_addTraceOptions(lean_object*);
|
||||
static lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_mkDefaultValueAux_x3f___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Term_StructInst_initFn____x40_Lean_Elab_StructInst___hyg_9246_(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Term_StructInst_initFn____x40_Lean_Elab_StructInst___hyg_9243_(lean_object*);
|
||||
static lean_object* l___regBuiltin_Lean_Elab_Term_StructInst_expandStructInstExpectedType___closed__2;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_mkDefaultValueAux_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Meta_0__Lean_Syntax_isNatLitAux(lean_object*, lean_object*);
|
||||
|
|
@ -23596,7 +23596,7 @@ x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1);
|
|||
return x_6;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Term_StructInst_initFn____x40_Lean_Elab_StructInst___hyg_9246_(lean_object* x_1) {
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Term_StructInst_initFn____x40_Lean_Elab_StructInst___hyg_9243_(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3;
|
||||
|
|
@ -24176,7 +24176,7 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_StructInst_elabStructInst___c
|
|||
res = l___regBuiltin_Lean_Elab_Term_StructInst_elabStructInst(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
res = l_Lean_Elab_Term_StructInst_initFn____x40_Lean_Elab_StructInst___hyg_9246_(lean_io_mk_world());
|
||||
res = l_Lean_Elab_Term_StructInst_initFn____x40_Lean_Elab_StructInst___hyg_9243_(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
return lean_io_result_mk_ok(lean_box(0));
|
||||
|
|
|
|||
88
stage0/stdlib/Lean/Meta/DiscrTree.c
generated
88
stage0/stdlib/Lean/Meta/DiscrTree.c
generated
|
|
@ -3137,15 +3137,17 @@ uint8_t x_16;
|
|||
x_16 = !lean_is_exclusive(x_10);
|
||||
if (x_16 == 0)
|
||||
{
|
||||
lean_object* x_17; lean_object* x_18; lean_object* x_19; uint8_t x_20;
|
||||
lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; uint8_t x_21;
|
||||
x_17 = lean_ctor_get(x_10, 1);
|
||||
x_18 = lean_ctor_get(x_10, 0);
|
||||
lean_dec(x_18);
|
||||
x_19 = lean_ctor_get(x_11, 0);
|
||||
lean_inc(x_19);
|
||||
lean_dec(x_11);
|
||||
x_20 = l___private_Lean_Meta_DiscrTree_0__Lean_Meta_DiscrTree_isBadKey(x_19);
|
||||
if (x_20 == 0)
|
||||
x_20 = l_Lean_Expr_getAppFn(x_19);
|
||||
x_21 = l___private_Lean_Meta_DiscrTree_0__Lean_Meta_DiscrTree_isBadKey(x_20);
|
||||
lean_dec(x_20);
|
||||
if (x_21 == 0)
|
||||
{
|
||||
lean_free_object(x_10);
|
||||
lean_dec(x_8);
|
||||
|
|
@ -3166,89 +3168,91 @@ return x_10;
|
|||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_22; lean_object* x_23; uint8_t x_24;
|
||||
x_22 = lean_ctor_get(x_10, 1);
|
||||
lean_inc(x_22);
|
||||
lean_dec(x_10);
|
||||
x_23 = lean_ctor_get(x_11, 0);
|
||||
lean_object* x_23; lean_object* x_24; lean_object* x_25; uint8_t x_26;
|
||||
x_23 = lean_ctor_get(x_10, 1);
|
||||
lean_inc(x_23);
|
||||
lean_dec(x_10);
|
||||
x_24 = lean_ctor_get(x_11, 0);
|
||||
lean_inc(x_24);
|
||||
lean_dec(x_11);
|
||||
x_24 = l___private_Lean_Meta_DiscrTree_0__Lean_Meta_DiscrTree_isBadKey(x_23);
|
||||
if (x_24 == 0)
|
||||
x_25 = l_Lean_Expr_getAppFn(x_24);
|
||||
x_26 = l___private_Lean_Meta_DiscrTree_0__Lean_Meta_DiscrTree_isBadKey(x_25);
|
||||
lean_dec(x_25);
|
||||
if (x_26 == 0)
|
||||
{
|
||||
lean_dec(x_8);
|
||||
x_1 = x_23;
|
||||
x_6 = x_22;
|
||||
x_1 = x_24;
|
||||
x_6 = x_23;
|
||||
goto _start;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_26;
|
||||
lean_dec(x_23);
|
||||
lean_object* x_28;
|
||||
lean_dec(x_24);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
x_26 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_26, 0, x_8);
|
||||
lean_ctor_set(x_26, 1, x_22);
|
||||
return x_26;
|
||||
x_28 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_28, 0, x_8);
|
||||
lean_ctor_set(x_28, 1, x_23);
|
||||
return x_28;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_27;
|
||||
uint8_t x_29;
|
||||
lean_dec(x_8);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
x_27 = !lean_is_exclusive(x_10);
|
||||
if (x_27 == 0)
|
||||
x_29 = !lean_is_exclusive(x_10);
|
||||
if (x_29 == 0)
|
||||
{
|
||||
return x_10;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_28; lean_object* x_29; lean_object* x_30;
|
||||
x_28 = lean_ctor_get(x_10, 0);
|
||||
x_29 = lean_ctor_get(x_10, 1);
|
||||
lean_inc(x_29);
|
||||
lean_inc(x_28);
|
||||
lean_object* x_30; lean_object* x_31; lean_object* x_32;
|
||||
x_30 = lean_ctor_get(x_10, 0);
|
||||
x_31 = lean_ctor_get(x_10, 1);
|
||||
lean_inc(x_31);
|
||||
lean_inc(x_30);
|
||||
lean_dec(x_10);
|
||||
x_30 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_30, 0, x_28);
|
||||
lean_ctor_set(x_30, 1, x_29);
|
||||
return x_30;
|
||||
x_32 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_32, 0, x_30);
|
||||
lean_ctor_set(x_32, 1, x_31);
|
||||
return x_32;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_31;
|
||||
uint8_t x_33;
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
x_31 = !lean_is_exclusive(x_7);
|
||||
if (x_31 == 0)
|
||||
x_33 = !lean_is_exclusive(x_7);
|
||||
if (x_33 == 0)
|
||||
{
|
||||
return x_7;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_32; lean_object* x_33; lean_object* x_34;
|
||||
x_32 = lean_ctor_get(x_7, 0);
|
||||
x_33 = lean_ctor_get(x_7, 1);
|
||||
lean_inc(x_33);
|
||||
lean_inc(x_32);
|
||||
lean_object* x_34; lean_object* x_35; lean_object* x_36;
|
||||
x_34 = lean_ctor_get(x_7, 0);
|
||||
x_35 = lean_ctor_get(x_7, 1);
|
||||
lean_inc(x_35);
|
||||
lean_inc(x_34);
|
||||
lean_dec(x_7);
|
||||
x_34 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_34, 0, x_32);
|
||||
lean_ctor_set(x_34, 1, x_33);
|
||||
return x_34;
|
||||
x_36 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_36, 0, x_34);
|
||||
lean_ctor_set(x_36, 1, x_35);
|
||||
return x_36;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
190
stage0/stdlib/Lean/Meta/Match/Match.c
generated
190
stage0/stdlib/Lean/Meta/Match/Match.c
generated
|
|
@ -24,7 +24,6 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_wi
|
|||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_mkMatcher___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_List_moveToFront_loop___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_checkNumPatterns___closed__1;
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__1;
|
||||
lean_object* lean_array_set(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processConstructor___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_mkMatcher___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -72,6 +71,7 @@ lean_object* l_Lean_LocalDecl_userName(lean_object*);
|
|||
LEAN_EXPORT lean_object* l_List_mapTRAux___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processArrayLit___spec__1(lean_object*, lean_object*);
|
||||
static lean_object* l_List_mapM___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processVariable___spec__2___closed__1;
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_withAlts___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__1;
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_mkMatcher___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_List_mapM___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processArrayLit___spec__8___closed__2;
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_throwInductiveTypeExpected(lean_object*);
|
||||
|
|
@ -84,6 +84,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_Match_mkMatcher___lambda__4___boxed(lean_ob
|
|||
lean_object* lean_array_uget(lean_object*, size_t);
|
||||
LEAN_EXPORT lean_object* l_List_foldr___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_isArrayLitTransition___spec__1___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_mkMatcher___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____lambda__1___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_List_mapTRAux___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processArrayLit___spec__2(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_append___rarg(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_List_mapTRAux___at_Lean_Meta_Match_processInaccessibleAsCtor___spec__4(lean_object*, lean_object*);
|
||||
|
|
@ -122,6 +123,7 @@ lean_object* l_Lean_Meta_saveState___rarg(lean_object*, lean_object*, lean_objec
|
|||
lean_object* l_Lean_EnvExtensionInterfaceUnsafe_imp___elambda__2___rarg(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_process_tryToProcess___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_matchMatcherApp_x3f___at_Lean_Meta_Match_withMkMatcherInput___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__4;
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoArrayLit(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_withAlts_loop___rarg___closed__12;
|
||||
LEAN_EXPORT lean_object* l_List_mapTRAux___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_moveToFront___spec__7(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -136,7 +138,6 @@ LEAN_EXPORT lean_object* l_List_mapTRAux___at___private_Lean_Meta_Match_Match_0_
|
|||
uint8_t l_Lean_checkTraceOption(lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_throwCasesException___rarg___closed__1;
|
||||
static lean_object* l_Lean_Meta_Match_getMkMatcherInputInContext___closed__2;
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__4;
|
||||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_unify_x3f___closed__5;
|
||||
lean_object* l_Lean_Meta_dependsOn(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_st_ref_get(lean_object*, lean_object*);
|
||||
|
|
@ -150,7 +151,6 @@ LEAN_EXPORT uint8_t l_Lean_Meta_Match_Unify_occurs(lean_object*, lean_object*);
|
|||
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processConstructor___spec__11(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t lean_name_eq(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_checkNumPatterns(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__8;
|
||||
lean_object* l_Lean_Expr_constructorApp_x3f(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_Match_mkMatcher___spec__5___boxed(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_throwCasesException___rarg___closed__6;
|
||||
|
|
@ -163,6 +163,7 @@ static lean_object* l_Lean_Meta_Match_Unify_assign___closed__7;
|
|||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_hasValPattern___boxed(lean_object*);
|
||||
static lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_Match_getMkMatcherInputInContext___spec__5___lambda__1___closed__1;
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_withAlts_loop___rarg___lambda__2___boxed(lean_object**);
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__8;
|
||||
lean_object* lean_expr_instantiate1(lean_object*, lean_object*);
|
||||
lean_object* l_Array_toSubarray___rarg(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_collectValues(lean_object*);
|
||||
|
|
@ -175,7 +176,6 @@ static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_process
|
|||
LEAN_EXPORT lean_object* l_Lean_addTrace___at_Lean_Meta_Match_Unify_assign___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_throwCasesException___rarg___closed__13;
|
||||
static lean_object* l_Lean_Meta_Match_mkMatcher___lambda__5___closed__8;
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__2;
|
||||
LEAN_EXPORT uint8_t l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_hasNatValPattern(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_List_mapTRAux___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processConstructor___spec__7(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_MessageData_ofList(lean_object*);
|
||||
|
|
@ -208,6 +208,7 @@ LEAN_EXPORT lean_object* l_Nat_foldAux___at_Lean_Meta_Match_mkMatcher___spec__4_
|
|||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_checkNextPatternTypes___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_List_filterAux___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processValue___spec__1(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_mkMatcher(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__2;
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_matchMatcherApp_x3f___at_Lean_Meta_Match_withMkMatcherInput___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processArrayLit___lambda__1___closed__2;
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_withAlts_loop(lean_object*);
|
||||
|
|
@ -243,7 +244,6 @@ LEAN_EXPORT uint8_t l_List_foldr___at___private_Lean_Meta_Match_Match_0__Lean_Me
|
|||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_mkMatcher___lambda__8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Meta_Match_withMkMatcherInput___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_List_mapM___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoArrayLit_loop___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__2;
|
||||
LEAN_EXPORT lean_object* l_List_foldl___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processLeaf___spec__6___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processLeaf___spec__7(lean_object*, lean_object*);
|
||||
uint32_t lean_uint32_add(uint32_t, uint32_t);
|
||||
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_withAlts_mkMinorType___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -254,7 +254,7 @@ lean_object* l_Lean_mkAppN(lean_object*, lean_object*);
|
|||
static lean_object* l_List_filterMapM_loop___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processNonVariable___spec__1___closed__2;
|
||||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_withAlts_loop___rarg___closed__3;
|
||||
size_t lean_uint64_to_usize(uint64_t);
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Match_Match___hyg_11699_(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Match_Match___hyg_11694_(lean_object*);
|
||||
uint8_t l_Lean_Environment_hasUnsafe(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_checkNextPatternTypes(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processLeaf___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -280,6 +280,7 @@ static lean_object* l_Lean_Meta_Match_mkMatcher___lambda__7___closed__2;
|
|||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_throwCasesException___rarg___closed__15;
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_processInaccessibleAsCtor(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_panic___at___private_Lean_Meta_Tactic_Contradiction_0__Lean_Meta_processGenDiseq___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__2;
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_withAlts(lean_object*);
|
||||
static lean_object* l_Lean_Meta_Match_processInaccessibleAsCtor___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_process_tryToProcess___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -287,6 +288,7 @@ lean_object* lean_array_fget(lean_object*, lean_object*);
|
|||
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Meta_Match_withMkMatcherInput___spec__3(lean_object*);
|
||||
static lean_object* l_List_mapTRAux___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandNatValuePattern___spec__1___closed__2;
|
||||
LEAN_EXPORT lean_object* l_List_filterAux___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processConstructor___spec__8___boxed(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__1;
|
||||
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_throwCasesException___rarg___closed__18;
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processConstructor___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -297,7 +299,6 @@ LEAN_EXPORT lean_object* l_List_mapTRAux___at___private_Lean_Meta_Match_Match_0_
|
|||
LEAN_EXPORT lean_object* l_List_mapTRAux___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoCtor_x3f___spec__4(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_Match_Pattern_toMessageData(lean_object*);
|
||||
lean_object* lean_st_ref_take(lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__4;
|
||||
static lean_object* l_List_mapTRAux___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processSkipInaccessible___spec__3___closed__4;
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_mkMatcher___lambda__9(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoCtor_x3f___lambda__1___boxed__const__1;
|
||||
|
|
@ -315,6 +316,7 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_Match_getMkMatche
|
|||
LEAN_EXPORT lean_object* l_List_forIn_loop___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_checkNextPatternTypes___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_List_mapTRAux___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandNatValuePattern___spec__1___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_Unify_assign___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__4;
|
||||
lean_object* l_Lean_Meta_Match_Alt_checkAndReplaceFVarId(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_List_forIn_loop___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_checkNextPatternTypes___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processAsPattern___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -390,7 +392,6 @@ static lean_object* l_List_filterMapM_loop___at___private_Lean_Meta_Match_Match_
|
|||
lean_object* lean_st_mk_ref(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_List_mapTRAux___at_Lean_Meta_Match_mkMatcher___spec__6(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_matcherExt;
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__1;
|
||||
extern lean_object* l_Lean_Expr_instHashableExpr;
|
||||
static lean_object* l_Lean_EnvExtensionInterfaceUnsafe_getState___at_Lean_Meta_Match_mkMatcherAuxDefinition___spec__1___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_Unify_assign(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -435,7 +436,6 @@ static lean_object* l_Lean_Meta_Match_getMkMatcherInputInContext___lambda__3___c
|
|||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processLeaf(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_MatcherApp_addArg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processArrayLit(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__3;
|
||||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processAsPattern___closed__1;
|
||||
lean_object* l___private_Init_Util_0__mkPanicMessageWithDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Meta_Match_Unify_assign___closed__8;
|
||||
|
|
@ -449,13 +449,13 @@ LEAN_EXPORT lean_object* l_panic___at___private_Lean_Meta_Match_Match_0__Lean_Me
|
|||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_withAlts_loop___rarg___closed__2;
|
||||
LEAN_EXPORT uint8_t l_List_foldr___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_isVariableTransition___spec__1(uint8_t, lean_object*);
|
||||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_process_tryToProcess___lambda__1___closed__2;
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____lambda__1___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_getMkMatcherInputInContext___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_getMkMatcherInputInContext___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_contradictionCore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_Closure_mkValueTypeClosure(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Meta_Match_getMkMatcherInputInContext___lambda__3___closed__2;
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_processInaccessibleAsCtor___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__3;
|
||||
LEAN_EXPORT lean_object* l_Lean_Expr_withAppAux___at_Lean_Meta_Match_getMkMatcherInputInContext___spec__3___boxed__const__1;
|
||||
static lean_object* l_Lean_Meta_Match_Unify_assign___closed__1;
|
||||
LEAN_EXPORT lean_object* l_List_foldr___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_hasValPattern___spec__1___boxed(lean_object*, lean_object*);
|
||||
|
|
@ -467,7 +467,6 @@ LEAN_EXPORT lean_object* l_List_mapTRAux___at___private_Lean_Meta_Match_Match_0_
|
|||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_withAlts_mkMinorType___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_mkFVar(lean_object*);
|
||||
uint8_t l_List_elem___at_Lean_Occurrences_contains___spec__1(lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__6;
|
||||
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_Match_mkMatcher___spec__2___boxed(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_indexOfAux___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_getUElimPos_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_Match_toPattern___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -492,6 +491,7 @@ lean_object* l_Lean_Meta_withMVarContext___at___private_Lean_Meta_SynthInstance_
|
|||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processLeaf___closed__1;
|
||||
static lean_object* l_Lean_Meta_Match_mkMatcher___lambda__8___closed__1;
|
||||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_withAlts_loop___rarg___lambda__1___closed__2;
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__6;
|
||||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_withAlts_loop___rarg___lambda__1___closed__5;
|
||||
lean_object* l_Lean_LocalDecl_fvarId(lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_List_moveToFront___rarg(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -520,7 +520,6 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_pr
|
|||
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoCtor_x3f___spec__1(size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_List_redLength___rarg(lean_object*);
|
||||
lean_object* l_Std_PersistentArray_push___rarg(lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__7;
|
||||
lean_object* l_Lean_Meta_Cases_cases(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processLeaf___closed__5;
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_isNatValueTransition___boxed(lean_object*);
|
||||
|
|
@ -536,6 +535,7 @@ LEAN_EXPORT uint8_t l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_hasAsPa
|
|||
LEAN_EXPORT lean_object* l_List_foldr___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_hasCtorPattern___spec__1___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_panic___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processVariable___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processArrayLit___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__7;
|
||||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processValue___closed__1;
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_traceState___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_getLocalDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -577,6 +577,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_Li
|
|||
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_withAlts_mkMinorType___spec__1(size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_hasNatValPattern___boxed(lean_object*);
|
||||
static lean_object* l_List_filterMapM_loop___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processNonVariable___spec__1___closed__4;
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__5;
|
||||
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Meta_Match_processInaccessibleAsCtor___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT uint8_t l_List_foldr___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_hasValPattern___spec__1(uint8_t, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_List_mapTRAux___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processConstructor___spec__4___boxed(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -591,7 +592,6 @@ LEAN_EXPORT lean_object* l_List_filterAux___at___private_Lean_Meta_Match_Match_0
|
|||
LEAN_EXPORT lean_object* l_Lean_EnvExtensionInterfaceUnsafe_getState___at_Lean_Meta_Match_mkMatcherAuxDefinition___spec__1(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_List_mapTRAux___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processValue___spec__7___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Meta_LevelDefEq_0__Lean_Meta_postponeIsLevelDefEq___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__5;
|
||||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_process_tryToProcess___lambda__1___closed__4;
|
||||
LEAN_EXPORT lean_object* l_Array_mapIdxM_map___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processValue___spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_throwCasesException___rarg___closed__10;
|
||||
|
|
@ -600,6 +600,7 @@ lean_object* l_Array_ofSubarray___rarg(lean_object*);
|
|||
LEAN_EXPORT lean_object* l_List_mapM___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processAsPattern___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_unify_x3f___closed__6;
|
||||
lean_object* l_Lean_Meta_getLevel(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__3;
|
||||
static lean_object* l_Lean_Meta_MatcherApp_addArg___lambda__4___closed__2;
|
||||
LEAN_EXPORT lean_object* l_Nat_foldAux___at_Lean_Meta_Match_mkMatcher___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_nat_mul(lean_object*, lean_object*);
|
||||
|
|
@ -653,7 +654,6 @@ static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_withAlt
|
|||
lean_object* l_instHashableProd___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_Match_MatcherInfo_arity(lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoArrayLit_loop___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__5;
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_Unify_unify(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_Unify_expandIfVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_List_mapTRAux___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processValue___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -661,7 +661,6 @@ lean_object* l_Lean_Meta_instantiateMVars(lean_object*, lean_object*, lean_objec
|
|||
LEAN_EXPORT lean_object* l_Std_HashSetImp_insert___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processLeaf___spec__3(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Meta_Match_processInaccessibleAsCtor___closed__3;
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__3;
|
||||
lean_object* lean_mk_array(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_withExistingLocalDecls___at_Lean_Meta_Match_Alt_toMessageData___spec__3___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_List_filterAux___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processArrayLit___spec__6(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -671,7 +670,6 @@ static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_process
|
|||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_Unify_occurs___boxed(lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_traceStep___closed__1;
|
||||
lean_object* l_Lean_Meta_withLocalDecl___at_Lean_Meta_GeneralizeTelescope_generalizeTelescopeAux___spec__1___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__6;
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoArrayLit___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Expr_instBEqExpr;
|
||||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_unify_x3f___closed__1;
|
||||
|
|
@ -681,6 +679,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_pr
|
|||
static lean_object* l_List_mapTRAux___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processValue___spec__6___closed__2;
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_List_moveToFront_loop___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_moveToFront___spec__2(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_getMkMatcherInputInContext___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__9;
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_throwCasesException___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processNonVariable___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_getMatcherInfo_x3f___at_Lean_Meta_reduceMatcher_x3f___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -719,7 +718,6 @@ static lean_object* l_Lean_Meta_Match_mkMatcher___lambda__5___closed__3;
|
|||
static lean_object* l_Lean_Meta_Match_mkMatcher___lambda__5___closed__7;
|
||||
LEAN_EXPORT lean_object* l_Std_HashSetImp_expand___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processLeaf___spec__4(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_process_tryToProcess(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__9;
|
||||
lean_object* l_Lean_Expr_getAppFn(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_List_mapTRAux___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processConstructor___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_List_mapTRAux___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processValue___spec__3(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -741,6 +739,7 @@ static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_process
|
|||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_unify_x3f___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_getMkMatcherInputInContext___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_instHashableBool___boxed(lean_object*);
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__6;
|
||||
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_lambdaTelescopeImp___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_mkLevelParam(lean_object*);
|
||||
static lean_object* l_Lean_Meta_MatcherApp_addArg___lambda__4___closed__4;
|
||||
|
|
@ -750,6 +749,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_Match_bootstrap_genMatcherCode;
|
|||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_moveToFront(lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Meta_Match_Unify_assign___closed__6;
|
||||
LEAN_EXPORT uint8_t l_List_foldr___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_inLocalDecls___spec__1(lean_object*, uint8_t, lean_object*);
|
||||
static lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__5;
|
||||
uint8_t lean_level_eq(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_mkMatcher___lambda__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_EStateM_pure___rarg(lean_object*, lean_object*);
|
||||
|
|
@ -779,13 +779,14 @@ LEAN_EXPORT lean_object* l_List_filterMapM_loop___at___private_Lean_Meta_Match_M
|
|||
lean_object* l_Lean_Meta_Match_Alt_applyFVarSubst(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_panic___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_List_moveToFront_loop___spec__1(lean_object*);
|
||||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_throwCasesException___rarg___closed__12;
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012_(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986_(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007_(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981_(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Meta_Match_withMkMatcherInput___spec__3___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_panic___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processAsPattern___spec__1___closed__1;
|
||||
lean_object* l_List_appendTR___rarg(lean_object*, lean_object*);
|
||||
LEAN_EXPORT uint8_t l_List_foldr___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_isArrayLitTransition___spec__1(uint8_t, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_Unify_isAltVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT uint8_t l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____lambda__1(uint8_t, uint8_t);
|
||||
LEAN_EXPORT lean_object* l_List_mapTRAux___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processConstructor___spec__5(lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processLeaf___closed__4;
|
||||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_throwInductiveTypeExpected___rarg___closed__2;
|
||||
|
|
@ -810,7 +811,6 @@ static lean_object* l_Lean_Meta_Match_mkMatcher___lambda__5___closed__5;
|
|||
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___lambda__2___closed__1;
|
||||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___closed__1;
|
||||
LEAN_EXPORT uint8_t l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____lambda__1(uint8_t, uint8_t);
|
||||
static lean_object* l_Lean_Meta_Match_withMkMatcherInput___rarg___lambda__1___closed__2;
|
||||
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_unify_x3f___closed__7;
|
||||
LEAN_EXPORT uint8_t l_List_foldr___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_checkNumPatterns___spec__1(lean_object* x_1, uint8_t x_2, lean_object* x_3) {
|
||||
|
|
@ -21802,7 +21802,7 @@ lean_dec(x_2);
|
|||
return x_7;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__1() {
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -21810,17 +21810,17 @@ x_1 = lean_mk_string("bootstrap");
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__2() {
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = lean_box(0);
|
||||
x_2 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__1;
|
||||
x_2 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__1;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__3() {
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -21828,17 +21828,17 @@ x_1 = lean_mk_string("genMatcherCode");
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__4() {
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__4() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__2;
|
||||
x_2 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__3;
|
||||
x_1 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__2;
|
||||
x_2 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__3;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__5() {
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__5() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -21846,13 +21846,13 @@ x_1 = lean_mk_string("disable code generation for auxiliary matcher function");
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__6() {
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__6() {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_1 = 1;
|
||||
x_2 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__1;
|
||||
x_3 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__5;
|
||||
x_2 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__1;
|
||||
x_3 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__5;
|
||||
x_4 = lean_box(x_1);
|
||||
x_5 = lean_alloc_ctor(0, 3, 0);
|
||||
lean_ctor_set(x_5, 0, x_4);
|
||||
|
|
@ -21861,12 +21861,12 @@ lean_ctor_set(x_5, 2, x_3);
|
|||
return x_5;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986_(lean_object* x_1) {
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981_(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
||||
x_2 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__4;
|
||||
x_3 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__6;
|
||||
x_2 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__4;
|
||||
x_3 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__6;
|
||||
x_4 = l_Lean_Option_register___at_Std_Format_initFn____x40_Lean_Data_Format___hyg_54____spec__1(x_2, x_3, x_1);
|
||||
return x_4;
|
||||
}
|
||||
|
|
@ -21884,7 +21884,7 @@ lean_ctor_set(x_4, 1, x_3);
|
|||
return x_4;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT uint8_t l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____lambda__1(uint8_t x_1, uint8_t x_2) {
|
||||
LEAN_EXPORT uint8_t l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____lambda__1(uint8_t x_1, uint8_t x_2) {
|
||||
_start:
|
||||
{
|
||||
if (x_1 == 0)
|
||||
|
|
@ -21908,37 +21908,37 @@ return x_2;
|
|||
}
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__1() {
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_alloc_closure((void*)(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____lambda__1___boxed), 2, 0);
|
||||
x_1 = lean_alloc_closure((void*)(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____lambda__1___boxed), 2, 0);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__2() {
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__1;
|
||||
x_1 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__1;
|
||||
x_2 = lean_alloc_closure((void*)(l_instBEq___rarg), 3, 1);
|
||||
lean_closure_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__3() {
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Expr_instBEqExpr;
|
||||
x_2 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__2;
|
||||
x_2 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__2;
|
||||
x_3 = lean_alloc_closure((void*)(l_instBEqProd___rarg), 4, 2);
|
||||
lean_closure_set(x_3, 0, x_1);
|
||||
lean_closure_set(x_3, 1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__4() {
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__4() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -21946,19 +21946,19 @@ x_1 = lean_alloc_closure((void*)(l_instHashableBool___boxed), 1, 0);
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__5() {
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__5() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Expr_instHashableExpr;
|
||||
x_2 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__4;
|
||||
x_2 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__4;
|
||||
x_3 = lean_alloc_closure((void*)(l_instHashableProd___rarg___boxed), 3, 2);
|
||||
lean_closure_set(x_3, 0, x_1);
|
||||
lean_closure_set(x_3, 1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__6() {
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__6() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -21966,21 +21966,21 @@ x_1 = l_Std_PersistentHashMap_mkEmptyEntriesArray(lean_box(0), lean_box(0));
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__7() {
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__7() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__6;
|
||||
x_1 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__6;
|
||||
x_2 = lean_alloc_ctor(0, 1, 0);
|
||||
lean_ctor_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__8() {
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__8() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__7;
|
||||
x_1 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__7;
|
||||
x_2 = lean_unsigned_to_nat(0u);
|
||||
x_3 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
|
|
@ -21988,26 +21988,26 @@ lean_ctor_set(x_3, 1, x_2);
|
|||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__9() {
|
||||
static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__9() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__8;
|
||||
x_1 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__8;
|
||||
x_2 = lean_alloc_closure((void*)(l_EStateM_pure___rarg), 2, 1);
|
||||
lean_closure_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012_(lean_object* x_1) {
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007_(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3;
|
||||
x_2 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__9;
|
||||
x_2 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__9;
|
||||
x_3 = l_Lean_EnvExtensionInterfaceUnsafe_registerExt___rarg(x_2, x_1);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____lambda__1___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____lambda__1___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_3; uint8_t x_4; uint8_t x_5; lean_object* x_6;
|
||||
|
|
@ -22015,7 +22015,7 @@ x_3 = lean_unbox(x_1);
|
|||
lean_dec(x_1);
|
||||
x_4 = lean_unbox(x_2);
|
||||
lean_dec(x_2);
|
||||
x_5 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____lambda__1(x_3, x_4);
|
||||
x_5 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____lambda__1(x_3, x_4);
|
||||
x_6 = lean_box(x_5);
|
||||
return x_6;
|
||||
}
|
||||
|
|
@ -22044,8 +22044,8 @@ static lean_object* _init_l_panic___at_Lean_Meta_Match_mkMatcherAuxDefinition___
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__3;
|
||||
x_2 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__5;
|
||||
x_1 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__3;
|
||||
x_2 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__5;
|
||||
x_3 = l_Std_PersistentHashMap_instInhabitedPersistentHashMap___rarg(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
|
|
@ -22464,8 +22464,8 @@ lean_inc(x_25);
|
|||
x_27 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_27, 0, x_25);
|
||||
lean_ctor_set(x_27, 1, x_26);
|
||||
x_28 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__3;
|
||||
x_29 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__5;
|
||||
x_28 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__3;
|
||||
x_29 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__5;
|
||||
lean_inc(x_27);
|
||||
x_30 = l_Std_PersistentHashMap_find_x3f___rarg(x_28, x_29, x_24, x_27);
|
||||
if (lean_obj_tag(x_30) == 0)
|
||||
|
|
@ -22686,8 +22686,8 @@ lean_inc(x_93);
|
|||
x_95 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_95, 0, x_93);
|
||||
lean_ctor_set(x_95, 1, x_94);
|
||||
x_96 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__3;
|
||||
x_97 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__5;
|
||||
x_96 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__3;
|
||||
x_97 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__5;
|
||||
lean_inc(x_95);
|
||||
x_98 = l_Std_PersistentHashMap_find_x3f___rarg(x_96, x_97, x_92, x_95);
|
||||
if (lean_obj_tag(x_98) == 0)
|
||||
|
|
@ -28059,7 +28059,7 @@ lean_dec(x_9);
|
|||
return x_15;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Match_Match___hyg_11699_(lean_object* x_1) {
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Match_Match___hyg_11694_(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3;
|
||||
|
|
@ -28505,48 +28505,48 @@ l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_getUElimPos_x3f___closed__1
|
|||
lean_mark_persistent(l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_getUElimPos_x3f___closed__1);
|
||||
l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_getUElimPos_x3f___closed__2 = _init_l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_getUElimPos_x3f___closed__2();
|
||||
lean_mark_persistent(l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_getUElimPos_x3f___closed__2);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__1 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__1();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__1);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__2 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__2();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__2);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__3 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__3();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__3);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__4 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__4();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__4);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__5 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__5();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__5);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__6 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__6();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986____closed__6);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__1 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__1();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__1);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__2 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__2();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__2);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__3 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__3();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__3);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__4 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__4();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__4);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__5 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__5();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__5);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__6 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__6();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981____closed__6);
|
||||
l_Lean_Meta_Match_bootstrap_genMatcherCode___closed__1 = _init_l_Lean_Meta_Match_bootstrap_genMatcherCode___closed__1();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_bootstrap_genMatcherCode___closed__1);
|
||||
res = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8986_(lean_io_mk_world());
|
||||
res = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_8981_(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
l_Lean_Meta_Match_bootstrap_genMatcherCode = lean_io_result_get_value(res);
|
||||
lean_mark_persistent(l_Lean_Meta_Match_bootstrap_genMatcherCode);
|
||||
lean_dec_ref(res);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__1 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__1();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__1);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__2 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__2();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__2);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__3 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__3();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__3);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__4 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__4();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__4);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__5 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__5();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__5);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__6 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__6();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__6);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__7 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__7();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__7);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__8 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__8();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__8);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__9 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__9();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012____closed__9);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__1 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__1();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__1);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__2 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__2();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__2);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__3 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__3();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__3);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__4 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__4();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__4);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__5 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__5();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__5);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__6 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__6();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__6);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__7 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__7();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__7);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__8 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__8();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__8);
|
||||
l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__9 = _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__9();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007____closed__9);
|
||||
l_Lean_Meta_Match_matcherExt___closed__1 = _init_l_Lean_Meta_Match_matcherExt___closed__1();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_matcherExt___closed__1);
|
||||
l_Lean_Meta_Match_matcherExt___closed__2 = _init_l_Lean_Meta_Match_matcherExt___closed__2();
|
||||
lean_mark_persistent(l_Lean_Meta_Match_matcherExt___closed__2);
|
||||
res = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9012_(lean_io_mk_world());
|
||||
res = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_9007_(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
l_Lean_Meta_Match_matcherExt = lean_io_result_get_value(res);
|
||||
lean_mark_persistent(l_Lean_Meta_Match_matcherExt);
|
||||
|
|
@ -28653,7 +28653,7 @@ l_Lean_Meta_MatcherApp_addArg___lambda__4___closed__3 = _init_l_Lean_Meta_Matche
|
|||
lean_mark_persistent(l_Lean_Meta_MatcherApp_addArg___lambda__4___closed__3);
|
||||
l_Lean_Meta_MatcherApp_addArg___lambda__4___closed__4 = _init_l_Lean_Meta_MatcherApp_addArg___lambda__4___closed__4();
|
||||
lean_mark_persistent(l_Lean_Meta_MatcherApp_addArg___lambda__4___closed__4);
|
||||
res = l_Lean_Meta_initFn____x40_Lean_Meta_Match_Match___hyg_11699_(lean_io_mk_world());
|
||||
res = l_Lean_Meta_initFn____x40_Lean_Meta_Match_Match___hyg_11694_(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
return lean_io_result_mk_ok(lean_box(0));
|
||||
|
|
|
|||
1532
stage0/stdlib/Lean/Server/FileWorker/RequestHandling.c
generated
1532
stage0/stdlib/Lean/Server/FileWorker/RequestHandling.c
generated
File diff suppressed because it is too large
Load diff
|
|
@ -113,10 +113,11 @@ uint8_t lean_usize_dec_lt(size_t, size_t);
|
|||
static lean_object* l___private_Lean_Data_Lsp_Diagnostics_0__Lean_Lsp_toJsonDiagnosticWith____x40_Lean_Data_Lsp_Diagnostics___hyg_883____at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1143____spec__5___closed__5;
|
||||
LEAN_EXPORT lean_object* l_liftExcept___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_246____spec__3(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__14___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_7731____spec__31(lean_object*);
|
||||
lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_7735____spec__31(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1143____spec__1___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_toJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_948_(lean_object*);
|
||||
static lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_246____spec__1___lambda__4___closed__1;
|
||||
lean_object* l_liftExcept___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_7735____spec__29___boxed(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_913____boxed(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_854____spec__1___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instFromJsonRpcEncodingPacket;
|
||||
|
|
@ -169,9 +170,9 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_Inf
|
|||
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___lambda__10(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_246____spec__11___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Widget_getInteractiveDiagnostics___lambda__1(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_7731____spec__28(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_913____spec__1___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__12___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_7735____spec__28(lean_object*);
|
||||
static lean_object* l_Lean_Widget_getInteractiveDiagnostics___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_854____spec__2___boxed__const__1;
|
||||
LEAN_EXPORT lean_object* l_Lean_Widget_getInteractiveDiagnostics___boxed(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -343,9 +344,9 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_initFn____x40_L
|
|||
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_854____spec__2(size_t, size_t, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_246____closed__3;
|
||||
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_854____closed__6;
|
||||
lean_object* l_liftExcept___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_7731____spec__29___boxed(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1143____spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_246____spec__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_liftExcept___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_7735____spec__32___boxed(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___closed__2;
|
||||
LEAN_EXPORT lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_613____lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_246____spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -388,7 +389,6 @@ LEAN_EXPORT lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_i
|
|||
static lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_246____spec__1___lambda__5___closed__1;
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Widget_InteractiveCode_0__Lean_Widget_Lean_Widget_InfoWithCtx_encodeUnsafe____x40_Lean_Widget_InteractiveCode___hyg_5____at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_246____spec__6(lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Server_WithRpcRef_decodeUnsafeAs___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_246____spec__5___rarg___closed__3;
|
||||
lean_object* l_liftExcept___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_7731____spec__32___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Widget_TaggedText_0__Lean_Widget_toJsonTaggedText____x40_Lean_Widget_TaggedText___hyg_578____at___private_Lean_Widget_InteractiveGoal_0__Lean_Widget_Lean_Widget_InteractiveHypothesis_toJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveGoal___hyg_149____spec__1(lean_object*);
|
||||
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__19(lean_object*);
|
||||
|
|
@ -8205,8 +8205,8 @@ lean_inc(x_12);
|
|||
x_13 = lean_ctor_get(x_11, 1);
|
||||
lean_inc(x_13);
|
||||
lean_dec(x_11);
|
||||
x_14 = l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_7731____spec__28(x_3);
|
||||
x_15 = lean_alloc_closure((void*)(l_liftExcept___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_7731____spec__29___boxed), 3, 1);
|
||||
x_14 = l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_7735____spec__28(x_3);
|
||||
x_15 = lean_alloc_closure((void*)(l_liftExcept___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_7735____spec__29___boxed), 3, 1);
|
||||
lean_closure_set(x_15, 0, x_14);
|
||||
x_16 = l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_854____spec__1___lambda__3___closed__1;
|
||||
x_17 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Server_FileWorker_handleDocumentSymbol___spec__2___rarg), 4, 2);
|
||||
|
|
@ -8601,8 +8601,8 @@ lean_inc(x_12);
|
|||
x_13 = lean_ctor_get(x_11, 1);
|
||||
lean_inc(x_13);
|
||||
lean_dec(x_11);
|
||||
x_14 = l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_7731____spec__31(x_3);
|
||||
x_15 = lean_alloc_closure((void*)(l_liftExcept___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_7731____spec__32___boxed), 3, 1);
|
||||
x_14 = l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_7735____spec__31(x_3);
|
||||
x_15 = lean_alloc_closure((void*)(l_liftExcept___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_7735____spec__32___boxed), 3, 1);
|
||||
lean_closure_set(x_15, 0, x_14);
|
||||
x_16 = l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_854____spec__1___lambda__3___closed__1;
|
||||
x_17 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Server_FileWorker_handleDocumentSymbol___spec__2___rarg), 4, 2);
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue