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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-02-09 16:29:04 -08:00
parent 164cd4395a
commit 0d36820bc5
11 changed files with 11495 additions and 31235 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
stage0/src/Init/Lean/Meta/Tactic/Clear.lean
View file

@ -19,10 +19,10 @@ withMVarContext mvarId $ do
mctx ← getMCtx;
lctx.forM $ fun localDecl =>
unless (localDecl.fvarId == fvarId) $
when (mctx.localDeclDependsOn (fun fvarId' => fvarId' == fvarId) localDecl) $
when (mctx.localDeclDependsOn localDecl fvarId) $
throwTacticEx `clear mvarId ("hypothesis '" ++ localDecl.value ++ "' depends on '" ++ mkFVar fvarId ++ "'");
mvarDecl ← getMVarDecl mvarId;
when (mctx.exprDependsOn (fun fvarId' => fvarId' == fvarId) mvarDecl.type) $
when (mctx.exprDependsOn mvarDecl.type fvarId) $
throwTacticEx `clear mvarId ("taget depends on '" ++ mkFVar fvarId ++ "'");
let lctx := lctx.erase fvarId;
localInsts ← getLocalInstances;

19
stage0/src/Init/Lean/MetavarContext.lean
View file

@ -624,16 +624,23 @@ end DependsOn
1- If `?m := t`, then we visit `t` looking for `x`
2- If `?m` is unassigned, then we consider the worst case and check whether `x` is in the local context of `?m`.
This case is a "may dependency". That is, we may assign a term `t` to `?m` s.t. `t` contains `x`. -/
@[inline] def exprDependsOn (mctx : MetavarContext) (p : FVarId → Bool) (e : Expr) : Bool :=
@[inline] def findExprDependsOn (mctx : MetavarContext) (e : Expr) (p : FVarId → Bool) : Bool :=
(DependsOn.main mctx p e).run' {}
/--
Similar to `exprDependsOn`, but checks the expressions in the given local declaration
depends on a free variable `x` s.t. `p x` is `true`. -/
@[inline] def localDeclDependsOn (mctx : MetavarContext) (p : FVarId → Bool) : LocalDecl → Bool
| LocalDecl.cdecl _ _ _ type _ => exprDependsOn mctx p type
@[inline] def findLocalDeclDependsOn (mctx : MetavarContext) (localDecl : LocalDecl) (p : FVarId → Bool) : Bool :=
match localDecl with
| LocalDecl.cdecl _ _ _ type _ => findExprDependsOn mctx type p
| LocalDecl.ldecl _ _ _ type value => (DependsOn.main mctx p type <||> DependsOn.main mctx p value).run' {}
def exprDependsOn (mctx : MetavarContext) (e : Expr) (fvarId : FVarId) : Bool :=
findExprDependsOn mctx e $ fun fvarId' => fvarId == fvarId'
def localDeclDependsOn (mctx : MetavarContext) (localDecl : LocalDecl) (fvarId : FVarId) : Bool :=
findLocalDeclDependsOn mctx localDecl $ fun fvarId' => fvarId == fvarId'
namespace MkBinding
inductive Exception
@ -695,7 +702,7 @@ else do
i.forM $ fun j =>
let prevFVar := toRevert.get! j;
let prevDecl := lctx.getFVar! prevFVar;
when (localDeclDependsOn mctx (fun fvarId => fvarId == fvar.fvarId!) prevDecl) $
when (localDeclDependsOn mctx prevDecl fvar.fvarId!) $
throw (Exception.revertFailure mctx lctx toRevert prevDecl)
};
let newToRevert := if preserveOrder then toRevert else Array.mkEmpty toRevert.size;
@ -706,7 +713,7 @@ else do
if skipFirst && decl.index == firstDeclToVisit.index then pure newToRevert
else if toRevert.any (fun x => decl.fvarId == x.fvarId!) then
pure (newToRevert.push decl.toExpr)
else if localDeclDependsOn mctx (fun fvarId => newToRevert.any $ fun x => x.fvarId! == fvarId) decl then
else if findLocalDeclDependsOn mctx decl (fun fvarId => newToRevert.any $ fun x => x.fvarId! == fvarId) then
if decl.binderInfo.isAuxDecl then
throw (Exception.revertFailure mctx lctx toRevert decl)
else
@ -791,7 +798,7 @@ pure mvarId
/-- Return true iff some `e` in `es` depends on `fvarId` -/
private def anyDependsOn (mctx : MetavarContext) (es : Array Expr) (fvarId : FVarId) : Bool :=
es.any $ fun e => exprDependsOn mctx (fun fvarId' => fvarId == fvarId') e
es.any $ fun e => exprDependsOn mctx e fvarId
private partial def elimMVarDepsApp (elimMVarDepsAux : Expr → M Expr) (xs : Array Expr) : Expr → Array Expr → M Expr
| f, args =>

