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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2021-04-04 20:32:35 -07:00
parent ba3dd181f5
commit 9f708ece44
6 changed files with 1079 additions and 2379 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
stage0/src/Lean/Elab/Binders.lean generated
View file

@ -374,7 +374,7 @@ private def getMatchAltsNumPatterns (matchAlts : Syntax) : Nat :=
def expandWhereDecls (whereDecls : Syntax) (body : Syntax) : MacroM Syntax :=
match whereDecls with
| `(whereDecls|where $[$decls:letRecDecl $[;]?]*) => `(let rec $decls:letRecDecl,*; $body)
| _ => unreachable!
| _ => Macro.throwUnsupported
def expandWhereDeclsOpt (whereDeclsOpt : Syntax) (body : Syntax) : MacroM Syntax :=
if whereDeclsOpt.isNone then

42
stage0/src/Lean/Server/Completion.lean generated
View file

@ -42,19 +42,22 @@ private partial def consumeImplicitPrefix (e : Expr) : MetaM Expr := do
return e
| _ => return e
private def isTypeApplicable (type : Expr) (expectedType? : Option Expr) : MetaM Bool := do
match expectedType? with
| none => return true
| some expectedType =>
let mut (numArgs, hasMVarHead) ← getExpectedNumArgsAux type
unless hasMVarHead do
let targetTypeNumArgs ← getExpectedNumArgs expectedType
numArgs := numArgs - targetTypeNumArgs
let (newMVars, _, type) ← forallMetaTelescopeReducing type (some numArgs)
-- TODO take coercions into account
-- We use `withReducible` to make sure we don't spend too much time unfolding definitions
-- Alternative: use default and small number of heartbeats
withReducible <| isDefEq type expectedType
private def isTypeApplicable (type : Expr) (expectedType? : Option Expr) : MetaM Bool :=
try
match expectedType? with
| none => return true
| some expectedType =>
let mut (numArgs, hasMVarHead) ← getExpectedNumArgsAux type
unless hasMVarHead do
let targetTypeNumArgs ← getExpectedNumArgs expectedType
numArgs := numArgs - targetTypeNumArgs
let (newMVars, _, type) ← forallMetaTelescopeReducing type (some numArgs)
-- TODO take coercions into account
-- We use `withReducible` to make sure we don't spend too much time unfolding definitions
-- Alternative: use default and small number of heartbeats
withReducible <| isDefEq type expectedType
catch _ =>
return false
private def sortCompletionItems (items : Array CompletionItem) : Array CompletionItem :=
items.qsort fun i1 i2 => i1.label < i2.label
@ -175,10 +178,17 @@ private def idCompletion (ctx : ContextInfo) (lctx : LocalContext) (stx : Syntax
private def dotCompletion (ctx : ContextInfo) (info : TermInfo) (expectedType? : Option Expr) : IO (Option CompletionList) :=
runM ctx info.lctx do
let type ← instantiateMVars (← inferType info.expr)
let name? ←
try
let type ← instantiateMVars (← inferType info.expr)
match type.getAppFn with
| Expr.const name .. => pure (some name)
| _ => pure none
catch _ =>
pure none
-- dbg_trace "dot >> {info.stx}, {info.expr} : {type}, {info.stx.isIdent}"
match type.getAppFn with
| Expr.const name .. =>
match name? with
| some name =>
(← getEnv).constants.forM fun declName c => do
if declName.getPrefix == name then
unless (← isBlackListed c.name) do

341
stage0/stdlib/Lean/Elab/Binders.c generated
View file

@ -23,6 +23,7 @@ extern lean_object* l_myMacro____x40_Init_Notation___hyg_14458____closed__5;
uint8_t l_Lean_Syntax_isAntiquotSuffixSplice(lean_object*);
lean_object* l_Lean_Elab_Term_quoteAutoTactic___closed__6;
lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_getMatchAltsNumPatterns(lean_object*);
lean_object* l_Lean_Elab_Term_expandWhereDecls___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabLetFunDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_elabForall___spec__1___rarg(lean_object*);
size_t l_USize_add(size_t, size_t);
@ -63,7 +64,6 @@ lean_object* l___regBuiltin_Lean_Elab_Term_elabDepArrow___closed__1;
extern lean_object* l_Lean_Parser_Syntax_addPrec___closed__1;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_2278____closed__2;
lean_object* l_Array_append___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_expandWhereDecls___closed__4;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_quoteAutoTactic___spec__3___lambda__1___closed__6;
lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Term_quoteAutoTactic___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_throwUnsupportedSyntax___rarg___closed__1;
@ -219,13 +219,12 @@ lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_addLocalVarInfo(lea
lean_object* l_Lean_Meta_mkLambdaFVars(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_getFunBinderIds_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Syntax_addPrec___closed__5;
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Binders___hyg_5465_(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Binders___hyg_5451_(lean_object*);
lean_object* l_Lean_Elab_Term_quoteAutoTactic___closed__20;
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_20447____closed__2;
lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandBinderModifier___closed__8;
lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_registerFailedToInferBinderTypeInfo(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_setKind(lean_object*, lean_object*);
lean_object* l_instInhabited___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Meta_forallBoundedTelescope___at_Lean_Elab_Term_elabLetDeclAux___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandMatchAltsIntoMatchAux___closed__2;
lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_addLocalVarInfoCore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -256,7 +255,6 @@ lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_myMacro____x40_Init_Nota
extern lean_object* l_Lean_Parser_Term_instBinder___elambda__1___closed__1;
lean_object* l_Lean_Elab_Term_quoteAutoTactic___closed__10;
lean_object* l_Lean_Elab_Term_elabLetDeclCore___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_Lean_Elab_Term_expandWhereDecls___closed__2;
lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_addLocalVarInfo___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabBinder___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_matchBinder___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -275,7 +273,6 @@ lean_object* l___regBuiltin_Lean_Elab_Term_elabForall(lean_object*);
lean_object* l_Lean_Syntax_mkStrLit(lean_object*, lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_13856____closed__12;
extern lean_object* l_Lean_Parser_Term_let__delayed___elambda__1___closed__2;
extern lean_object* l_instMonadEST___closed__1;
lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_elabBindersAux_loop___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_instInhabitedExpr;
lean_object* l_Lean_Elab_Term_quoteAutoTactic___closed__19;
@ -335,7 +332,6 @@ lean_object* l_Lean_Elab_Term_expandFunBinders_loop_match__1___rarg(lean_object*
lean_object* l_Lean_Elab_Term_expandMatchAltsWhereDecls_loop_match__1___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_14458____closed__12;
lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_FunBinders_elabFunBinderViews_match__1(lean_object*);
lean_object* l_Lean_Elab_Term_expandWhereDecls___closed__5;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandMatchAltsIntoMatchAux___spec__2(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_Elab_Term_elabArrow(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Term_quoteAutoTactic___spec__4(lean_object*, lean_object*, lean_object*, lean_object*);
@ -353,7 +349,6 @@ lean_object* l_Lean_Elab_Term_elabFunBinders___rarg___boxed(lean_object*, lean_o
lean_object* l_Lean_Syntax_setArg(lean_object*, lean_object*, lean_object*);
lean_object* lean_environment_main_module(lean_object*);
lean_object* l_Lean_mkFreshId___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_FunBinders_elabFunBinderViews___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_expandWhereDecls___closed__3;
extern lean_object* l_Lean_Expr_getOptParamDefault_x3f___closed__1;
lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_getBinderIds___boxed__const__1;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_matchBinder___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -366,7 +361,6 @@ lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderN
lean_object* l_Lean_Syntax_getArgs(lean_object*);
extern lean_object* l_myMacro____x40_Init_NotationExtra___hyg_5201____closed__6;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandMatchAltsIntoMatchAux___spec__1(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l_instInhabitedReaderT___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getKind(lean_object*);
lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___closed__1;
lean_object* l_Lean_Meta_saveAndResetSynthInstanceCache___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -18614,47 +18608,6 @@ return x_27;
static lean_object* _init_l_Lean_Elab_Term_expandWhereDecls___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_instMonadEST___closed__1;
x_2 = l_Lean_instInhabitedSyntax;
x_3 = l_instInhabited___rarg(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_Term_expandWhereDecls___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_expandWhereDecls___closed__1;
x_2 = lean_alloc_closure((void*)(l_instInhabitedReaderT___rarg___boxed), 2, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Term_expandWhereDecls___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Lean.Elab.Term.expandWhereDecls");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_expandWhereDecls___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Elab_Term_quoteAutoTactic___closed__1;
x_2 = l_Lean_Elab_Term_expandWhereDecls___closed__3;
x_3 = lean_unsigned_to_nat(377u);
x_4 = lean_unsigned_to_nat(9u);
x_5 = l_Lean_Name_getString_x21___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
}
}
static lean_object* _init_l_Lean_Elab_Term_expandWhereDecls___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_myMacro____x40_Init_Notation___hyg_2278____closed__2;
x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Term_expandWhereDecls___lambda__1), 2, 1);
@ -18671,161 +18624,169 @@ lean_inc(x_1);
x_6 = l_Lean_Syntax_isOfKind(x_1, x_5);
if (x_6 == 0)
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
lean_object* x_7; lean_object* x_8;
lean_dec(x_2);
lean_dec(x_1);
x_7 = l_Lean_Elab_Term_expandWhereDecls___closed__2;
x_8 = l_Lean_Elab_Term_expandWhereDecls___closed__4;
x_9 = lean_panic_fn(x_7, x_8);
x_10 = lean_apply_2(x_9, x_3, x_4);
return x_10;
x_7 = lean_box(1);
x_8 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_8, 0, x_7);
lean_ctor_set(x_8, 1, x_4);
return x_8;
}
else
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_11 = lean_unsigned_to_nat(1u);
x_12 = l_Lean_Syntax_getArg(x_1, x_11);
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_9 = lean_unsigned_to_nat(1u);
x_10 = l_Lean_Syntax_getArg(x_1, x_9);
lean_dec(x_1);
x_13 = l_Lean_Syntax_getArgs(x_12);
lean_dec(x_12);
x_14 = l_Lean_Elab_Term_expandWhereDecls___closed__5;
x_15 = l_Array_sequenceMap___at_myMacro____x40_Init_NotationExtra___hyg_5201____spec__1(x_13, x_14);
x_11 = l_Lean_Syntax_getArgs(x_10);
lean_dec(x_10);
x_12 = l_Lean_Elab_Term_expandWhereDecls___closed__1;
x_13 = l_Array_sequenceMap___at_myMacro____x40_Init_NotationExtra___hyg_5201____spec__1(x_11, x_12);
lean_dec(x_11);
if (lean_obj_tag(x_13) == 0)
{
lean_object* x_14; lean_object* x_15;
lean_dec(x_2);
x_14 = lean_box(1);
x_15 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_15, 0, x_14);
lean_ctor_set(x_15, 1, x_4);
return x_15;
}
else
{
lean_object* x_16; lean_object* x_17; uint8_t x_18;
x_16 = lean_ctor_get(x_13, 0);
lean_inc(x_16);
lean_dec(x_13);
if (lean_obj_tag(x_15) == 0)
x_17 = l_Lean_MonadRef_mkInfoFromRefPos___at_myMacro____x40_Init_Notation___hyg_113____spec__1(x_3, x_4);
x_18 = !lean_is_exclusive(x_17);
if (x_18 == 0)
{
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
lean_dec(x_2);
x_16 = l_Lean_Elab_Term_expandWhereDecls___closed__2;
x_17 = l_Lean_Elab_Term_expandWhereDecls___closed__4;
x_18 = lean_panic_fn(x_16, x_17);
x_19 = lean_apply_2(x_18, x_3, x_4);
return x_19;
}
else
{
lean_object* x_20; lean_object* x_21; uint8_t x_22;
x_20 = lean_ctor_get(x_15, 0);
lean_inc(x_20);
lean_dec(x_15);
x_21 = l_Lean_MonadRef_mkInfoFromRefPos___at_myMacro____x40_Init_Notation___hyg_113____spec__1(x_3, x_4);
lean_dec(x_3);
x_22 = !lean_is_exclusive(x_21);
if (x_22 == 0)
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49;
x_23 = lean_ctor_get(x_21, 0);
x_24 = l_myMacro____x40_Init_Notation___hyg_15947____closed__1;
lean_inc(x_23);
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45;
x_19 = lean_ctor_get(x_17, 0);
x_20 = l_myMacro____x40_Init_Notation___hyg_15947____closed__1;
lean_inc(x_19);
x_21 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_21, 0, x_19);
lean_ctor_set(x_21, 1, x_20);
x_22 = l_Array_empty___closed__1;
x_23 = lean_array_push(x_22, x_21);
x_24 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_20447____closed__3;
lean_inc(x_19);
x_25 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_25, 0, x_23);
lean_ctor_set(x_25, 0, x_19);
lean_ctor_set(x_25, 1, x_24);
x_26 = l_Array_empty___closed__1;
x_27 = lean_array_push(x_26, x_25);
x_28 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_20447____closed__3;
lean_inc(x_23);
x_29 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_29, 0, x_23);
lean_ctor_set(x_29, 1, x_28);
x_30 = lean_array_push(x_27, x_29);
x_31 = l_Lean_nullKind___closed__2;
x_32 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_32, 0, x_31);
lean_ctor_set(x_32, 1, x_30);
x_33 = lean_array_push(x_26, x_32);
x_34 = l_myMacro____x40_Init_Notation___hyg_1346____closed__7;
x_35 = l_Lean_Syntax_SepArray_ofElems(x_34, x_20);
lean_dec(x_20);
x_36 = l_Array_appendCore___rarg(x_26, x_35);
lean_dec(x_35);
x_37 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_37, 0, x_31);
lean_ctor_set(x_37, 1, x_36);
x_38 = lean_array_push(x_26, x_37);
x_39 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_20447____closed__1;
x_40 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_40, 0, x_39);
lean_ctor_set(x_40, 1, x_38);
x_41 = lean_array_push(x_33, x_40);
x_42 = l_myMacro____x40_Init_Notation___hyg_15947____closed__12;
x_43 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_43, 0, x_23);
lean_ctor_set(x_43, 1, x_42);
x_44 = lean_array_push(x_26, x_43);
x_26 = lean_array_push(x_23, x_25);
x_27 = l_Lean_nullKind___closed__2;
x_28 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_28, 0, x_27);
lean_ctor_set(x_28, 1, x_26);
x_29 = lean_array_push(x_22, x_28);
x_30 = l_myMacro____x40_Init_Notation___hyg_1346____closed__7;
x_31 = l_Lean_Syntax_SepArray_ofElems(x_30, x_16);
lean_dec(x_16);
x_32 = l_Array_appendCore___rarg(x_22, x_31);
lean_dec(x_31);
x_33 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_33, 0, x_27);
lean_ctor_set(x_33, 1, x_32);
x_34 = lean_array_push(x_22, x_33);
x_35 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_20447____closed__1;
x_36 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_36, 0, x_35);
lean_ctor_set(x_36, 1, x_34);
x_37 = lean_array_push(x_29, x_36);
x_38 = l_myMacro____x40_Init_Notation___hyg_15947____closed__12;
x_39 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_39, 0, x_19);
lean_ctor_set(x_39, 1, x_38);
x_40 = lean_array_push(x_22, x_39);
x_41 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_41, 0, x_27);
lean_ctor_set(x_41, 1, x_40);
x_42 = lean_array_push(x_37, x_41);
x_43 = lean_array_push(x_42, x_2);
x_44 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_20447____closed__2;
x_45 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_45, 0, x_31);
lean_ctor_set(x_45, 1, x_44);
x_46 = lean_array_push(x_41, x_45);
x_47 = lean_array_push(x_46, x_2);
x_48 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_20447____closed__2;
x_49 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_49, 0, x_48);
lean_ctor_set(x_49, 1, x_47);
lean_ctor_set(x_21, 0, x_49);
return x_21;
lean_ctor_set(x_45, 0, x_44);
lean_ctor_set(x_45, 1, x_43);
lean_ctor_set(x_17, 0, x_45);
return x_17;
}
else
{
lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78;
x_50 = lean_ctor_get(x_21, 0);
x_51 = lean_ctor_get(x_21, 1);
lean_inc(x_51);
lean_inc(x_50);
lean_dec(x_21);
x_52 = l_myMacro____x40_Init_Notation___hyg_15947____closed__1;
lean_inc(x_50);
lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74;
x_46 = lean_ctor_get(x_17, 0);
x_47 = lean_ctor_get(x_17, 1);
lean_inc(x_47);
lean_inc(x_46);
lean_dec(x_17);
x_48 = l_myMacro____x40_Init_Notation___hyg_15947____closed__1;
lean_inc(x_46);
x_49 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_49, 0, x_46);
lean_ctor_set(x_49, 1, x_48);
x_50 = l_Array_empty___closed__1;
x_51 = lean_array_push(x_50, x_49);
x_52 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_20447____closed__3;
lean_inc(x_46);
x_53 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_53, 0, x_50);
lean_ctor_set(x_53, 0, x_46);
lean_ctor_set(x_53, 1, x_52);
x_54 = l_Array_empty___closed__1;
x_55 = lean_array_push(x_54, x_53);
x_56 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_20447____closed__3;
lean_inc(x_50);
x_57 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_57, 0, x_50);
lean_ctor_set(x_57, 1, x_56);
x_58 = lean_array_push(x_55, x_57);
x_59 = l_Lean_nullKind___closed__2;
x_60 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_60, 0, x_59);
lean_ctor_set(x_60, 1, x_58);
x_61 = lean_array_push(x_54, x_60);
x_62 = l_myMacro____x40_Init_Notation___hyg_1346____closed__7;
x_63 = l_Lean_Syntax_SepArray_ofElems(x_62, x_20);
lean_dec(x_20);
x_64 = l_Array_appendCore___rarg(x_54, x_63);
lean_dec(x_63);
x_65 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_65, 0, x_59);
lean_ctor_set(x_65, 1, x_64);
x_66 = lean_array_push(x_54, x_65);
x_67 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_20447____closed__1;
x_68 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_68, 0, x_67);
lean_ctor_set(x_68, 1, x_66);
x_69 = lean_array_push(x_61, x_68);
x_70 = l_myMacro____x40_Init_Notation___hyg_15947____closed__12;
x_71 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_71, 0, x_50);
lean_ctor_set(x_71, 1, x_70);
x_72 = lean_array_push(x_54, x_71);
x_54 = lean_array_push(x_51, x_53);
x_55 = l_Lean_nullKind___closed__2;
x_56 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_56, 0, x_55);
lean_ctor_set(x_56, 1, x_54);
x_57 = lean_array_push(x_50, x_56);
x_58 = l_myMacro____x40_Init_Notation___hyg_1346____closed__7;
x_59 = l_Lean_Syntax_SepArray_ofElems(x_58, x_16);
lean_dec(x_16);
x_60 = l_Array_appendCore___rarg(x_50, x_59);
lean_dec(x_59);
x_61 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_61, 0, x_55);
lean_ctor_set(x_61, 1, x_60);
x_62 = lean_array_push(x_50, x_61);
x_63 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_20447____closed__1;
x_64 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_64, 0, x_63);
lean_ctor_set(x_64, 1, x_62);
x_65 = lean_array_push(x_57, x_64);
x_66 = l_myMacro____x40_Init_Notation___hyg_15947____closed__12;
x_67 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_67, 0, x_46);
lean_ctor_set(x_67, 1, x_66);
x_68 = lean_array_push(x_50, x_67);
x_69 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_69, 0, x_55);
lean_ctor_set(x_69, 1, x_68);
x_70 = lean_array_push(x_65, x_69);
x_71 = lean_array_push(x_70, x_2);
x_72 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_20447____closed__2;
x_73 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_73, 0, x_59);
lean_ctor_set(x_73, 1, x_72);
x_74 = lean_array_push(x_69, x_73);
x_75 = lean_array_push(x_74, x_2);
x_76 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_20447____closed__2;
x_77 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_77, 0, x_76);
lean_ctor_set(x_77, 1, x_75);
x_78 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_78, 0, x_77);
lean_ctor_set(x_78, 1, x_51);
return x_78;
lean_ctor_set(x_73, 0, x_72);
lean_ctor_set(x_73, 1, x_71);
x_74 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_74, 0, x_73);
lean_ctor_set(x_74, 1, x_47);
return x_74;
}
}
}
}
}
lean_object* l_Lean_Elab_Term_expandWhereDecls___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_Lean_Elab_Term_expandWhereDecls(x_1, x_2, x_3, x_4);
lean_dec(x_3);
return x_5;
}
}
lean_object* l_Lean_Elab_Term_expandWhereDeclsOpt(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
@ -18842,7 +18803,6 @@ return x_8;
else
{
lean_object* x_9;
lean_dec(x_3);
x_9 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_9, 0, x_2);
lean_ctor_set(x_9, 1, x_4);
@ -18855,6 +18815,7 @@ _start:
{
lean_object* x_5;
x_5 = l_Lean_Elab_Term_expandWhereDeclsOpt(x_1, x_2, x_3, x_4);
lean_dec(x_3);
lean_dec(x_1);
return x_5;
}
@ -20311,6 +20272,7 @@ if (x_173 == 0)
lean_object* x_174;
lean_free_object(x_144);
x_174 = l_Lean_Elab_Term_expandWhereDeclsOpt(x_2, x_172, x_5, x_147);
lean_dec(x_5);
return x_174;
}
else
@ -20370,6 +20332,7 @@ if (x_202 == 0)
{
lean_object* x_203;
x_203 = l_Lean_Elab_Term_expandWhereDeclsOpt(x_2, x_201, x_5, x_176);
lean_dec(x_5);
return x_203;
}
else
@ -22793,7 +22756,7 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Binders___hyg_5465_(lean_object* x_1) {
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Binders___hyg_5451_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -22962,14 +22925,6 @@ l_Lean_Elab_Term_FunBinders_State_expectedType_x3f___default = _init_l_Lean_Elab
lean_mark_persistent(l_Lean_Elab_Term_FunBinders_State_expectedType_x3f___default);
l_Lean_Elab_Term_expandWhereDecls___closed__1 = _init_l_Lean_Elab_Term_expandWhereDecls___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_expandWhereDecls___closed__1);
l_Lean_Elab_Term_expandWhereDecls___closed__2 = _init_l_Lean_Elab_Term_expandWhereDecls___closed__2();
lean_mark_persistent(l_Lean_Elab_Term_expandWhereDecls___closed__2);
l_Lean_Elab_Term_expandWhereDecls___closed__3 = _init_l_Lean_Elab_Term_expandWhereDecls___closed__3();
lean_mark_persistent(l_Lean_Elab_Term_expandWhereDecls___closed__3);
l_Lean_Elab_Term_expandWhereDecls___closed__4 = _init_l_Lean_Elab_Term_expandWhereDecls___closed__4();
lean_mark_persistent(l_Lean_Elab_Term_expandWhereDecls___closed__4);
l_Lean_Elab_Term_expandWhereDecls___closed__5 = _init_l_Lean_Elab_Term_expandWhereDecls___closed__5();
lean_mark_persistent(l_Lean_Elab_Term_expandWhereDecls___closed__5);
l___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandMatchAltsIntoMatchAux___closed__1 = _init_l___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandMatchAltsIntoMatchAux___closed__1();
lean_mark_persistent(l___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandMatchAltsIntoMatchAux___closed__1);
l___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandMatchAltsIntoMatchAux___closed__2 = _init_l___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandMatchAltsIntoMatchAux___closed__2();
@ -23014,7 +22969,7 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabLetDelayedDecl___closed__
res = l___regBuiltin_Lean_Elab_Term_elabLetDelayedDecl(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_Binders___hyg_5465_(lean_io_mk_world());
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Binders___hyg_5451_(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));

