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:
Lean stage0 autoupdater 2025-09-18 04:56:02 +00:00
parent 6ca699b1ff
commit 5d50ec90f9
2 changed files with 51 additions and 53 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
stage0/src/stdlib_flags.h
View file

@ -1,11 +1,9 @@
// update me!
#include "util/options.h"
namespace lean {
options get_default_options() {
options opts;
// see https://github.com/leanprover/lean4/blob/master/doc/dev/bootstrap.md#further-bootstrapping-complications
opts = opts.update({"backward", "grind", "inferPattern"}, false);
#if LEAN_IS_STAGE0 == 1
// set to true to generally avoid bootstrapping issues limited to proofs
opts = opts.update({"debug", "proofAsSorry"}, false);

102
stage0/stdlib/Lean/Meta/Tactic/Grind/EMatchTheorem.c generated
View file

@ -21,6 +21,7 @@ LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_Defs_0__Std_DHas
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_mkEMatchTheoremWithKind_x3f___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* l_Lean_Expr_const___override(lean_object*, lean_object*);
lean_object* l_Lean_Meta_FVarSubst_apply(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Option_register___at___Lean_Meta_Grind_initFn____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4__spec__0(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_ematchTheoremsExt;
static lean_object* l___private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_dontCare___closed__0;
uint8_t lean_is_matcher(lean_object*, lean_object*);
@ -132,7 +133,6 @@ LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Origin_stx_elim(lean_object*, lean_ob
LEAN_EXPORT lean_object* l_Std_DHashMap_Internal_AssocList_foldlM___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_sizeOfDiff_spec__0___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Grind_instReprOrigin_repr___closed__5;
lean_object* l_Lean_Environment_header(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Option_register___at___Lean_Meta_Grind_initFn____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4__spec__0(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_ScopedEnvExtension_add___at___Lean_Meta_Grind_addSymbolPriorityAttr_spec__0___redArg___closed__0;
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_EMatchTheoremKind_toAttribute(lean_object*);
extern lean_object* l_Lean_maxRecDepthErrorMessage;
@ -142,6 +142,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_Grind_addEMatchTheorem(lean_object*, lean_o
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_checkTypeFVars___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Lean_PersistentHashMap_containsAtAux___at___Lean_PersistentHashMap_containsAux___at___Lean_PersistentHashMap_contains___at___Lean_Meta_Grind_SymbolPriorities_contains_spec__0_spec__0_spec__0(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_EMatchTheoremKind_eqBoth_elim(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Grind_initFn___closed__2____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_;
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_initFn___lam__2____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2275318982____hygCtx___hyg_2____boxed(lean_object*);
lean_object* l_Lean_MessageData_toString(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_DHashMap_Internal_Raw_u2080_expand___at___Std_DHashMap_Internal_Raw_u2080_insertIfNew___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_NormalizePattern_saveSymbol_spec__2_spec__2___redArg(lean_object*);
@ -171,7 +172,6 @@ LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_forIn_x27Uns
lean_object* l_Lean_PersistentHashMap_isUnaryNode___redArg(lean_object*);
static lean_object* l___private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_collectPatterns_x3f___closed__1;
lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Grind_initFn___closed__1____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_;
LEAN_EXPORT lean_object* l_Std_PRange_RangeIterator_instIteratorLoop_loop___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_NormalizePattern_go_spec__1(lean_object*, uint8_t, lean_object*, uint8_t, uint8_t, 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*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_NormalizePattern_PatternArgKind_instImplicit_elim___redArg(lean_object*);
static lean_object* l_Lean_Meta_Grind_mkOffsetPattern___closed__1;
@ -356,7 +356,6 @@ LEAN_EXPORT lean_object* l_Lean_Meta_Grind_getGlobalSymbolPriorities___redArg(le
lean_object* l_ReaderT_instApplicativeOfMonad___redArg___lam__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_initFn___closed__2____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_1821940401____hygCtx___hyg_2_;
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_NormalizePattern_PatternArgKind_proof_elim(lean_object*, uint8_t, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Grind_initFn___closed__4____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_;
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_collectPatterns_x3f_spec__0(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, 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_Std_DHashMap_Internal_Raw_u2080_expand___at___Std_DHashMap_Internal_Raw_u2080_insertIfNew___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_NormalizePattern_saveBVar_spec__0_spec__0(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_isMatcher___at___Lean_Meta_Grind_isMatchCongrEqDeclName_spec__0___redArg___boxed(lean_object*, lean_object*, lean_object*);
@ -495,7 +494,6 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lea
lean_object* l_Lean_mkNatAdd(lean_object*, lean_object*);
lean_object* l_Nat_reprFast(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_collectPatterns_x3f___lam__1(lean_object*);
static lean_object* l_Lean_Meta_Grind_initFn___closed__0____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_;
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_mkEMatchTheoremUsingSingletonPatterns_go_spec__0(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, 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*);
static lean_object* l_Lean_Meta_Grind_instReprGenPatternInfo_repr___redArg___closed__10;
@ -544,7 +542,6 @@ static lean_object* l_Lean_PersistentHashMap_empty___at___Lean_Meta_Grind_instIn
LEAN_EXPORT lean_object* l_Lean_throwError___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_NormalizePattern_go_spec__0(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_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_checkCoverage___lam__0___closed__0;
static lean_object* l_Lean_Meta_Grind_ppPattern___closed__7;
static lean_object* l_Lean_Meta_Grind_initFn___closed__5____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_;
LEAN_EXPORT lean_object* l_Lean_Meta_forallTelescopeReducing___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_preprocessMatchCongrEqType_spec__5___redArg___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_Meta_Grind_preprocessPattern(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_NormalizePattern_saveSymbol___redArg___boxed(lean_object*, lean_object*, lean_object*);
@ -576,6 +573,7 @@ static lean_object* l___private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Met
static lean_object* l_Lean_Expr_withAppAux___at___Lean_Expr_withAppAux___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_canBeSynthesized_spec__2_spec__2___closed__0;
static lean_object* l___private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_OldCollector_collect___lam__1___closed__2;
static size_t l_Lean_PersistentHashMap_eraseAux___at___Lean_PersistentHashMap_erase___at___Lean_Meta_Grind_SymbolPriorities_erase_spec__0_spec__0___redArg___closed__1;
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_initFn____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_(lean_object*);
uint8_t lean_expr_eqv(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_OldCollector_collect___lam__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_object*, lean_object*);
lean_object* l_Lean_Meta_Match_Extension_getMatcherInfo_x3f(lean_object*, lean_object*);
@ -628,6 +626,7 @@ static lean_object* l___private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Met
LEAN_EXPORT lean_object* l_Lean_throwError___at___Lean_throwErrorAt___at___Lean_throwUnknownIdentifierAt___at___Lean_throwUnknownConstantAt___at___Lean_throwUnknownConstant___at___Lean_getConstVal___at___Lean_Meta_Grind_EMatchTheorem_getProofWithFreshMVarLevels_spec__1_spec__1_spec__1_spec__1_spec__2_spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_NormalizePattern_go_goArg(lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_Defs_0__Std_DHashMap_Internal_Raw_u2080_expand_go___at___Std_DHashMap_Internal_Raw_u2080_expand___at___Std_DHashMap_Internal_Raw_u2080_insertIfNew___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_NormalizePattern_saveSymbol_spec__2_spec__2_spec__2___redArg(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Grind_initFn___closed__1____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_;
static lean_object* l_Lean_Meta_Grind_mkGroundPattern___closed__0;
static size_t l_Lean_PersistentHashMap_eraseAux___at___Lean_PersistentHashMap_erase___at___Lean_Meta_Grind_SymbolPriorities_erase_spec__0_spec__0___redArg___closed__0;
static lean_object* l___private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_NormalizePattern_go___closed__3;
@ -647,7 +646,6 @@ LEAN_EXPORT lean_object* l_Array_finIdxOf_x3f___at___Lean_PersistentHashMap_eras
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_collectSingletons_spec__2___redArg___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_EXPORT lean_object* l_Lean_Meta_Grind_Origin_ctorElim___redArg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_groundPattern_x3f(lean_object*);
static lean_object* l_Lean_Meta_Grind_initFn___closed__2____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_;
static lean_object* l_Lean_Meta_Grind_NormalizePattern_instReprPatternArgKind_repr___closed__1;
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_mapMUnsafe_map___at_____private_Lean_Meta_Transform_0__Lean_Core_transform_visit___at___Lean_Core_transform___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_expandOffsetPatterns_spec__0_spec__0_spec__0(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwUnknownConstant___at___Lean_getConstVal___at___Lean_Meta_Grind_EMatchTheorem_getProofWithFreshMVarLevels_spec__1_spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -809,6 +807,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_Grind_EMatchTheoremKind_eqBwd_elim___boxed(
static lean_object* l_Lean_logAt___at___Lean_log___at___Lean_logInfo___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_logPatternWhen_spec__2_spec__2_spec__2___lam__0___closed__1;
static lean_object* l_Lean_Meta_Grind_mkEMatchTheoremForDecl___closed__4;
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_NormalizePattern_main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Grind_initFn___closed__0____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_;
LEAN_EXPORT lean_object* l_Lean_addTrace___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_collectSingletons_spec__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___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_OldCollector_collect_spec__0___boxed(lean_object**);
lean_object* l_Lean_privateToUserName(lean_object*);
@ -964,7 +963,6 @@ LEAN_EXPORT lean_object* l_Lean_log___at___Lean_logInfo___at_____private_Lean_Me
LEAN_EXPORT lean_object* l_Array_idxOfAux___at___Array_finIdxOf_x3f___at___Lean_PersistentHashMap_eraseAux___at___Lean_PersistentHashMap_erase___at___Lean_Meta_Grind_SymbolPriorities_erase_spec__0_spec__0_spec__0_spec__0___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_anyMUnsafe_any___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_save_spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_foldlMUnsafe_fold___at_____private_Init_Data_Array_Basic_0__Array_foldlMUnsafe_fold___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_checkCoverage_spec__3_spec__3(lean_object*, lean_object*, size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_initFn____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_(lean_object*);
static lean_object* l___private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_save___closed__0;
LEAN_EXPORT lean_object* l_List_filterTR_loop___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_OldCollector_diff_spec__0___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Grind_mkEMatchEqTheoremCore___lam__1___closed__0;
@ -1015,7 +1013,6 @@ static lean_object* l_Lean_Meta_Grind_NormalizePattern_instReprPatternArgKind_re
static lean_object* l_Lean_Core_transform___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_detectOffsets_spec__0___closed__3;
static lean_object* l_Lean_Meta_Grind_instReprEMatchTheoremKind_repr___closed__10;
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_instReprGenPatternInfo;
static lean_object* l_Lean_Meta_Grind_initFn___closed__6____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_;
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_mkEMatchEqTheoremsForDef_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l___private_Init_Data_Array_Basic_0__Array_anyMUnsafe_any___at___Lean_Meta_Grind_EMatchTheorems_eraseDecl_spec__1(lean_object*, uint8_t, uint8_t, lean_object*, size_t, size_t);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_mkEMatchEqBwdTheoremCore___lam__0___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1043,7 +1040,6 @@ lean_object* l_Lean_Expr_getAppNumArgs(lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_foldlMUnsafe_fold___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_sizeOfDiff_spec__1(lean_object*, lean_object*, size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_logInfo___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_logPatternWhen_spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_mapTR_loop___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_checkCoverage_spec__2(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Option_register___at___Lean_Meta_Grind_initFn____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4__spec__0___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Grind_instReprGenPatternInfo_repr___redArg___closed__9;
lean_object* l_Lean_Name_mkStr6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Context_config(lean_object*);
@ -1097,7 +1093,6 @@ LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insert___at___Lean_Meta_Grind_
lean_object* lean_array_fget(lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_mkEMatchTheoremWithKind_x3f_collect___closed__0;
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_addGrindEqAttr(lean_object*, uint8_t, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Grind_initFn___closed__3____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_;
static lean_object* l_Lean_Meta_Grind_instReprGenPatternInfo_repr___redArg___closed__2;
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_containsAux___at___Lean_PersistentHashMap_contains___at___Lean_Meta_Grind_SymbolPriorities_contains_spec__0_spec__0___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Grind_EMatchTheoremKind_toAttribute___closed__0;
@ -1114,6 +1109,7 @@ LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_foldlMUnsafe
static lean_object* l_panic___at___Lean_Meta_Grind_isGenPattern_x3f_spec__0___closed__5;
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_EMatchTheoremKind_fwd_elim___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Id_instMonad___lam__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Grind_initFn___closed__4____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_;
lean_object* l_Lean_Expr_appFnCleanup___redArg(lean_object*);
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_toList___at___Lean_PersistentHashSet_toList___at___Lean_Meta_Grind_EMatchTheorems_getOrigins_spec__0_spec__0___redArg(lean_object*);
LEAN_EXPORT uint8_t l_Lean_Meta_Grind_isEqBwdPattern(lean_object*);
@ -1166,6 +1162,7 @@ LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_forIn_x27Uns
LEAN_EXPORT lean_object* l_Lean_isTracingEnabledFor___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_addNewPattern_spec__0___redArg(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Grind_splitWhileForbidden___closed__5;
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_EMatchTheoremKind_eqBoth_elim___redArg___boxed(lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Grind_initFn___closed__3____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_;
lean_object* l_Lean_PersistentHashMap_mkCollisionNode___redArg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_contains___at___Lean_Meta_Grind_SymbolPriorities_contains_spec__0___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_collectUsedPriorities_spec__1___redArg___lam__0(lean_object*, lean_object*, lean_object*);
@ -1220,6 +1217,7 @@ static lean_object* l_Lean_Meta_Grind_instReprGenPatternInfo_repr___redArg___clo
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_Origin_fvar_elim(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_PRange_RangeIterator_instIteratorLoop_loop___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_ppParamsAt_spec__1___boxed(lean_object**);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_ppPattern(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Option_register___at___Lean_Meta_Grind_initFn____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4__spec__0___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_collectSingletons_spec__2___redArg(lean_object*, lean_object*, size_t, size_t, 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_Grind_instReprEMatchTheoremKind;
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_detectGeneralizedPatterns_x3f___lam__0(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1356,6 +1354,7 @@ static lean_object* l_Lean_Meta_Grind_mkEMatchTheoremCore___closed__4;
LEAN_EXPORT lean_object* l_Std_DHashMap_Internal_Raw_u2080_Const_get_x3f___at_____private_Lean_Meta_Transform_0__Lean_Core_transform_visit___at___Lean_Core_transform___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_detectOffsets_spec__0_spec__0_spec__2___redArg___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_mkEMatchEqBwdTheoremCore___lam__0(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_PRange_RangeIterator_instIteratorLoop_loop___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_NormalizePattern_go_spec__1___boxed(lean_object**);
static lean_object* l_Lean_Meta_Grind_initFn___closed__6____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_;
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_foldlMAux___at___Lean_PersistentHashMap_foldlM___at___Lean_PersistentHashMap_foldl___at___Lean_PersistentHashMap_toList___at___Lean_PersistentHashSet_toList___at___Lean_Meta_Grind_EMatchTheorems_getOrigins_spec__0_spec__0_spec__0_spec__0_spec__0(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_EMatchTheoremKind_user_elim___redArg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_foldlMUnsafe_fold___at___Array_filterMapM___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_getPropTypes_spec__0_spec__0(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1497,6 +1496,7 @@ LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_forIn_x27Uns
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_canBeSynthesized_spec__0___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_List_beq___at___Option_instBEq_beq___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_collectPatterns_x3f_spec__2_spec__2___boxed(lean_object*, lean_object*);
lean_object* l_Lean_ScopedEnvExtension_addCore___redArg(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
static lean_object* l_Lean_Meta_Grind_initFn___closed__5____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_;
LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_Defs_0__Std_DHashMap_Internal_Raw_u2080_expand_go___at___Std_DHashMap_Internal_Raw_u2080_expand___at___Std_DHashMap_Internal_Raw_u2080_insert___at_____private_Lean_Meta_Transform_0__Lean_Core_transform_visit___at___Lean_Core_transform___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_detectOffsets_spec__0_spec__0_spec__8_spec__9_spec__9___redArg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_EMatchTheorems_erase(lean_object*, lean_object*);
uint8_t l_Lean_Meta_FVarSubst_contains(lean_object*, lean_object*);
@ -45488,7 +45488,7 @@ x_13 = l___private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_colle
return x_13;
}
}
LEAN_EXPORT lean_object* l_Lean_Option_register___at___Lean_Meta_Grind_initFn____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4__spec__0(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
LEAN_EXPORT lean_object* l_Lean_Option_register___at___Lean_Meta_Grind_initFn____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4__spec__0(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9; lean_object* x_10; lean_object* x_11;
@ -45564,7 +45564,7 @@ return x_21;
}
}
}
static lean_object* _init_l_Lean_Meta_Grind_initFn___closed__0____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_() {
static lean_object* _init_l_Lean_Meta_Grind_initFn___closed__0____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_() {
_start:
{
lean_object* x_1;
@ -45572,7 +45572,7 @@ x_1 = lean_mk_string_unchecked("backward", 8, 8);
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Grind_initFn___closed__1____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_() {
static lean_object* _init_l_Lean_Meta_Grind_initFn___closed__1____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_() {
_start:
{
lean_object* x_1;
@ -45580,18 +45580,18 @@ x_1 = lean_mk_string_unchecked("inferPattern", 12, 12);
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Grind_initFn___closed__2____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_() {
static lean_object* _init_l_Lean_Meta_Grind_initFn___closed__2____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Meta_Grind_initFn___closed__1____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_;
x_1 = l_Lean_Meta_Grind_initFn___closed__1____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_;
x_2 = l_Lean_Meta_Grind_mkGroundPattern___closed__0;
x_3 = l_Lean_Meta_Grind_initFn___closed__0____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_;
x_3 = l_Lean_Meta_Grind_initFn___closed__0____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_;
x_4 = l_Lean_Name_mkStr3(x_3, x_2, x_1);
return x_4;
}
}
static lean_object* _init_l_Lean_Meta_Grind_initFn___closed__3____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_() {
static lean_object* _init_l_Lean_Meta_Grind_initFn___closed__3____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_() {
_start:
{
lean_object* x_1;
@ -45599,7 +45599,7 @@ x_1 = lean_mk_string_unchecked("backward compatibility", 22, 22);
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Grind_initFn___closed__4____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_() {
static lean_object* _init_l_Lean_Meta_Grind_initFn___closed__4____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_() {
_start:
{
lean_object* x_1;
@ -45607,13 +45607,13 @@ x_1 = lean_mk_string_unchecked("use old E-matching pattern inference", 36, 36);
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Grind_initFn___closed__5____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_() {
static lean_object* _init_l_Lean_Meta_Grind_initFn___closed__5____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_Meta_Grind_initFn___closed__4____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_;
x_2 = l_Lean_Meta_Grind_initFn___closed__3____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_;
x_3 = 1;
x_1 = l_Lean_Meta_Grind_initFn___closed__4____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_;
x_2 = l_Lean_Meta_Grind_initFn___closed__3____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_;
x_3 = 0;
x_4 = lean_box(x_3);
x_5 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_5, 0, x_4);
@ -45622,13 +45622,13 @@ lean_ctor_set(x_5, 2, x_1);
return x_5;
}
}
static lean_object* _init_l_Lean_Meta_Grind_initFn___closed__6____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_() {
static lean_object* _init_l_Lean_Meta_Grind_initFn___closed__6____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_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; lean_object* x_7;
x_1 = l_Lean_Meta_Grind_initFn___closed__1____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_;
x_1 = l_Lean_Meta_Grind_initFn___closed__1____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_;
x_2 = l_Lean_Meta_Grind_mkGroundPattern___closed__0;
x_3 = l_Lean_Meta_Grind_initFn___closed__0____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_;
x_3 = l_Lean_Meta_Grind_initFn___closed__0____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_;
x_4 = l___private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_initFn___closed__8____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2275318982____hygCtx___hyg_2_;
x_5 = l___private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_initFn___closed__4____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2275318982____hygCtx___hyg_2_;
x_6 = l___private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_initFn___closed__2____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2275318982____hygCtx___hyg_2_;
@ -45636,22 +45636,22 @@ x_7 = l_Lean_Name_mkStr6(x_6, x_5, x_4, x_3, x_2, x_1);
return x_7;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_initFn____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_Meta_Grind_initFn____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_Meta_Grind_initFn___closed__2____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_;
x_3 = l_Lean_Meta_Grind_initFn___closed__5____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_;
x_4 = l_Lean_Meta_Grind_initFn___closed__6____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_;
x_5 = l_Lean_Option_register___at___Lean_Meta_Grind_initFn____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4__spec__0(x_2, x_3, x_4, x_1);
x_2 = l_Lean_Meta_Grind_initFn___closed__2____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_;
x_3 = l_Lean_Meta_Grind_initFn___closed__5____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_;
x_4 = l_Lean_Meta_Grind_initFn___closed__6____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_;
x_5 = l_Lean_Option_register___at___Lean_Meta_Grind_initFn____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4__spec__0(x_2, x_3, x_4, x_1);
return x_5;
}
}
LEAN_EXPORT lean_object* l_Lean_Option_register___at___Lean_Meta_Grind_initFn____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4__spec__0___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
LEAN_EXPORT lean_object* l_Lean_Option_register___at___Lean_Meta_Grind_initFn____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4__spec__0___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_Option_register___at___Lean_Meta_Grind_initFn____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4__spec__0(x_1, x_2, x_3, x_4);
x_5 = l_Lean_Option_register___at___Lean_Meta_Grind_initFn____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4__spec__0(x_1, x_2, x_3, x_4);
lean_dec_ref(x_2);
return x_5;
}
@ -45670,7 +45670,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Meta_Grind_initFn___closed__0____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2690967049____hygCtx___hyg_4_;
x_2 = l_Lean_Meta_Grind_mkGroundPattern___closed__0;
x_3 = l_Lean_Meta_Grind_initFn___closed__0____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_;
x_3 = l_Lean_Meta_Grind_initFn___closed__0____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_;
x_4 = l_Lean_Name_mkStr3(x_3, x_2, x_1);
return x_4;
}
@ -45688,7 +45688,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_Meta_Grind_initFn___closed__2____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2690967049____hygCtx___hyg_4_;
x_2 = l_Lean_Meta_Grind_initFn___closed__3____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_;
x_2 = l_Lean_Meta_Grind_initFn___closed__3____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_;
x_3 = 0;
x_4 = lean_box(x_3);
x_5 = lean_alloc_ctor(0, 3, 0);
@ -45704,7 +45704,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_1 = l_Lean_Meta_Grind_initFn___closed__0____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2690967049____hygCtx___hyg_4_;
x_2 = l_Lean_Meta_Grind_mkGroundPattern___closed__0;
x_3 = l_Lean_Meta_Grind_initFn___closed__0____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_;
x_3 = l_Lean_Meta_Grind_initFn___closed__0____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_;
x_4 = l___private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_initFn___closed__8____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2275318982____hygCtx___hyg_2_;
x_5 = l___private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_initFn___closed__4____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2275318982____hygCtx___hyg_2_;
x_6 = l___private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_initFn___closed__2____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2275318982____hygCtx___hyg_2_;
@ -45719,7 +45719,7 @@ lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_Meta_Grind_initFn___closed__1____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2690967049____hygCtx___hyg_4_;
x_3 = l_Lean_Meta_Grind_initFn___closed__3____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2690967049____hygCtx___hyg_4_;
x_4 = l_Lean_Meta_Grind_initFn___closed__4____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2690967049____hygCtx___hyg_4_;
x_5 = l_Lean_Option_register___at___Lean_Meta_Grind_initFn____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4__spec__0(x_2, x_3, x_4, x_1);
x_5 = l_Lean_Option_register___at___Lean_Meta_Grind_initFn____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4__spec__0(x_2, x_3, x_4, x_1);
return x_5;
}
}
@ -63341,21 +63341,21 @@ l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private
lean_mark_persistent(l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_normalizePattern_x3f_spec__0_spec__0___redArg___closed__1);
l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_normalizePattern_x3f_spec__0_spec__0___redArg___closed__2 = _init_l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_normalizePattern_x3f_spec__0_spec__0___redArg___closed__2();
lean_mark_persistent(l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_normalizePattern_x3f_spec__0_spec__0___redArg___closed__2);
l_Lean_Meta_Grind_initFn___closed__0____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_ = _init_l_Lean_Meta_Grind_initFn___closed__0____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_();
lean_mark_persistent(l_Lean_Meta_Grind_initFn___closed__0____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_);
l_Lean_Meta_Grind_initFn___closed__1____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_ = _init_l_Lean_Meta_Grind_initFn___closed__1____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_();
lean_mark_persistent(l_Lean_Meta_Grind_initFn___closed__1____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_);
l_Lean_Meta_Grind_initFn___closed__2____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_ = _init_l_Lean_Meta_Grind_initFn___closed__2____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_();
lean_mark_persistent(l_Lean_Meta_Grind_initFn___closed__2____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_);
l_Lean_Meta_Grind_initFn___closed__3____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_ = _init_l_Lean_Meta_Grind_initFn___closed__3____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_();
lean_mark_persistent(l_Lean_Meta_Grind_initFn___closed__3____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_);
l_Lean_Meta_Grind_initFn___closed__4____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_ = _init_l_Lean_Meta_Grind_initFn___closed__4____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_();
lean_mark_persistent(l_Lean_Meta_Grind_initFn___closed__4____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_);
l_Lean_Meta_Grind_initFn___closed__5____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_ = _init_l_Lean_Meta_Grind_initFn___closed__5____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_();
lean_mark_persistent(l_Lean_Meta_Grind_initFn___closed__5____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_);
l_Lean_Meta_Grind_initFn___closed__6____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_ = _init_l_Lean_Meta_Grind_initFn___closed__6____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_();
lean_mark_persistent(l_Lean_Meta_Grind_initFn___closed__6____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_);
if (builtin) {res = l_Lean_Meta_Grind_initFn____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_2192377466____hygCtx___hyg_4_(lean_io_mk_world());
l_Lean_Meta_Grind_initFn___closed__0____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_ = _init_l_Lean_Meta_Grind_initFn___closed__0____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_();
lean_mark_persistent(l_Lean_Meta_Grind_initFn___closed__0____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_);
l_Lean_Meta_Grind_initFn___closed__1____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_ = _init_l_Lean_Meta_Grind_initFn___closed__1____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_();
lean_mark_persistent(l_Lean_Meta_Grind_initFn___closed__1____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_);
l_Lean_Meta_Grind_initFn___closed__2____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_ = _init_l_Lean_Meta_Grind_initFn___closed__2____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_();
lean_mark_persistent(l_Lean_Meta_Grind_initFn___closed__2____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_);
l_Lean_Meta_Grind_initFn___closed__3____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_ = _init_l_Lean_Meta_Grind_initFn___closed__3____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_();
lean_mark_persistent(l_Lean_Meta_Grind_initFn___closed__3____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_);
l_Lean_Meta_Grind_initFn___closed__4____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_ = _init_l_Lean_Meta_Grind_initFn___closed__4____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_();
lean_mark_persistent(l_Lean_Meta_Grind_initFn___closed__4____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_);
l_Lean_Meta_Grind_initFn___closed__5____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_ = _init_l_Lean_Meta_Grind_initFn___closed__5____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_();
lean_mark_persistent(l_Lean_Meta_Grind_initFn___closed__5____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_);
l_Lean_Meta_Grind_initFn___closed__6____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_ = _init_l_Lean_Meta_Grind_initFn___closed__6____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_();
lean_mark_persistent(l_Lean_Meta_Grind_initFn___closed__6____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_);
if (builtin) {res = l_Lean_Meta_Grind_initFn____x40_Lean_Meta_Tactic_Grind_EMatchTheorem_3627094279____hygCtx___hyg_4_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
l_Lean_Meta_Grind_backward_grind_inferPattern = lean_io_result_get_value(res);
lean_mark_persistent(l_Lean_Meta_Grind_backward_grind_inferPattern);