32
stage0/stdlib/Init/Lean/Elab/App.c
View file

@ -116,6 +116,7 @@ lean_object* l___private_Init_Lean_Elab_App_12__throwLValError___rarg(lean_objec
lean_object* l_Lean_Elab_Term_getOptions(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_App_9__propagateExpectedType(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_mkTermIdFromIdent___closed__2;
extern lean_object* l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
extern lean_object* l_Lean_Parser_Term_proj___elambda__1___closed__2;
lean_object* l___private_Init_Lean_Elab_App_17__addLValArg___main___closed__9;
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_App_26__expandApp___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -266,7 +267,6 @@ lean_object* l_Lean_mkLevelSucc(lean_object*);
lean_object* l___private_Init_Lean_Elab_App_13__resolveLValAux___closed__9;
lean_object* l_Lean_Elab_Term_getLCtx(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_App_13__resolveLValAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
lean_object* l_Lean_Elab_Term_elabSortApp(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkApp(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_App_13__resolveLValAux___closed__27;
@ -5767,7 +5767,7 @@ lean_ctor_set(x_82, 0, x_65);
x_83 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_83, 0, x_81);
lean_ctor_set(x_83, 1, x_82);
x_84 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
x_84 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
x_85 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_85, 0, x_83);
lean_ctor_set(x_85, 1, x_84);
@ -5826,7 +5826,7 @@ lean_ctor_set(x_99, 0, x_65);
x_100 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_100, 0, x_98);
lean_ctor_set(x_100, 1, x_99);
x_101 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
x_101 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
x_102 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_102, 0, x_100);
lean_ctor_set(x_102, 1, x_101);
@ -5902,7 +5902,7 @@ lean_ctor_set(x_117, 0, x_65);
x_118 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_118, 0, x_116);
lean_ctor_set(x_118, 1, x_117);
x_119 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
x_119 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
x_120 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_120, 0, x_118);
lean_ctor_set(x_120, 1, x_119);
@ -5962,7 +5962,7 @@ lean_ctor_set(x_135, 0, x_65);
x_136 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_136, 0, x_134);
lean_ctor_set(x_136, 1, x_135);
x_137 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
x_137 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
x_138 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_138, 0, x_136);
lean_ctor_set(x_138, 1, x_137);
@ -6066,7 +6066,7 @@ lean_ctor_set(x_165, 0, x_148);
x_166 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_166, 0, x_164);
lean_ctor_set(x_166, 1, x_165);
x_167 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
x_167 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
x_168 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_168, 0, x_166);
lean_ctor_set(x_168, 1, x_167);
@ -6125,7 +6125,7 @@ lean_ctor_set(x_182, 0, x_148);
x_183 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_183, 0, x_181);
lean_ctor_set(x_183, 1, x_182);
x_184 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
x_184 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
x_185 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_185, 0, x_183);
lean_ctor_set(x_185, 1, x_184);
@ -6201,7 +6201,7 @@ lean_ctor_set(x_200, 0, x_148);
x_201 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_201, 0, x_199);
lean_ctor_set(x_201, 1, x_200);
x_202 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
x_202 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
x_203 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_203, 0, x_201);
lean_ctor_set(x_203, 1, x_202);
@ -6261,7 +6261,7 @@ lean_ctor_set(x_218, 0, x_148);
x_219 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_219, 0, x_217);
lean_ctor_set(x_219, 1, x_218);
x_220 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
x_220 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
x_221 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_221, 0, x_219);
lean_ctor_set(x_221, 1, x_220);
@ -6395,7 +6395,7 @@ lean_ctor_set(x_252, 0, x_235);
x_253 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_253, 0, x_251);
lean_ctor_set(x_253, 1, x_252);
x_254 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
x_254 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
x_255 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_255, 0, x_253);
lean_ctor_set(x_255, 1, x_254);
@ -6460,7 +6460,7 @@ lean_ctor_set(x_270, 0, x_235);
x_271 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_271, 0, x_269);
lean_ctor_set(x_271, 1, x_270);
x_272 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
x_272 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
x_273 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_273, 0, x_271);
lean_ctor_set(x_273, 1, x_272);
@ -6576,7 +6576,7 @@ lean_ctor_set(x_300, 0, x_283);
x_301 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_301, 0, x_299);
lean_ctor_set(x_301, 1, x_300);
x_302 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
x_302 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
x_303 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_303, 0, x_301);
lean_ctor_set(x_303, 1, x_302);
@ -6641,7 +6641,7 @@ lean_ctor_set(x_318, 0, x_283);
x_319 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_319, 0, x_317);
lean_ctor_set(x_319, 1, x_318);
x_320 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
x_320 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
x_321 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_321, 0, x_319);
lean_ctor_set(x_321, 1, x_320);
@ -6748,7 +6748,7 @@ x_341 = l___private_Init_Lean_Elab_App_13__resolveLValAux___closed__28;
x_342 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_342, 0, x_341);
lean_ctor_set(x_342, 1, x_340);
x_343 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
x_343 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
x_344 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_344, 0, x_342);
lean_ctor_set(x_344, 1, x_343);
@ -6791,7 +6791,7 @@ x_353 = l___private_Init_Lean_Elab_App_13__resolveLValAux___closed__28;
x_354 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_354, 0, x_353);
lean_ctor_set(x_354, 1, x_352);
x_355 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
x_355 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
x_356 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_356, 0, x_354);
lean_ctor_set(x_356, 1, x_355);
@ -7644,7 +7644,7 @@ x_37 = l___private_Init_Lean_Elab_App_17__addLValArg___main___closed__12;
x_38 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_38, 0, x_37);
lean_ctor_set(x_38, 1, x_36);
x_39 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
x_39 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
x_40 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_40, 0, x_38);
lean_ctor_set(x_40, 1, x_39);