117
stage0/stdlib/Lean/Elab/Do.c generated
View file

@ -20,6 +20,7 @@ lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_mkForInBody(lean_object*);
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__10___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_ToTerm_breakToTerm___closed__8;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__11___closed__3;
lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__6;
lean_object* l_Lean_Elab_Term_Do_ToTerm_breakToTerm___closed__4;
lean_object* l_Lean_Elab_Term_Do_mkSeq(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_ToTerm_continueToTerm___closed__35;
@ -343,6 +344,7 @@ extern lean_object* l_myMacro____x40_Init_Notation___hyg_12513____closed__9;
extern lean_object* l_Lean_Meta_Closure_mkNewLevelParam___closed__1;
lean_object* l_Lean_Elab_Term_Do_getPatternVarNames(lean_object*);
lean_object* l_Lean_Elab_Term_Do_ToTerm_returnToTerm___closed__15;
lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__7;
lean_object* l_Lean_Elab_Term_Do_ToTerm_returnToTerm___closed__3;
extern lean_object* l_Lean_Json_Parser_anyCore___rarg___closed__6;
lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Term_Do_ToCodeBlock_doUnlessToCode___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -587,7 +589,6 @@ lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_myMacro____x40_Init_Nota
lean_object* l_Lean_Elab_Term_Do_ToTerm_breakToTerm___closed__6;
lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_getTryCatchUpdatedVars(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_anyMUnsafe_any___at_Lean_Elab_Term_Do_hasBreakContinue___spec__2___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Term_expandWhereDecls___closed__2;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2925____spec__2(lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_tryCatchPred___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doForToCode___closed__11;
@ -21878,12 +21879,32 @@ return x_6;
static lean_object* _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_instMonadEST___closed__1;
x_2 = l_Lean_instInhabitedSyntax;
x_3 = l_instInhabited___rarg(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__1;
x_2 = lean_alloc_closure((void*)(l_instInhabitedReaderT___rarg___boxed), 2, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Lean.Elab.Do");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__2() {
static lean_object* _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__4() {
_start:
{
lean_object* x_1;
@ -21891,12 +21912,12 @@ x_1 = lean_mk_string("_private.Lean.Elab.Do.0.Lean.Elab.Term.Do.destructTuple.de
return x_1;
}
}
static lean_object* _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3() {
static lean_object* _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__1;
x_2 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__2;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3;
x_2 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__4;
x_3 = lean_unsigned_to_nat(718u);
x_4 = lean_unsigned_to_nat(13u);
x_5 = l_Lean_Name_getString_x21___closed__3;
@ -21904,7 +21925,7 @@ x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
}
}
static lean_object* _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__4() {
static lean_object* _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__6() {
_start:
{
lean_object* x_1;
@ -21912,7 +21933,7 @@ x_1 = lean_mk_string("1");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__5() {
static lean_object* _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__7() {
_start:
{
lean_object* x_1;
@ -21928,8 +21949,8 @@ if (lean_obj_tag(x_1) == 0)
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
lean_dec(x_3);
lean_dec(x_2);
x_6 = l_Lean_Elab_Term_expandWhereDecls___closed__2;
x_7 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3;
x_6 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__2;
x_7 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__5;
x_8 = lean_panic_fn(x_6, x_7);
x_9 = lean_apply_2(x_8, x_4, x_5);
return x_9;
@ -22021,7 +22042,7 @@ x_47 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_47, 0, x_33);
lean_ctor_set(x_47, 1, x_46);
x_48 = lean_array_push(x_45, x_47);
x_49 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__4;
x_49 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__6;
lean_inc(x_33);
x_50 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_50, 0, x_33);
@ -22071,7 +22092,7 @@ x_71 = lean_array_push(x_36, x_70);
x_72 = lean_array_push(x_71, x_39);
x_73 = lean_array_push(x_72, x_39);
x_74 = lean_array_push(x_73, x_43);
x_75 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__5;
x_75 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__7;
x_76 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_76, 0, x_33);
lean_ctor_set(x_76, 1, x_75);
@ -22138,7 +22159,7 @@ x_107 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_107, 0, x_92);
lean_ctor_set(x_107, 1, x_106);
x_108 = lean_array_push(x_105, x_107);
x_109 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__4;
x_109 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__6;
lean_inc(x_92);
x_110 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_110, 0, x_92);
@ -22188,7 +22209,7 @@ x_131 = lean_array_push(x_96, x_130);
x_132 = lean_array_push(x_131, x_99);
x_133 = lean_array_push(x_132, x_99);
x_134 = lean_array_push(x_133, x_103);
x_135 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__5;
x_135 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__7;
x_136 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_136, 0, x_92);
lean_ctor_set(x_136, 1, x_135);
@ -22346,7 +22367,7 @@ x_194 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_194, 0, x_178);
lean_ctor_set(x_194, 1, x_193);
x_195 = lean_array_push(x_192, x_194);
x_196 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__4;
x_196 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__6;
lean_inc(x_178);
x_197 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_197, 0, x_178);
@ -22396,7 +22417,7 @@ x_218 = lean_array_push(x_183, x_217);
x_219 = lean_array_push(x_218, x_186);
x_220 = lean_array_push(x_219, x_186);
x_221 = lean_array_push(x_220, x_190);
x_222 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__5;
x_222 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__7;
x_223 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_223, 0, x_178);
lean_ctor_set(x_223, 1, x_222);
@ -22524,7 +22545,7 @@ x_269 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_269, 0, x_255);
lean_ctor_set(x_269, 1, x_268);
x_270 = lean_array_push(x_267, x_269);
x_271 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__4;
x_271 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__6;
lean_inc(x_255);
x_272 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_272, 0, x_255);
@ -22568,7 +22589,7 @@ x_292 = lean_array_push(x_258, x_251);
x_293 = lean_array_push(x_292, x_261);
x_294 = lean_array_push(x_293, x_261);
x_295 = lean_array_push(x_294, x_265);
x_296 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__5;
x_296 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__7;
x_297 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_297, 0, x_255);
lean_ctor_set(x_297, 1, x_296);
@ -22635,7 +22656,7 @@ x_328 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_328, 0, x_313);
lean_ctor_set(x_328, 1, x_327);
x_329 = lean_array_push(x_326, x_328);
x_330 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__4;
x_330 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__6;
lean_inc(x_313);
x_331 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_331, 0, x_313);
@ -22679,7 +22700,7 @@ x_351 = lean_array_push(x_317, x_251);
x_352 = lean_array_push(x_351, x_320);
x_353 = lean_array_push(x_352, x_320);
x_354 = lean_array_push(x_353, x_324);
x_355 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__5;
x_355 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__7;
x_356 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_356, 0, x_313);
lean_ctor_set(x_356, 1, x_355);
@ -22799,7 +22820,7 @@ x_409 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_409, 0, x_395);
lean_ctor_set(x_409, 1, x_408);
x_410 = lean_array_push(x_407, x_409);
x_411 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__4;
x_411 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__6;
lean_inc(x_395);
x_412 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_412, 0, x_395);
@ -22849,7 +22870,7 @@ x_433 = lean_array_push(x_398, x_432);
x_434 = lean_array_push(x_433, x_401);
x_435 = lean_array_push(x_434, x_401);
x_436 = lean_array_push(x_435, x_405);
x_437 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__5;
x_437 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__7;
x_438 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_438, 0, x_395);
lean_ctor_set(x_438, 1, x_437);
@ -22916,7 +22937,7 @@ x_469 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_469, 0, x_454);
lean_ctor_set(x_469, 1, x_468);
x_470 = lean_array_push(x_467, x_469);
x_471 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__4;
x_471 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__6;
lean_inc(x_454);
x_472 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_472, 0, x_454);
@ -22966,7 +22987,7 @@ x_493 = lean_array_push(x_458, x_492);
x_494 = lean_array_push(x_493, x_461);
x_495 = lean_array_push(x_494, x_461);
x_496 = lean_array_push(x_495, x_465);
x_497 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__5;
x_497 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__7;
x_498 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_498, 0, x_454);
lean_ctor_set(x_498, 1, x_497);
@ -23124,7 +23145,7 @@ x_556 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_556, 0, x_540);
lean_ctor_set(x_556, 1, x_555);
x_557 = lean_array_push(x_554, x_556);
x_558 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__4;
x_558 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__6;
lean_inc(x_540);
x_559 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_559, 0, x_540);
@ -23174,7 +23195,7 @@ x_580 = lean_array_push(x_545, x_579);
x_581 = lean_array_push(x_580, x_548);
x_582 = lean_array_push(x_581, x_548);
x_583 = lean_array_push(x_582, x_552);
x_584 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__5;
x_584 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__7;
x_585 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_585, 0, x_540);
lean_ctor_set(x_585, 1, x_584);
@ -23937,7 +23958,7 @@ static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_returnToTerm___closed__16()
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_expandWhereDecls___closed__2;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__2;
x_2 = lean_alloc_closure((void*)(l_instInhabitedReaderT___rarg___boxed), 2, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
@ -23955,7 +23976,7 @@ static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_returnToTerm___closed__18()
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__1;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3;
x_2 = l_Lean_Elab_Term_Do_ToTerm_returnToTerm___closed__17;
x_3 = lean_unsigned_to_nat(837u);
x_4 = lean_unsigned_to_nat(28u);
@ -25567,7 +25588,7 @@ static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_continueToTerm___closed__2(
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__1;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3;
x_2 = l_Lean_Elab_Term_Do_ToTerm_continueToTerm___closed__1;
x_3 = lean_unsigned_to_nat(846u);
x_4 = lean_unsigned_to_nat(28u);
@ -25793,7 +25814,7 @@ static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_continueToTerm___closed__23
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__1;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3;
x_2 = l_Lean_Elab_Term_Do_ToTerm_continueToTerm___closed__1;
x_3 = lean_unsigned_to_nat(850u);
x_4 = lean_unsigned_to_nat(28u);
@ -26960,7 +26981,7 @@ static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_breakToTerm___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__1;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3;
x_2 = l_Lean_Elab_Term_Do_ToTerm_breakToTerm___closed__1;
x_3 = lean_unsigned_to_nat(858u);
x_4 = lean_unsigned_to_nat(28u);
@ -27038,7 +27059,7 @@ static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_breakToTerm___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__1;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3;
x_2 = l_Lean_Elab_Term_Do_ToTerm_breakToTerm___closed__1;
x_3 = lean_unsigned_to_nat(862u);
x_4 = lean_unsigned_to_nat(28u);
@ -28253,7 +28274,7 @@ static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___clos
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__1;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3;
x_2 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__5;
x_3 = lean_unsigned_to_nat(873u);
x_4 = lean_unsigned_to_nat(28u);
@ -36894,7 +36915,7 @@ static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_mkNestedKind___closed__2()
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__1;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3;
x_2 = l_Lean_Elab_Term_Do_ToTerm_mkNestedKind___closed__1;
x_3 = lean_unsigned_to_nat(1020u);
x_4 = lean_unsigned_to_nat(27u);
@ -37087,7 +37108,7 @@ static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___clo
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__1;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__3;
x_2 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__3;
x_3 = lean_unsigned_to_nat(1076u);
x_4 = lean_unsigned_to_nat(27u);
@ -37962,7 +37983,7 @@ x_401 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_401, 0, x_353);
lean_ctor_set(x_401, 1, x_400);
x_402 = lean_array_push(x_370, x_401);
x_403 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__5;
x_403 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__7;
lean_inc(x_353);
x_404 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_404, 0, x_353);
@ -38000,7 +38021,7 @@ x_422 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_422, 0, x_353);
lean_ctor_set(x_422, 1, x_421);
x_423 = lean_array_push(x_358, x_422);
x_424 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__4;
x_424 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__6;
x_425 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_425, 0, x_353);
lean_ctor_set(x_425, 1, x_424);
@ -38142,7 +38163,7 @@ x_498 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_498, 0, x_449);
lean_ctor_set(x_498, 1, x_497);
x_499 = lean_array_push(x_467, x_498);
x_500 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__5;
x_500 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__7;
lean_inc(x_449);
x_501 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_501, 0, x_449);
@ -38180,7 +38201,7 @@ x_519 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_519, 0, x_449);
lean_ctor_set(x_519, 1, x_518);
x_520 = lean_array_push(x_455, x_519);
x_521 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__4;
x_521 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__6;
x_522 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_522, 0, x_449);
lean_ctor_set(x_522, 1, x_521);
@ -39352,7 +39373,7 @@ x_1124 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_1124, 0, x_1076);
lean_ctor_set(x_1124, 1, x_1123);
x_1125 = lean_array_push(x_1093, x_1124);
x_1126 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__5;
x_1126 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__7;
lean_inc(x_1076);
x_1127 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_1127, 0, x_1076);
@ -39395,7 +39416,7 @@ lean_ctor_set(x_1148, 1, x_1146);
lean_ctor_set(x_1148, 2, x_1145);
lean_ctor_set(x_1148, 3, x_1147);
x_1149 = lean_array_push(x_1081, x_1148);
x_1150 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__4;
x_1150 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__6;
x_1151 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_1151, 0, x_1076);
lean_ctor_set(x_1151, 1, x_1150);
@ -39543,7 +39564,7 @@ x_1226 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_1226, 0, x_1177);
lean_ctor_set(x_1226, 1, x_1225);
x_1227 = lean_array_push(x_1195, x_1226);
x_1228 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__5;
x_1228 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__7;
lean_inc(x_1177);
x_1229 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_1229, 0, x_1177);
@ -39586,7 +39607,7 @@ lean_ctor_set(x_1250, 1, x_1248);
lean_ctor_set(x_1250, 2, x_1247);
lean_ctor_set(x_1250, 3, x_1249);
x_1251 = lean_array_push(x_1183, x_1250);
x_1252 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__4;
x_1252 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__6;
x_1253 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_1253, 0, x_1177);
lean_ctor_set(x_1253, 1, x_1252);
@ -55097,7 +55118,7 @@ x_416 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_416, 0, x_349);
lean_ctor_set(x_416, 1, x_415);
x_417 = lean_array_push(x_409, x_416);
x_418 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__5;
x_418 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__7;
lean_inc(x_349);
x_419 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_419, 0, x_349);
@ -55279,7 +55300,7 @@ x_512 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_512, 0, x_451);
lean_ctor_set(x_512, 1, x_511);
x_513 = lean_array_push(x_359, x_512);
x_514 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__4;
x_514 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__6;
lean_inc(x_451);
x_515 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_515, 0, x_451);
@ -56856,7 +56877,7 @@ x_1156 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_1156, 0, x_1089);
lean_ctor_set(x_1156, 1, x_1155);
x_1157 = lean_array_push(x_1149, x_1156);
x_1158 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__5;
x_1158 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__7;
lean_inc(x_1089);
x_1159 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_1159, 0, x_1089);
@ -57038,7 +57059,7 @@ x_1252 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_1252, 0, x_1191);
lean_ctor_set(x_1252, 1, x_1251);
x_1253 = lean_array_push(x_1099, x_1252);
x_1254 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__4;
x_1254 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__6;
lean_inc(x_1191);
x_1255 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_1255, 0, x_1191);
@ -64425,6 +64446,10 @@ l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__4
lean_mark_persistent(l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__4);
l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__5 = _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__5();
lean_mark_persistent(l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__5);
l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__6 = _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__6();
lean_mark_persistent(l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__6);
l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__7 = _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__7();
lean_mark_persistent(l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_destructTuple_destruct___closed__7);
l_Lean_Elab_Term_Do_ToTerm_instInhabitedKind = _init_l_Lean_Elab_Term_Do_ToTerm_instInhabitedKind();
l_Lean_Elab_Term_Do_ToTerm_mkUVarTuple___boxed__const__1 = _init_l_Lean_Elab_Term_Do_ToTerm_mkUVarTuple___boxed__const__1();
lean_mark_persistent(l_Lean_Elab_Term_Do_ToTerm_mkUVarTuple___boxed__const__1);