4
stage0/stdlib/Init/Lean/Elab/Command.c
View file

@ -176,6 +176,7 @@ lean_object* l_Lean_Elab_Command_declareBuiltinCommandElab(lean_object*, lean_ob
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabUniverses___closed__1;
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Command_elabOpenOnly___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_Lean_Elab_MonadMacroAdapter___closed__1;
extern lean_object* l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
lean_object* l_Lean_Elab_Command_State_inhabited___closed__1;
lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_Term_elabParen___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__1;
@ -404,7 +405,6 @@ lean_object* lean_environment_main_module(lean_object*);
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabOpen___closed__1;
lean_object* l_Lean_Elab_Command_elabVariables___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabExport___closed__1;
extern lean_object* l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
lean_object* l_Lean_Elab_Command_getScope(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabEnd___closed__6;
lean_object* l_Lean_Elab_Command_elabExport___boxed(lean_object*, lean_object*, lean_object*);
@ -12960,7 +12960,7 @@ x_9 = l_Lean_Elab_Command_logUnknownDecl___closed__2;
x_10 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_10, 0, x_9);
lean_ctor_set(x_10, 1, x_8);
x_11 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
x_11 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
x_12 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_12, 0, x_10);
lean_ctor_set(x_12, 1, x_11);

6
stage0/stdlib/Init/Lean/Elab/StructInst.c
View file

@ -119,6 +119,7 @@ lean_object* l_Lean_Elab_Term_whnf(lean_object*, lean_object*, lean_object*, lea
lean_object* l_Lean_Elab_Term_StructInst_FieldLHS_toSyntax___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_FieldLHS_hasFormat(lean_object*);
extern lean_object* l_Lean_mkTermIdFromIdent___closed__2;
extern lean_object* l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
lean_object* l_Lean_Elab_Term_StructInst_Source_isNone___boxed(lean_object*);
lean_object* l___private_Init_Lean_Elab_StructInst_4__elabModifyOp___closed__1;
extern lean_object* l_Lean_Parser_Term_proj___elambda__1___closed__2;
@ -242,7 +243,6 @@ lean_object* l_Lean_Elab_Term_StructInst_formatField___closed__1;
lean_object* l_List_map___main___at___private_Init_Lean_Elab_StructInst_7__mkStructView___spec__3(lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_Source_hasFormat___closed__1;
lean_object* l_Lean_Syntax_setArg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
lean_object* l_Lean_Elab_Term_StructInst_Struct_modifyFieldsM___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_Source_hasFormat___closed__4;
lean_object* l_AssocList_find___main___at___private_Init_Lean_Elab_StructInst_12__mkFieldMap___spec__2___boxed(lean_object*, lean_object*);
@ -10003,7 +10003,7 @@ lean_dec(x_8);
lean_dec(x_2);
x_34 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_34, 0, x_31);
x_35 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
x_35 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
x_36 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_36, 0, x_35);
lean_ctor_set(x_36, 1, x_34);
@ -11412,7 +11412,7 @@ lean_ctor_set(x_14, 0, x_2);
x_15 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_15, 0, x_13);
lean_ctor_set(x_15, 1, x_14);
x_16 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
x_16 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
x_17 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_17, 0, x_15);
lean_ctor_set(x_17, 1, x_16);

10
stage0/stdlib/Init/Lean/Elab/Syntax.c
View file

@ -177,6 +177,7 @@ lean_object* l_Lean_Elab_addBuiltinMacro(lean_object*, lean_object*, lean_object
uint8_t l_Lean_Parser_leadingIdentAsSymbol(lean_object*, lean_object*);
extern lean_object* l_Lean_mkTermIdFromIdent___closed__2;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__16;
extern lean_object* l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
extern lean_object* l_Lean_Parser_Command_macro__rules___elambda__1___closed__1;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__49;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__105;
@ -395,7 +396,6 @@ lean_object* l_Lean_Syntax_setArg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__18;
lean_object* l_Lean_Elab_Command_elabNoKindMacroRulesAux___closed__3;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__3;
extern lean_object* l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
extern lean_object* l_Lean_Parser_Syntax_sepBy1___elambda__1___closed__1;
uint8_t l_Lean_Parser_isParserCategory(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Syntax_5__withoutLeftRec___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -6717,7 +6717,7 @@ x_1633 = l_Lean_Elab_Term_toParserDescrAux___main___closed__118;
x_1634 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_1634, 0, x_1633);
lean_ctor_set(x_1634, 1, x_1632);
x_1635 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
x_1635 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
x_1636 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_1636, 0, x_1634);
lean_ctor_set(x_1636, 1, x_1635);
@ -8187,7 +8187,7 @@ x_378 = l_Lean_Elab_Term_toParserDescrAux___main___closed__118;
x_379 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_379, 0, x_378);
lean_ctor_set(x_379, 1, x_377);
x_380 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
x_380 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
x_381 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_381, 0, x_379);
lean_ctor_set(x_381, 1, x_380);
@ -9743,7 +9743,7 @@ x_19 = l_Lean_Elab_Command_elabMacroRulesAux___lambda__1___closed__3;
x_20 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_20, 0, x_19);
lean_ctor_set(x_20, 1, x_18);
x_21 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
x_21 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
x_22 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_22, 0, x_20);
lean_ctor_set(x_22, 1, x_21);
@ -9769,7 +9769,7 @@ x_27 = l_Lean_Elab_Command_elabMacroRulesAux___lambda__1___closed__6;
x_28 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_28, 0, x_27);
lean_ctor_set(x_28, 1, x_26);
x_29 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
x_29 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
x_30 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_30, 0, x_28);
lean_ctor_set(x_30, 1, x_29);

4
stage0/stdlib/Init/Lean/Elab/Tactic/Basic.c
View file

@ -134,6 +134,7 @@ lean_object* l___private_Init_Lean_Elab_Tactic_Basic_3__getIntrosSize___main___b
lean_object* l_Lean_Elab_Tactic_getMainGoal___closed__2;
lean_object* l___private_Init_Lean_Elab_Tactic_Basic_3__getIntrosSize(lean_object*);
lean_object* l_Lean_Elab_Tactic_monadLog___closed__3;
extern lean_object* l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__1;
lean_object* l_Lean_Meta_intro(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_tagUntaggedGoals___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -312,7 +313,6 @@ extern lean_object* l_Lean_Elab_macroAttribute;
lean_object* l_Lean_Elab_Tactic_liftMetaTactic(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalTactic___main___closed__1;
lean_object* lean_environment_main_module(lean_object*);
extern lean_object* l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
lean_object* l_Lean_Elab_Tactic_evalTactic___main___lambda__1___boxed(lean_object*, lean_object*);
lean_object* l_PersistentHashMap_empty___at_Lean_Elab_Tactic_mkBuiltinTacticTable___spec__3;
lean_object* l_Lean_Elab_Tactic_evalRevert___closed__1;
@ -15137,7 +15137,7 @@ x_25 = l_Array_umapMAux___main___at_Lean_Elab_Tactic_evalRevert___spec__1___clos
x_26 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_26, 0, x_25);
lean_ctor_set(x_26, 1, x_24);
x_27 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
x_27 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
x_28 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_28, 0, x_26);
lean_ctor_set(x_28, 1, x_27);