41
stage0/stdlib/Lean/Elab/MutualDef.c generated
View file

@ -29,6 +29,7 @@ lean_object* l_Lean_Elab_Term_MutualClosure_FixPoint_run_match__1(lean_object*);
extern lean_object* l_Lean_Parser_Command_protected___elambda__1___closed__1;
extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1139____closed__33;
lean_object* lean_erase_macro_scopes(lean_object*);
extern lean_object* l_Lean_Elab_Term_expandWhereDecls___closed__1;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___spec__2___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_forallBoundedTelescope___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabFunValues___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_1346____closed__7;
@ -352,7 +353,6 @@ lean_object* l_List_foldl___at_Lean_Elab_Term_MutualClosure_pushLetRecs___spec__
lean_object* l_Lean_Elab_Term_synthesizeSyntheticMVars_loop(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_foldAux___at_Lean_Elab_Term_MutualClosure_insertReplacementForMainFns___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_levelMVarToParamHeaders_process___spec__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*);
extern lean_object* l_Lean_Elab_Term_expandWhereDecls___closed__2;
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_check___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* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkClosureForAux___closed__3;
lean_object* l_List_map___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkFreeVarMap___spec__1(lean_object*);
@ -398,6 +398,7 @@ extern lean_object* l_Lean_KernelException_toMessageData___closed__15;
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_getFunName___lambda__1___boxed(lean_object*, lean_object*);
extern lean_object* l_Lean_instInhabitedSyntax;
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_FixPoint_fixpoint_match__1___rarg(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___closed__2;
uint8_t l_Array_anyMUnsafe_any___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_isTheorem___spec__1(lean_object*, size_t, size_t);
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_FixPoint_resetModified(lean_object*);
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkClosureFor_match__1(lean_object*);
@ -470,7 +471,6 @@ lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkL
lean_object* l_Lean_Syntax_getPos_x3f(lean_object*, uint8_t);
lean_object* l_Lean_Meta_assignExprMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders_match__2(lean_object*);
extern lean_object* l_Lean_Elab_Term_expandWhereDecls___closed__5;
extern lean_object* l_Option_get_x21___rarg___closed__4;
lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_checkLetRecsToLiftTypes___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
size_t lean_ptr_addr(lean_object*);
@ -493,6 +493,7 @@ lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_MutualDef_0__Lea
extern lean_object* l_Lean_Elab_mkDeclName___rarg___lambda__1___closed__2;
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_levelMVarToParamHeaders_process(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_forM___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_collectUsed___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___closed__3;
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_pickMaxFVar_x3f___boxed(lean_object*, lean_object*);
lean_object* l_Lean_mkHole(lean_object*);
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_checkModifiers___closed__2;
@ -6212,6 +6213,26 @@ goto _start;
static lean_object* _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_instMonadEST___closed__1;
x_2 = l_Lean_instInhabitedSyntax;
x_3 = l_instInhabited___rarg(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___closed__1;
x_2 = lean_alloc_closure((void*)(l_instInhabitedReaderT___rarg___boxed), 2, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___spec__1___lambda__1___closed__1;
x_2 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___spec__1___lambda__1___closed__2;
@ -6242,8 +6263,8 @@ if (x_5 == 0)
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
lean_dec(x_1);
x_6 = l_Lean_Elab_Term_expandWhereDecls___closed__2;
x_7 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___closed__1;
x_6 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___closed__2;
x_7 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___closed__3;
x_8 = lean_panic_fn(x_6, x_7);
x_9 = lean_apply_2(x_8, x_2, x_3);
return x_9;
@ -6256,14 +6277,14 @@ x_11 = l_Lean_Syntax_getArg(x_1, x_10);
lean_dec(x_1);
x_12 = l_Lean_Syntax_getArgs(x_11);
lean_dec(x_11);
x_13 = l_Lean_Elab_Term_expandWhereDecls___closed__5;
x_13 = l_Lean_Elab_Term_expandWhereDecls___closed__1;
x_14 = l_Array_sequenceMap___at_myMacro____x40_Init_NotationExtra___hyg_5201____spec__1(x_12, x_13);
lean_dec(x_12);
if (lean_obj_tag(x_14) == 0)
{
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18;
x_15 = l_Lean_Elab_Term_expandWhereDecls___closed__2;
x_16 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___closed__1;
x_15 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___closed__2;
x_16 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___closed__3;
x_17 = lean_panic_fn(x_15, x_16);
x_18 = lean_apply_2(x_17, x_2, x_3);
return x_18;
@ -6659,6 +6680,7 @@ x_24 = lean_unsigned_to_nat(1u);
x_25 = l_Lean_Syntax_getArg(x_1, x_24);
lean_dec(x_1);
x_26 = l_Lean_Elab_Term_expandWhereDeclsOpt(x_23, x_25, x_2, x_3);
lean_dec(x_2);
lean_dec(x_23);
return x_26;
}
@ -6748,6 +6770,7 @@ x_50 = lean_unsigned_to_nat(1u);
x_51 = l_Lean_Syntax_getArg(x_1, x_50);
lean_dec(x_1);
x_52 = l_Lean_Elab_Term_expandWhereDeclsOpt(x_49, x_51, x_34, x_3);
lean_dec(x_34);
lean_dec(x_49);
return x_52;
}
@ -21153,6 +21176,10 @@ l_Array_mapMUnsafe_map___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expa
lean_mark_persistent(l_Array_mapMUnsafe_map___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___spec__2___lambda__3___closed__1);
l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___closed__1 = _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___closed__1();
lean_mark_persistent(l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___closed__1);
l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___closed__2 = _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___closed__2();
lean_mark_persistent(l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___closed__2);
l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___closed__3 = _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___closed__3();
lean_mark_persistent(l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___closed__3);
l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___boxed__const__1 = _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___boxed__const__1();
lean_mark_persistent(l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___boxed__const__1);
l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_declValToTerm___closed__1 = _init_l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_declValToTerm___closed__1();

2915
stage0/stdlib/Lean/Server/Completion.c generated
View file

File diff suppressed because it is too large Load diff