6
stage0/stdlib/Init/Lean/Elab/Term.c
View file

@ -256,6 +256,7 @@ lean_object* l_Lean_Elab_Term_monadLog___lambda__1___boxed(lean_object*, lean_ob
lean_object* l_Lean_Elab_Term_elabParen___closed__1;
lean_object* l_Lean_Elab_Term_elabListLit___closed__1;
extern lean_object* l_Lean_mkTermIdFromIdent___closed__2;
extern lean_object* l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_Term_elabParen___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_liftMetaM(lean_object*);
extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__1;
@ -589,7 +590,6 @@ lean_object* l_Lean_Elab_Term_withReducible(lean_object*);
lean_object* l_PersistentHashMap_contains___at_Lean_Elab_Term_addBuiltinTermElab___spec__4___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_TermElabM_inhabited___rarg(lean_object*);
uint8_t l_Lean_Expr_isMVar(lean_object*);
extern lean_object* l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
lean_object* l_Lean_Elab_Term_monadLog___closed__9;
lean_object* l_Lean_Meta_mkFreshExprMVar(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_mkConst___closed__5;
@ -23935,7 +23935,7 @@ x_11 = l_Lean_Elab_Term_mkConst___closed__2;
x_12 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_12, 0, x_11);
lean_ctor_set(x_12, 1, x_10);
x_13 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
x_13 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
x_14 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_14, 0, x_12);
lean_ctor_set(x_14, 1, x_13);
@ -24419,7 +24419,7 @@ x_30 = l_Lean_Elab_Term_resolveName___closed__3;
x_31 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_31, 0, x_30);
lean_ctor_set(x_31, 1, x_29);
x_32 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__41___closed__8;
x_32 = l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
x_33 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_33, 0, x_31);
lean_ctor_set(x_33, 1, x_32);

4
stage0/stdlib/Init/Lean/Meta/SynthInstance.c
View file

@ -281,7 +281,6 @@ lean_object* l_Lean_mkApp(lean_object*, lean_object*);
lean_object* l_Lean_Meta_SynthInstance_newSubgoal___closed__2;
uint8_t l_Lean_Expr_hasMVar(lean_object*);
lean_object* l_Lean_Meta_SynthInstance_synth___main___closed__8;
extern lean_object* l_Nat_forMAux___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__87___closed__1;
lean_object* l_Array_umapMAux___main___at_Lean_Meta_SynthInstance_getInstances___spec__2___closed__1;
lean_object* l_List_foldlM___main___at___private_Init_Lean_Meta_SynthInstance_3__preprocessLevels___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_SynthInstance_addContext___boxed(lean_object*, lean_object*, lean_object*);
@ -289,6 +288,7 @@ lean_object* l___private_Init_Lean_Util_Trace_5__checkTraceOptionM___at_Lean_Met
lean_object* l_Lean_Meta_SynthInstance_Waiter_isRoot___boxed(lean_object*);
uint8_t l_AssocList_contains___main___at_Lean_Meta_SynthInstance_MkTableKey_normLevel___main___spec__4(lean_object*, lean_object*);
lean_object* lean_panic_fn(lean_object*, lean_object*);
extern lean_object* l_Nat_forMAux___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__51___closed__1;
lean_object* l_Lean_MetavarContext_incDepth(lean_object*);
uint8_t l_Lean_TagAttribute_hasTag(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_SynthInstance_getResult___boxed(lean_object*);
@ -398,7 +398,7 @@ lean_object* l_Lean_Meta_SynthInstance_mkInferTCGoalsLRAttr___lambda__1(lean_obj
_start:
{
lean_object* x_3;
x_3 = l_Nat_forMAux___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__87___closed__1;
x_3 = l_Nat_forMAux___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__51___closed__1;
return x_3;
}
}

23412
stage0/stdlib/Init/Lean/Meta/Tactic/Clear.c
View file

File diff suppressed because it is too large Load diff

19229
stage0/stdlib/Init/Lean/MetavarContext.c
View file

File diff suppressed because it is too large Load diff