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-02-17 17:14:40 -08:00
parent c5673b6025
commit 083efd5825
24 changed files with 8012 additions and 7553 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
stage0/src/Lean/Elab/InfoTree.lean generated
View file

@ -195,8 +195,13 @@ def mkInfoNode (info : Info) : m Unit := do
else
x
@[inline] def withInfoContext [MonadFinally m] (x : m α) (mkInfo : m Info) : m α :=
withInfoContext' x fun _ => return Sum.inl (← mkInfo)
@[inline] def withInfoContext [MonadFinally m] (x : m α) (mkInfo : m Info) : m α := do
if (← getInfoState).enabled then
let treesSaved ← getResetInfoTrees
Prod.fst <$> MonadFinally.tryFinally' x fun _ => do
modifyInfoTrees fun trees => treesSaved.push <| InfoTree.node (← mkInfo) trees
else
x
def getInfoHoleIdAssignment? (mvarId : MVarId) : m (Option InfoTree) :=
return (← getInfoState).assignment[mvarId]
@ -218,12 +223,11 @@ def withMacroExpansionInfo [MonadFinally m] [Monad m] [MonadInfoTree m] [MonadLC
@[inline] def withInfoHole [MonadFinally m] [Monad m] [MonadInfoTree m] (mvarId : MVarId) (x : m α) : m α := do
if (← getInfoState).enabled then
let treesSaved ← getResetInfoTrees
Prod.fst <$> MonadFinally.tryFinally' x fun a? => do
match a? with
| none => modifyInfoTrees fun _ => treesSaved
| some a => modifyInfoState fun s =>
assert! s.trees.size == 1 -- if size is not one, then API is being misused.
{ s with trees := treesSaved, assignment := s.assignment.insert mvarId s.trees[0] }
Prod.fst <$> MonadFinally.tryFinally' x fun a? => modifyInfoState fun s =>
if s.trees.size > 0 then
{ s with trees := treesSaved, assignment := s.assignment.insert mvarId s.trees[s.trees.size - 1] }
else
{ s with trees := treesSaved }
else
x

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

@ -58,9 +58,9 @@ private def mkUserNameFor (e : Expr) : TermElabM Name :=
| Expr.fvar fvarId _ => do pure (← getLocalDecl fvarId).userName
| _ => mkFreshBinderName
-- `expandNonAtomicDiscrs?` create auxiliary variables with base name `_discr`
private def isAuxDiscrName (n : Name) : Bool :=
n.eraseMacroScopes == `_discr
/-- Return true iff `n` is an auxiliary variable created by `expandNonAtomicDiscrs?` -/
def isAuxDiscrName (n : Name) : Bool :=
n.hasMacroScopes && n.eraseMacroScopes == `_discr
-- See expandNonAtomicDiscrs?
private def elabAtomicDiscr (discr : Syntax) : TermElabM Expr := do

21
stage0/src/Lean/Elab/Tactic/Basic.lean generated
View file

@ -45,9 +45,11 @@ def saveBacktrackableState : TacticM BacktrackableState := do
def BacktrackableState.restore (b : BacktrackableState) : TacticM Unit := do
setEnv b.env
setMCtx b.mctx
let infoState ← getInfoState -- we do not backtrack info state
let msgLog ← Term.getMessageLog -- we do not backtrack the message log
set b.term
Term.setMessageLog msgLog
modifyInfoState fun _ => infoState
modify fun s => { s with goals := b.goals }
@[inline] protected def tryCatch {α} (x : TacticM α) (h : Exception → TacticM α) : TacticM α := do
@ -81,9 +83,6 @@ def SavedState.restore (s : SavedState) : TacticM Unit := do
@[inline] def liftMetaM {α} (x : MetaM α) : TacticM α := liftTermElabM $ Term.liftMetaM x
def ensureHasType (expectedType? : Option Expr) (e : Expr) : TacticM Expr := liftTermElabM $ Term.ensureHasType expectedType? e
def reportUnsolvedGoals (goals : List MVarId) : TacticM Unit := liftTermElabM $ Term.reportUnsolvedGoals goals
protected def getCurrMacroScope : TacticM MacroScope := do pure (← readThe Term.Context).currMacroScope
protected def getMainModule : TacticM Name := do pure (← getEnv).mainModule
@ -207,7 +206,7 @@ def withMainMVarContext {α} (x : TacticM α) : TacticM α := do
@[inline] def liftMetaMAtMain {α} (x : MVarId → MetaM α) : TacticM α := do
let (g, _) ← getMainGoal
withMVarContext g $ liftMetaM $ x g
withMVarContext g <| x g
@[inline] def liftMetaTacticAux {α} (tactic : MVarId → MetaM (α × List MVarId)) : TacticM α := do
let (g, gs) ← getMainGoal
@ -224,7 +223,7 @@ def withMainMVarContext {α} (x : TacticM α) : TacticM α := do
def done : TacticM Unit := do
let gs ← getUnsolvedGoals;
unless gs.isEmpty do
reportUnsolvedGoals gs
Term.reportUnsolvedGoals gs
@[builtinTactic Lean.Parser.Tactic.«done»] def evalDone : Tactic := fun _ => done
@ -354,8 +353,8 @@ where
@[builtinTactic Lean.Parser.Tactic.introMatch] def evalIntroMatch : Tactic := fun stx => do
let matchAlts := stx[1]
let stxNew ← liftMacroM $ Term.expandMatchAltsIntoMatchTactic stx matchAlts
withMacroExpansion stx stxNew $ evalTactic stxNew
let stxNew ← liftMacroM <| Term.expandMatchAltsIntoMatchTactic stx matchAlts
withMacroExpansion stx stxNew <| evalTactic stxNew
private def getIntrosSize : Expr → Nat
| Expr.forallE _ _ b _ => getIntrosSize b + 1
@ -380,7 +379,7 @@ def getNameOfIdent' (id : Syntax) : Name :=
| _ => throwUnsupportedSyntax
def getFVarId (id : Syntax) : TacticM FVarId := withRef id do
let fvar? ← liftTermElabM $ Term.isLocalIdent? id;
let fvar? ← Term.isLocalIdent? id;
match fvar? with
| some fvar => pure fvar.fvarId!
| none => throwError! "unknown variable '{id.getId}'"
@ -450,12 +449,12 @@ private def findTag? (gs : List MVarId) (tag : Name) : TacticM (Option MVarId) :
let some g ← findTag? gs tag | throwError "tag not found"
let gs := gs.erase g
setGoals [g]
let savedTag ← liftM $ getMVarTag g
liftM $ setMVarTag g Name.anonymous
let savedTag ← getMVarTag g
setMVarTag g Name.anonymous
try
closeUsingOrAdmit tac
finally
liftM $ setMVarTag g savedTag
setMVarTag g savedTag
done
setGoals gs
| _ => throwUnsupportedSyntax

2
stage0/src/Lean/Elab/Tactic/ElabTerm.lean generated
View file

@ -23,7 +23,7 @@ def elabTerm (stx : Syntax) (expectedType? : Option Expr) (mayPostpone := false)
def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (mayPostpone := false) : TacticM Expr := do
let e ← elabTerm stx expectedType? mayPostpone
ensureHasType expectedType? e
Term.ensureHasType expectedType? e
@[builtinTactic «exact»] def evalExact : Tactic := fun stx =>
match stx with

8
stage0/src/Lean/Elab/Tactic/Match.lean generated
View file

@ -28,13 +28,13 @@ private def mkAuxiliaryMatchTermAux (parentTag : Name) (matchTac : Syntax) : Sta
let holeName := mkIdentFrom holeOrTacticSeq tag
let newHole ← `(?$holeName:ident)
modify fun s => { s with nextIdx := s.nextIdx + 1}
pure $ alt.setArg 3 newHole
pure <| alt.setArg 3 newHole
else withFreshMacroScope do
let newHole ← `(?rhs)
let newHoleId := newHole[1]
let newCase ← `(tactic| case $newHoleId => $holeOrTacticSeq:tacticSeq )
modify fun s => { s with cases := s.cases.push newCase }
pure $ alt.setArg 3 newHole
pure <| alt.setArg 3 newHole
let result := matchTac.setKind ``Parser.Term.«match»
let result := result.setArg 4 (mkNode ``Parser.Term.matchAlts #[mkNullNode newAlts])
pure result
@ -46,9 +46,9 @@ private def mkAuxiliaryMatchTerm (parentTag : Name) (matchTac : Syntax) : MacroM
@[builtinTactic Lean.Parser.Tactic.match]
def evalMatch : Tactic := fun stx => do
let tag ← getMainTag
let (matchTerm, cases) ← liftMacroM $ mkAuxiliaryMatchTerm tag stx
let (matchTerm, cases) ← liftMacroM <| mkAuxiliaryMatchTerm tag stx
let refineMatchTerm ← `(tactic| refine $matchTerm)
let stxNew := mkNullNode (#[refineMatchTerm] ++ cases)
withMacroExpansion stx stxNew $ evalTactic stxNew
withMacroExpansion stx stxNew <| evalTactic stxNew
end Lean.Elab.Tactic

3
stage0/src/Lean/Parser/Tactic.lean generated
View file

@ -15,6 +15,9 @@ builtin_initialize
@[builtinTacticParser] def «unknown» := parser! withPosition (ident >> errorAtSavedPos "unknown tactic" true)
@[builtinTacticParser] def nestedTactic := tacticSeqBracketed
/- Auxiliary parser for expanding `match` tactic -/
@[builtinTacticParser] def eraseAuxDiscrs := parser!:maxPrec "eraseAuxDiscrs!"
def matchRhs := Term.hole <|> Term.syntheticHole <|> tacticSeq
def matchAlts := Term.matchAlts (rhsParser := matchRhs)
@[builtinTacticParser] def «match» := parser!:leadPrec "match " >> sepBy1 Term.matchDiscr ", " >> Term.optType >> " with " >> matchAlts

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

@ -308,6 +308,7 @@ lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Do_0__Lean_Elab_Ter
lean_object* lean_string_utf8_byte_size(lean_object*);
lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_extractBind___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_ToTerm_returnToTerm___closed__36;
lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MessageData_joinSep(lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Quotation_getPatternsVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -788,6 +789,7 @@ lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_expandDoIf_x3f_match_
lean_object* l_Lean_throwError___at___private_Lean_Elab_Do_0__Lean_Elab_Term_extractBind___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doReassignArrowToCode___closed__7;
lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_expandDoIf_x3f_match__8(lean_object*);
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__5___rarg(lean_object*);
lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_getDoSeqElems(lean_object*);
lean_object* l_Lean_Elab_Term_Do_pullExitPointsAux_match__1(lean_object*);
lean_object* l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -825,7 +827,6 @@ lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__1___closed__1
lean_object* l_Lean_Elab_Term_Do_ToTerm_breakToTerm___closed__14;
lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Term_Do_ToTerm_returnToTerm___spec__1___boxed(lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_Do_convertTerminalActionIntoJmp_loop___spec__3(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__7___rarg(lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_Do_ToTerm_mkJoinPoint___spec__2(size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_hasLiftMethod_match__1(lean_object*);
lean_object* l_Lean_Elab_Term_Do_hasTerminalAction___boxed(lean_object*);
@ -843,7 +844,6 @@ lean_object* l_Lean_Elab_Term_Do_ToTerm_breakToTerm___closed__18;
lean_object* l_Lean_Elab_Term_Do_ToTerm_returnToTerm___closed__1;
lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_toDoElem(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_pullExitPointsAux___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_expandDoIf_x3f_match__10___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_ToTerm_breakToTerm___closed__15;
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_27939_(lean_object*);
@ -63340,7 +63340,7 @@ x_87 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_87, 0, x_86);
x_88 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_88, 0, x_87);
x_89 = l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__5(x_85, x_88, x_3, x_4, x_5, x_6, x_7, x_8, x_60);
x_89 = l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__3(x_85, x_88, x_3, x_4, x_5, x_6, x_7, x_8, x_60);
lean_dec(x_8);
lean_dec(x_6);
lean_dec(x_5);
@ -63374,7 +63374,7 @@ lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_94 = l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__7___rarg(x_60);
x_94 = l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__5___rarg(x_60);
x_95 = !lean_is_exclusive(x_94);
if (x_95 == 0)
{

403
stage0/stdlib/Lean/Elab/InfoTree.c generated
View file

@ -22,7 +22,6 @@ lean_object* lean_io_get_num_heartbeats(lean_object*);
lean_object* l_Lean_Elab_InfoTree_substitute_match__1(lean_object*);
lean_object* l_Std_PersistentHashMap_insertAux___at_Lean_Elab_assignInfoHoleId___spec__2___boxed__const__2;
extern lean_object* l_Lean_Meta_ppGoal_ppVars___closed__1;
lean_object* l_Lean_Elab_withInfoContext_x27___at_Lean_Elab_withInfoContext___spec__1(lean_object*);
lean_object* l_Array_modify___at_Lean_Elab_assignInfoHoleId___spec__4___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_InternalExceptionId_toString___closed__1;
lean_object* lean_array_uget(lean_object*, size_t);
@ -61,6 +60,7 @@ extern lean_object* l_instReprSigma___rarg___closed__1;
lean_object* l_Lean_Elab_ContextInfo_runMetaM_match__1(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Info_format_match__1(lean_object*);
lean_object* l_Lean_Elab_getInfoTrees___rarg___lambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Elab_withInfoContext___rarg___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_instReprSigma___rarg___closed__7;
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
@ -74,6 +74,7 @@ lean_object* l_Lean_Elab_withInfoHole___rarg___lambda__3(lean_object*, lean_obje
lean_object* l_ReaderT_bind___at_Lean_Meta_instMonadLCtxMetaM___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_InfoTree_format(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_instInhabitedFieldInfo___closed__1;
lean_object* l_Lean_Elab_withInfoContext___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
size_t l_USize_shiftRight(size_t, size_t);
lean_object* l_Lean_Elab_withInfoContext_x27___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_ContextInfo_options___default;
@ -118,9 +119,9 @@ lean_object* l_Lean_Syntax_getHeadInfo(lean_object*);
lean_object* l_Lean_Elab_withInfoHole___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_insertAux___at_Lean_Elab_assignInfoHoleId___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_withInfoContext_x27___rarg___lambda__2(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_withInfoContext___rarg___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_InfoTree_format_match__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_withInfoHole___rarg___lambda__1___closed__3;
lean_object* l_Lean_Elab_TacticInfo_format___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_ContextInfo_mctx___default;
lean_object* l_Lean_Elab_withInfoHole___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -136,6 +137,7 @@ lean_object* l_Lean_Elab_ContextInfo_runMetaM(lean_object*);
lean_object* l_Lean_Elab_TermInfo_format___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_TermInfo_format___lambda__1___closed__1;
lean_object* l_Lean_Elab_TacticInfo_format___closed__1;
lean_object* l_Lean_Elab_withInfoContext___rarg___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
size_t l_Lean_Name_hash(lean_object*);
lean_object* l_Lean_Elab_TacticInfo_format___closed__6;
lean_object* l_Nat_repr(lean_object*);
@ -148,7 +150,6 @@ extern lean_object* l_instReprSigma___rarg___closed__5;
lean_object* lean_st_mk_ref(lean_object*, lean_object*);
lean_object* l_Lean_Core_getMaxHeartbeats(lean_object*);
lean_object* l_Lean_Elab_instInhabitedContextInfo___closed__1;
lean_object* l_Lean_Elab_withInfoHole_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_ContextInfo_toPPContext(lean_object*, lean_object*);
lean_object* l_Lean_Elab_InfoState_assignment___default;
lean_object* l_Lean_Elab_TermInfo_format___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -166,7 +167,6 @@ lean_object* l_Lean_Elab_withInfoContext_x27___rarg___lambda__3(lean_object*, le
lean_object* l_Std_PersistentHashMap_insertAux_traverse___at_Lean_Elab_assignInfoHoleId___spec__3(size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange_fmtPos_match__1(lean_object*);
lean_object* l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_withInfoHole___rarg___lambda__1___closed__1;
lean_object* l_Lean_Elab_InfoTree_substitute_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange___closed__1;
lean_object* l_Std_PersistentHashMap_findAux___at_Lean_Elab_InfoTree_substitute___spec__7(lean_object*, size_t, lean_object*);
@ -179,9 +179,7 @@ lean_object* l_Lean_Elab_ContextInfo_ppGoals___boxed(lean_object*, lean_object*,
size_t l_USize_mul(size_t, size_t);
lean_object* l_Lean_Elab_ContextInfo_ppGoals___closed__2;
lean_object* l_Lean_Elab_getInfoTrees(lean_object*);
lean_object* l_Lean_Elab_withInfoHole___rarg___lambda__1___closed__4;
lean_object* l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange(lean_object*, lean_object*);
lean_object* l_Lean_Elab_withInfoContext___rarg___lambda__2___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_getInfoHoleIdAssignment_x3f___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_enableInfoTree___rarg___boxed(lean_object*, lean_object*);
size_t lean_usize_of_nat(lean_object*);
@ -218,8 +216,6 @@ lean_object* l_Lean_Elab_MacroExpansionInfo_format___boxed(lean_object*, lean_ob
lean_object* l_Std_PersistentArray_get_x21___at_Lean_Elab_withInfoHole___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_assignInfoHoleId___rarg___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_InfoTree_format___closed__1;
lean_object* l_Lean_Elab_withInfoHole___rarg___lambda__1___closed__2;
lean_object* l_Lean_Elab_withInfoContext_x27___at_Lean_Elab_withInfoContext___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_instInhabitedInfo___closed__1;
lean_object* l_Lean_Elab_assignInfoHoleId(lean_object*);
lean_object* lean_panic_fn(lean_object*, lean_object*);
@ -278,7 +274,7 @@ extern lean_object* l_Lean_Core_State_ngen___default___closed__1;
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_InfoTree_substitute___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Expr_instantiateBetaRevRange___closed__1;
lean_object* l_Lean_Elab_getInfoTrees___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_withInfoContext___rarg___lambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Elab_withInfoContext___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_assignInfoHoleId___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_instInhabitedTermInfo___closed__1;
lean_object* l_Std_Format_prefixJoin___at_Lean_Elab_ContextInfo_ppGoals___spec__2___boxed(lean_object*, lean_object*);
@ -298,7 +294,7 @@ extern lean_object* l_instInhabitedPUnit;
lean_object* l_Lean_Elab_InfoTree_format_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_instInhabitedFieldInfo;
lean_object* l_Std_Format_nestD(lean_object*);
lean_object* l_Lean_Elab_withInfoHole_match__1(lean_object*, lean_object*);
lean_object* l_Lean_Elab_withInfoContext___rarg___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_mkCollisionNode___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_ContextInfo_ppGoals___closed__3;
lean_object* l_Array_modifyM___at_Lean_Elab_assignInfoHoleId___spec__5___boxed(lean_object*, lean_object*, lean_object*);
@ -4302,48 +4298,41 @@ lean_dec(x_7);
return x_8;
}
}
lean_object* l_Lean_Elab_withInfoContext_x27___at_Lean_Elab_withInfoContext___spec__1___rarg(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* l_Lean_Elab_withInfoContext___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_7 = lean_ctor_get(x_1, 1);
lean_inc(x_7);
x_8 = lean_ctor_get(x_2, 0);
lean_inc(x_8);
lean_inc(x_7);
x_9 = lean_alloc_closure((void*)(l_Lean_Elab_withInfoContext_x27___rarg___lambda__6___boxed), 7, 6);
lean_closure_set(x_9, 0, x_5);
lean_closure_set(x_9, 1, x_1);
lean_closure_set(x_9, 2, x_2);
lean_closure_set(x_9, 3, x_6);
lean_closure_set(x_9, 4, x_7);
lean_closure_set(x_9, 5, x_4);
x_10 = lean_apply_4(x_7, lean_box(0), lean_box(0), x_8, x_9);
return x_10;
}
}
lean_object* l_Lean_Elab_withInfoContext_x27___at_Lean_Elab_withInfoContext___spec__1(lean_object* x_1) {
_start:
uint8_t x_4;
x_4 = !lean_is_exclusive(x_3);
if (x_4 == 0)
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Elab_withInfoContext_x27___at_Lean_Elab_withInfoContext___spec__1___rarg), 6, 0);
return x_2;
lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_5 = lean_ctor_get(x_3, 1);
x_6 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_6, 0, x_1);
lean_ctor_set(x_6, 1, x_5);
x_7 = l_Std_PersistentArray_push___rarg(x_2, x_6);
lean_ctor_set(x_3, 1, x_7);
return x_3;
}
}
lean_object* l_Lean_Elab_withInfoContext___rarg___lambda__1(lean_object* x_1, lean_object* x_2) {
_start:
else
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_3 = lean_ctor_get(x_1, 0);
lean_inc(x_3);
lean_dec(x_1);
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
uint8_t x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_8 = lean_ctor_get_uint8(x_3, sizeof(void*)*2);
x_9 = lean_ctor_get(x_3, 0);
x_10 = lean_ctor_get(x_3, 1);
lean_inc(x_10);
lean_inc(x_9);
lean_dec(x_3);
x_5 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_5, 0, x_2);
x_6 = lean_apply_2(x_4, lean_box(0), x_5);
return x_6;
x_11 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_11, 0, x_1);
lean_ctor_set(x_11, 1, x_10);
x_12 = l_Std_PersistentArray_push___rarg(x_2, x_11);
x_13 = lean_alloc_ctor(0, 2, 1);
lean_ctor_set(x_13, 0, x_9);
lean_ctor_set(x_13, 1, x_12);
lean_ctor_set_uint8(x_13, sizeof(void*)*2, x_8);
return x_13;
}
}
}
lean_object* l_Lean_Elab_withInfoContext___rarg___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
@ -4352,22 +4341,100 @@ _start:
lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = lean_ctor_get(x_1, 1);
lean_inc(x_4);
x_5 = lean_alloc_closure((void*)(l_Lean_Elab_withInfoContext___rarg___lambda__1), 2, 1);
lean_closure_set(x_5, 0, x_1);
x_6 = lean_apply_4(x_4, lean_box(0), lean_box(0), x_2, x_5);
lean_dec(x_1);
x_5 = lean_alloc_closure((void*)(l_Lean_Elab_withInfoContext___rarg___lambda__1), 3, 2);
lean_closure_set(x_5, 0, x_3);
lean_closure_set(x_5, 1, x_2);
x_6 = lean_apply_1(x_4, x_5);
return x_6;
}
}
lean_object* l_Lean_Elab_withInfoContext___rarg___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7;
x_6 = lean_alloc_closure((void*)(l_Lean_Elab_withInfoContext___rarg___lambda__2), 3, 2);
lean_closure_set(x_6, 0, x_1);
lean_closure_set(x_6, 1, x_2);
x_7 = lean_apply_4(x_3, lean_box(0), lean_box(0), x_4, x_6);
return x_7;
}
}
lean_object* l_Lean_Elab_withInfoContext___rarg___lambda__4(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) {
_start:
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_8 = lean_ctor_get(x_1, 0);
lean_inc(x_8);
lean_dec(x_1);
x_9 = lean_ctor_get(x_8, 0);
lean_inc(x_9);
lean_dec(x_8);
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
lean_dec(x_9);
x_11 = lean_alloc_closure((void*)(l_Lean_Elab_withInfoContext___rarg___lambda__3___boxed), 5, 4);
lean_closure_set(x_11, 0, x_2);
lean_closure_set(x_11, 1, x_7);
lean_closure_set(x_11, 2, x_3);
lean_closure_set(x_11, 3, x_4);
x_12 = lean_apply_4(x_5, lean_box(0), lean_box(0), x_6, x_11);
x_13 = l_tryFinally___rarg___closed__1;
x_14 = lean_apply_4(x_10, lean_box(0), lean_box(0), x_13, x_12);
return x_14;
}
}
lean_object* l_Lean_Elab_withInfoContext___rarg___lambda__5(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) {
_start:
{
uint8_t x_8;
x_8 = lean_ctor_get_uint8(x_7, sizeof(void*)*2);
if (x_8 == 0)
{
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
return x_1;
}
else
{
lean_object* x_9; lean_object* x_10; lean_object* x_11;
lean_inc(x_3);
lean_inc(x_2);
x_9 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_getResetInfoTrees___rarg(x_2, x_3);
lean_inc(x_4);
x_10 = lean_alloc_closure((void*)(l_Lean_Elab_withInfoContext___rarg___lambda__4), 7, 6);
lean_closure_set(x_10, 0, x_2);
lean_closure_set(x_10, 1, x_3);
lean_closure_set(x_10, 2, x_4);
lean_closure_set(x_10, 3, x_5);
lean_closure_set(x_10, 4, x_6);
lean_closure_set(x_10, 5, x_1);
x_11 = lean_apply_4(x_4, lean_box(0), lean_box(0), x_9, x_10);
return x_11;
}
}
}
lean_object* l_Lean_Elab_withInfoContext___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7; lean_object* x_8;
lean_inc(x_1);
x_7 = lean_alloc_closure((void*)(l_Lean_Elab_withInfoContext___rarg___lambda__2___boxed), 3, 2);
lean_closure_set(x_7, 0, x_1);
lean_closure_set(x_7, 1, x_6);
x_8 = l_Lean_Elab_withInfoContext_x27___at_Lean_Elab_withInfoContext___spec__1___rarg(x_1, x_2, lean_box(0), x_4, x_5, x_7);
return x_8;
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_7 = lean_ctor_get(x_1, 1);
lean_inc(x_7);
x_8 = lean_ctor_get(x_2, 0);
lean_inc(x_8);
lean_inc(x_7);
x_9 = lean_alloc_closure((void*)(l_Lean_Elab_withInfoContext___rarg___lambda__5___boxed), 7, 6);
lean_closure_set(x_9, 0, x_5);
lean_closure_set(x_9, 1, x_1);
lean_closure_set(x_9, 2, x_2);
lean_closure_set(x_9, 3, x_7);
lean_closure_set(x_9, 4, x_6);
lean_closure_set(x_9, 5, x_4);
x_10 = lean_apply_4(x_7, lean_box(0), lean_box(0), x_8, x_9);
return x_10;
}
}
lean_object* l_Lean_Elab_withInfoContext(lean_object* x_1) {
@ -4378,13 +4445,22 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Elab_withInfoContext___rarg), 6, 0);
return x_2;
}
}
lean_object* l_Lean_Elab_withInfoContext___rarg___lambda__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_Elab_withInfoContext___rarg___lambda__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_4;
x_4 = l_Lean_Elab_withInfoContext___rarg___lambda__2(x_1, x_2, x_3);
lean_dec(x_3);
return x_4;
lean_object* x_6;
x_6 = l_Lean_Elab_withInfoContext___rarg___lambda__3(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_5);
return x_6;
}
}
lean_object* l_Lean_Elab_withInfoContext___rarg___lambda__5___boxed(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) {
_start:
{
lean_object* x_8;
x_8 = l_Lean_Elab_withInfoContext___rarg___lambda__5(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
lean_dec(x_7);
return x_8;
}
}
lean_object* l_Lean_Elab_getInfoHoleIdAssignment_x3f___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
@ -4974,7 +5050,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Elab_assignInfoHoleId___rarg___lambda__2___closed__3;
x_2 = l_Lean_Elab_assignInfoHoleId___rarg___lambda__2___closed__4;
x_3 = lean_unsigned_to_nat(205u);
x_3 = lean_unsigned_to_nat(210u);
x_4 = lean_unsigned_to_nat(2u);
x_5 = l_Lean_Elab_assignInfoHoleId___rarg___lambda__2___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -5128,7 +5204,7 @@ return x_9;
lean_object* l_Lean_Elab_withMacroExpansionInfo___rarg(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) {
_start:
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_8 = lean_ctor_get(x_2, 1);
lean_inc(x_8);
lean_inc(x_2);
@ -5136,9 +5212,20 @@ x_9 = lean_alloc_closure((void*)(l_Lean_Elab_withMacroExpansionInfo___rarg___lam
lean_closure_set(x_9, 0, x_2);
lean_closure_set(x_9, 1, x_5);
lean_closure_set(x_9, 2, x_6);
lean_inc(x_8);
x_10 = lean_apply_4(x_8, lean_box(0), lean_box(0), x_4, x_9);
x_11 = l_Lean_Elab_withInfoContext___rarg(x_2, x_3, lean_box(0), x_1, x_7, x_10);
return x_11;
x_11 = lean_ctor_get(x_3, 0);
lean_inc(x_11);
lean_inc(x_8);
x_12 = lean_alloc_closure((void*)(l_Lean_Elab_withInfoContext___rarg___lambda__5___boxed), 7, 6);
lean_closure_set(x_12, 0, x_7);
lean_closure_set(x_12, 1, x_2);
lean_closure_set(x_12, 2, x_3);
lean_closure_set(x_12, 3, x_8);
lean_closure_set(x_12, 4, x_10);
lean_closure_set(x_12, 5, x_1);
x_13 = lean_apply_4(x_8, lean_box(0), lean_box(0), x_11, x_12);
return x_13;
}
}
lean_object* l_Lean_Elab_withMacroExpansionInfo(lean_object* x_1, lean_object* x_2) {
@ -5149,37 +5236,6 @@ x_3 = lean_alloc_closure((void*)(l_Lean_Elab_withMacroExpansionInfo___rarg), 7,
return x_3;
}
}
lean_object* l_Lean_Elab_withInfoHole_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
lean_object* x_4; lean_object* x_5;
lean_dec(x_3);
x_4 = lean_box(0);
x_5 = lean_apply_1(x_2, x_4);
return x_5;
}
else
{
lean_object* x_6; lean_object* x_7;
lean_dec(x_2);
x_6 = lean_ctor_get(x_1, 0);
lean_inc(x_6);
lean_dec(x_1);
x_7 = lean_apply_1(x_3, x_6);
return x_7;
}
}
}
lean_object* l_Lean_Elab_withInfoHole_match__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Lean_Elab_withInfoHole_match__1___rarg), 3, 0);
return x_3;
}
}
lean_object* l_Std_PersistentArray_getAux___at_Lean_Elab_withInfoHole___spec__2(lean_object* x_1, size_t x_2, size_t x_3) {
_start:
{
@ -5256,45 +5312,6 @@ return x_12;
}
}
}
static lean_object* _init_l_Lean_Elab_withInfoHole___rarg___lambda__1___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("s.trees.size == 1 -- if size is not one, then API is being misused.\n ");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_withInfoHole___rarg___lambda__1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Expr_instantiateBetaRevRange___closed__1;
x_2 = l_Lean_Elab_withInfoHole___rarg___lambda__1___closed__1;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_withInfoHole___rarg___lambda__1___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Lean.Elab.withInfoHole");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_withInfoHole___rarg___lambda__1___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_assignInfoHoleId___rarg___lambda__2___closed__3;
x_2 = l_Lean_Elab_withInfoHole___rarg___lambda__1___closed__3;
x_3 = lean_unsigned_to_nat(225u);
x_4 = lean_unsigned_to_nat(8u);
x_5 = l_Lean_Elab_withInfoHole___rarg___lambda__1___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
}
}
lean_object* l_Lean_Elab_withInfoHole___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -5307,70 +5324,69 @@ x_5 = lean_ctor_get(x_3, 0);
x_6 = lean_ctor_get(x_3, 1);
x_7 = lean_ctor_get(x_6, 2);
lean_inc(x_7);
x_8 = lean_unsigned_to_nat(1u);
x_9 = lean_nat_dec_eq(x_7, x_8);
lean_dec(x_7);
x_8 = lean_unsigned_to_nat(0u);
x_9 = lean_nat_dec_lt(x_8, x_7);
if (x_9 == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12;
lean_free_object(x_3);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
x_10 = l_Lean_Elab_instInhabitedInfoState;
x_11 = l_Lean_Elab_withInfoHole___rarg___lambda__1___closed__4;
x_12 = lean_panic_fn(x_10, x_11);
return x_12;
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
else
{
lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_13 = lean_unsigned_to_nat(0u);
x_14 = l_Std_PersistentArray_get_x21___at_Lean_Elab_withInfoHole___spec__1(x_6, x_13);
x_15 = l_Std_PersistentHashMap_insert___at_Lean_Elab_assignInfoHoleId___spec__1(x_5, x_1, x_14);
lean_ctor_set(x_3, 1, x_2);
lean_ctor_set(x_3, 0, x_15);
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_10 = lean_unsigned_to_nat(1u);
x_11 = lean_nat_sub(x_7, x_10);
lean_dec(x_7);
x_12 = l_Std_PersistentArray_get_x21___at_Lean_Elab_withInfoHole___spec__1(x_6, x_11);
lean_dec(x_11);
x_13 = l_Std_PersistentHashMap_insert___at_Lean_Elab_assignInfoHoleId___spec__1(x_5, x_2, x_12);
lean_ctor_set(x_3, 1, x_1);
lean_ctor_set(x_3, 0, x_13);
return x_3;
}
}
else
{
uint8_t x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; uint8_t x_21;
x_16 = lean_ctor_get_uint8(x_3, sizeof(void*)*2);
x_17 = lean_ctor_get(x_3, 0);
x_18 = lean_ctor_get(x_3, 1);
lean_inc(x_18);
lean_inc(x_17);
uint8_t x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; uint8_t x_19;
x_14 = lean_ctor_get_uint8(x_3, sizeof(void*)*2);
x_15 = lean_ctor_get(x_3, 0);
x_16 = lean_ctor_get(x_3, 1);
lean_inc(x_16);
lean_inc(x_15);
lean_dec(x_3);
x_19 = lean_ctor_get(x_18, 2);
lean_inc(x_19);
x_20 = lean_unsigned_to_nat(1u);
x_21 = lean_nat_dec_eq(x_19, x_20);
lean_dec(x_19);
if (x_21 == 0)
x_17 = lean_ctor_get(x_16, 2);
lean_inc(x_17);
x_18 = lean_unsigned_to_nat(0u);
x_19 = lean_nat_dec_lt(x_18, x_17);
if (x_19 == 0)
{
lean_object* x_22; lean_object* x_23; lean_object* x_24;
lean_dec(x_18);
lean_object* x_20;
lean_dec(x_17);
lean_dec(x_16);
lean_dec(x_2);
lean_dec(x_1);
x_22 = l_Lean_Elab_instInhabitedInfoState;
x_23 = l_Lean_Elab_withInfoHole___rarg___lambda__1___closed__4;
x_24 = lean_panic_fn(x_22, x_23);
return x_24;
x_20 = lean_alloc_ctor(0, 2, 1);
lean_ctor_set(x_20, 0, x_15);
lean_ctor_set(x_20, 1, x_1);
lean_ctor_set_uint8(x_20, sizeof(void*)*2, x_14);
return x_20;
}
else
{
lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28;
x_25 = lean_unsigned_to_nat(0u);
x_26 = l_Std_PersistentArray_get_x21___at_Lean_Elab_withInfoHole___spec__1(x_18, x_25);
x_27 = l_Std_PersistentHashMap_insert___at_Lean_Elab_assignInfoHoleId___spec__1(x_17, x_1, x_26);
x_28 = lean_alloc_ctor(0, 2, 1);
lean_ctor_set(x_28, 0, x_27);
lean_ctor_set(x_28, 1, x_2);
lean_ctor_set_uint8(x_28, sizeof(void*)*2, x_16);
return x_28;
lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_21 = lean_unsigned_to_nat(1u);
x_22 = lean_nat_sub(x_17, x_21);
lean_dec(x_17);
x_23 = l_Std_PersistentArray_get_x21___at_Lean_Elab_withInfoHole___spec__1(x_16, x_22);
lean_dec(x_22);
x_24 = l_Std_PersistentHashMap_insert___at_Lean_Elab_assignInfoHoleId___spec__1(x_15, x_2, x_23);
x_25 = lean_alloc_ctor(0, 2, 1);
lean_ctor_set(x_25, 0, x_24);
lean_ctor_set(x_25, 1, x_1);
lean_ctor_set_uint8(x_25, sizeof(void*)*2, x_14);
return x_25;
}
}
}
@ -5378,31 +5394,16 @@ return x_28;
lean_object* l_Lean_Elab_withInfoHole___rarg___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
if (lean_obj_tag(x_4) == 0)
{
lean_object* x_5; lean_object* x_6; lean_object* x_7;
lean_dec(x_3);
x_5 = lean_ctor_get(x_1, 1);
lean_inc(x_5);
lean_dec(x_1);
x_6 = lean_alloc_closure((void*)(l_Lean_Elab_withInfoContext_x27___rarg___lambda__1), 2, 1);
x_6 = lean_alloc_closure((void*)(l_Lean_Elab_withInfoHole___rarg___lambda__1), 3, 2);
lean_closure_set(x_6, 0, x_2);
lean_closure_set(x_6, 1, x_3);
x_7 = lean_apply_1(x_5, x_6);
return x_7;
}
else
{
lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_8 = lean_ctor_get(x_1, 1);
lean_inc(x_8);
lean_dec(x_1);
x_9 = lean_alloc_closure((void*)(l_Lean_Elab_withInfoHole___rarg___lambda__1), 3, 2);
lean_closure_set(x_9, 0, x_3);
lean_closure_set(x_9, 1, x_2);
x_10 = lean_apply_1(x_8, x_9);
return x_10;
}
}
}
lean_object* l_Lean_Elab_withInfoHole___rarg___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
@ -5769,14 +5770,6 @@ l_Lean_Elab_assignInfoHoleId___rarg___lambda__2___closed__4 = _init_l_Lean_Elab_
lean_mark_persistent(l_Lean_Elab_assignInfoHoleId___rarg___lambda__2___closed__4);
l_Lean_Elab_assignInfoHoleId___rarg___lambda__2___closed__5 = _init_l_Lean_Elab_assignInfoHoleId___rarg___lambda__2___closed__5();
lean_mark_persistent(l_Lean_Elab_assignInfoHoleId___rarg___lambda__2___closed__5);
l_Lean_Elab_withInfoHole___rarg___lambda__1___closed__1 = _init_l_Lean_Elab_withInfoHole___rarg___lambda__1___closed__1();
lean_mark_persistent(l_Lean_Elab_withInfoHole___rarg___lambda__1___closed__1);
l_Lean_Elab_withInfoHole___rarg___lambda__1___closed__2 = _init_l_Lean_Elab_withInfoHole___rarg___lambda__1___closed__2();
lean_mark_persistent(l_Lean_Elab_withInfoHole___rarg___lambda__1___closed__2);
l_Lean_Elab_withInfoHole___rarg___lambda__1___closed__3 = _init_l_Lean_Elab_withInfoHole___rarg___lambda__1___closed__3();
lean_mark_persistent(l_Lean_Elab_withInfoHole___rarg___lambda__1___closed__3);
l_Lean_Elab_withInfoHole___rarg___lambda__1___closed__4 = _init_l_Lean_Elab_withInfoHole___rarg___lambda__1___closed__4();
lean_mark_persistent(l_Lean_Elab_withInfoHole___rarg___lambda__1___closed__4);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

8
stage0/stdlib/Lean/Elab/LetRec.c generated
View file

@ -71,6 +71,7 @@ lean_object* lean_string_utf8_extract(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addDocString___at___private_Lean_Elab_LetRec_0__Lean_Elab_Term_mkLetRecDeclView___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_elabAttrs___at___private_Lean_Elab_LetRec_0__Lean_Elab_Term_mkLetRecDeclView___spec__14___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_string_utf8_byte_size(lean_object*);
lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_LetRec_0__Lean_Elab_Term_mkLetRecDeclView___spec__17___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_toAttributeKind___at___private_Lean_Elab_LetRec_0__Lean_Elab_Term_mkLetRecDeclView___spec__16___closed__1;
lean_object* l_Lean_Elab_toAttributeKind___at___private_Lean_Elab_LetRec_0__Lean_Elab_Term_mkLetRecDeclView___spec__16___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -154,11 +155,10 @@ extern lean_object* l_Lean_KernelException_toMessageData___closed__3;
size_t lean_usize_of_nat(lean_object*);
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_LetRec_0__Lean_Elab_Term_mkLetRecDeclView___spec__19___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_LetRec_0__Lean_Elab_Term_withAuxLocalDecls_loop___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__5___rarg(lean_object*);
lean_object* l_Array_mapIdxM_map_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Term_termElabAttribute;
lean_object* l___private_Lean_Elab_LetRec_0__Lean_Elab_Term_registerLetRecsToLift(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_throwUnsupportedSyntax___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__7___rarg(lean_object*);
lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__5(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_LetRec_0__Lean_Elab_Term_mkLetRecDeclView___spec__19___lambda__3___closed__1;
lean_object* l_Lean_Syntax_getPos_x3f(lean_object*, uint8_t);
lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_LetRec_0__Lean_Elab_Term_mkLetRecDeclView___spec__4___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1503,7 +1503,7 @@ x_75 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_75, 0, x_74);
x_76 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_76, 0, x_75);
x_77 = l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__5(x_73, x_76, x_2, x_3, x_4, x_5, x_6, x_7, x_50);
x_77 = l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__3(x_73, x_76, x_2, x_3, x_4, x_5, x_6, x_7, x_50);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_4);
@ -1537,7 +1537,7 @@ lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_82 = l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__7___rarg(x_50);
x_82 = l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__5___rarg(x_50);
x_83 = !lean_is_exclusive(x_82);
if (x_83 == 0)
{

177
stage0/stdlib/Lean/Elab/Match.c generated
View file

@ -136,6 +136,7 @@ lean_object* lean_local_ctx_erase(lean_object*, lean_object*);
lean_object* l_List_mapM___at_Lean_Elab_Term_ToDepElimPattern_main___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_anonymousCtor___elambda__1___closed__2;
lean_object* l_Lean_mkMVar(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__3;
extern lean_object* l_Array_empty___closed__1;
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_ToDepElimPattern_throwInvalidPattern___rarg___closed__2;
lean_object* lean_environment_find(lean_object*, lean_object*);
@ -147,17 +148,16 @@ extern lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_checkTypesAndAs
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_nameToPattern___closed__8;
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_processVar___lambda__3___closed__3;
lean_object* l_Lean_Elab_Term_CollectPatternVars_CtorApp_processCtorApp___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_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__3;
lean_object* l_List_forIn_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___spec__4___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_get(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_CollectPatternVars_processCtorApp_match__1___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__5;
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_nameToPattern___closed__17;
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabDiscrsWitMatchType___spec__1___lambda__1___closed__6;
extern lean_object* l_Lean_instInhabitedParserDescr___closed__1;
lean_object* l_Lean_Elab_Term_CollectPatternVars_CtorApp_processCtorApp___lambda__1___boxed__const__1;
uint8_t lean_name_eq(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabMatchAltView___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_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__5;
lean_object* l_Lean_Elab_Term_elabMatchAltView___lambda__1___closed__1;
lean_object* l_Lean_annotation_x3f(lean_object*, lean_object*);
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -218,6 +218,7 @@ lean_object* l_Lean_Elab_Term_elabMatch_elabMatchDefault___closed__2;
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_getMatchAlts___closed__1;
lean_object* lean_string_utf8_byte_size(lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_nameToPattern___closed__4;
lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_CollectPatternVars_CtorApp_processCtorApp(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Match_0__Lean_Elab_Term_withPatternVars_loop___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*, lean_object*);
lean_object* l_Lean_Meta_Match_mkMatcher(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -233,7 +234,6 @@ extern lean_object* l_Lean_rootNamespace___closed__2;
lean_object* l_List_forIn_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___spec__4___closed__1;
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_throwCtorExpected___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at___private_Lean_Elab_Match_0__Lean_Elab_Term_ToDepElimPattern_throwInvalidPattern___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName___closed__2;
lean_object* l_Lean_Elab_Term_CollectPatternVars_CtorApp_instInhabitedContext;
lean_object* l_Lean_throwError___at_Lean_Elab_Term_CollectPatternVars_CtorApp_processCtorApp___spec__5___boxed(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_Match_0__Lean_Elab_Term_getMatchAlts___spec__1___closed__2;
@ -259,6 +259,7 @@ lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_Ct
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_CollectPatternVars_main___spec__3___closed__1;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchTypeAndDiscrs_loop___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_finalizePatternDecls(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_isAuxDiscrName___closed__2;
lean_object* l_Lean_Elab_Term_getPatternsVars_match__1___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabMatch_elabMatchDefault___lambda__1___boxed(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_13855____closed__9;
@ -282,7 +283,6 @@ lean_object* l_Array_foldlMUnsafe___at_Array_foldl___spec__1___rarg(lean_object*
lean_object* l_Lean_throwError___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_nameToPattern___closed__21;
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_getPatternsVars___spec__3___rarg(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__4;
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_getDiscrs(lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_expandMacrosInPatterns___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_CollectPatternVars_collect_match__1(lean_object*);
@ -295,7 +295,9 @@ lean_object* l_Lean_Elab_Term_withDepElimPatterns___rarg___boxed__const__1;
lean_object* l_Lean_Syntax_mkApp(lean_object*, lean_object*);
lean_object* l___private_Lean_Expr_0__Lean_Expr_getAppArgsAux(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_ToDepElimPattern_mkLocalDeclFor_match__2(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__4;
lean_object* l_Lean_LocalDecl_value(lean_object*);
uint8_t l_Lean_Name_hasMacroScopes(lean_object*);
lean_object* l_Lean_Elab_Term_elabMatchAltView(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_tryPostponeIfNoneOrMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_withPatternVars_loop_match__1(lean_object*);
@ -346,10 +348,13 @@ lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_CollectPatternVars_CtorApp_processCtorApp_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_Pattern_toExpr_visit(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_nameToPattern___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_isAuxDiscrName___boxed(lean_object*);
extern lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_solveSelfMax___closed__1;
uint8_t l_Lean_Elab_Term_isAuxDiscrName(lean_object*);
extern lean_object* l_Lean_strLitKind;
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_nameToPattern___closed__1;
lean_object* l_Lean_Elab_Term_ToDepElimPattern_main_match__4(lean_object*);
lean_object* l_Lean_Elab_Term_isAuxDiscrName___closed__1;
lean_object* l_Lean_Elab_Term_withDepElimPatterns___rarg___closed__2;
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingImp___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Meta_0__Array_mapSepElemsMAux___at_Lean_Elab_Term_CollectPatternVars_collect___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*, lean_object*);
@ -400,7 +405,6 @@ lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_getDiscrs___boxed(lea
lean_object* l_Lean_Elab_Term_CollectPatternVars_collect___closed__11;
lean_object* l_Nat_repr(lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___lambda__1___boxed__const__1;
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__1;
lean_object* l_Lean_Elab_Term_elabMatch_elabMatchDefault___closed__1;
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Array_forInUnsafe_loop___at_Lean_pushScope___spec__1___rarg___lambda__1___closed__1;
@ -413,6 +417,7 @@ lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_expandNonAtomicDiscrs
extern lean_object* l_Lean_Syntax_getHead_x3f___closed__4;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_14424____closed__1;
lean_object* l_Lean_Elab_Term_inaccessible_x3f___boxed(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__1;
lean_object* l_Lean_Syntax_getId(lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_getMatchOptType(lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_throwInvalidPattern___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -434,6 +439,7 @@ lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_expandNonAtomicDiscrs
extern lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__2;
lean_object* l_Lean_Elab_Term_finalizePatternDecls_match__2(lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_CtorApp_processCtorAppAux_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__2;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_2191____closed__2;
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___spec__9(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabDiscrsWitMatchType___spec__1___lambda__1___closed__4;
@ -448,7 +454,6 @@ lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchTypeAndDiscr
lean_object* l___regBuiltin_Lean_Elab_Term_elabNoMatch___closed__1;
lean_object* l_Lean_Elab_Term_CollectPatternVars_collect___closed__10;
extern lean_object* l___private_Init_Meta_0__Lean_quoteName___closed__2;
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__2;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_CollectPatternVars_processCtorApp(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_throwUnsupportedSyntax___at_Lean_Elab_Term_getPatternsVars___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -474,7 +479,6 @@ lean_object* l___private_Init_Util_0__mkPanicMessageWithDecl(lean_object*, lean_
lean_object* l_Array_reverse___rarg(lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_processVar___lambda__2___closed__4;
lean_object* l_Lean_Elab_Term_ToDepElimPattern_State_found___default;
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1486____closed__1;
extern lean_object* l_Lean_KernelException_toMessageData___closed__15;
uint8_t l_Array_isEmpty___rarg(lean_object*);
extern lean_object* l_Lean_instInhabitedLocalDecl;
@ -489,7 +493,6 @@ lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_expandMacrosInPatterns__
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_expandNonAtomicDiscrs_x3f_loop___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_mkUserNameFor_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_inaccessible_x3f(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1486____closed__2;
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_isMatchUnit_x3f_match__1(lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_ToDepElimPattern_throwInvalidPattern___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_bind___at_Lean_Elab_Term_instMonadLogTermElabM___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -502,9 +505,9 @@ lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_pr
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_CtorApp_pushNewArg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkFVar(lean_object*);
uint8_t l_List_elem___at_Lean_Occurrences_contains___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1489____closed__2;
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_getMVarSyntaxMVarId___boxed(lean_object*);
lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___spec__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName(lean_object*);
lean_object* l_Lean_Elab_Term_finalizePatternDecls_match__2___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_KernelException_toMessageData___closed__3;
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabAtomicDiscr___closed__1;
@ -526,6 +529,7 @@ lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_ToDepElimPattern_alre
lean_object* l_List_forIn_loop___at_Lean_Elab_Term_reportMatcherResultErrors___spec__1___closed__1;
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___closed__4;
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_withPatternVars_loop_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__5___rarg(lean_object*);
extern lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__5;
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabAtomicDiscr(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_LocalDecl_fvarId(lean_object*);
@ -543,17 +547,16 @@ lean_object* l_Lean_throwError___at___private_Lean_Elab_Match_0__Lean_Elab_Term_
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_tryPostponeIfDiscrTypeIsMVar___spec__1___closed__1;
extern lean_object* l_Lean_Elab_Term_termElabAttribute;
extern lean_object* l_Lean_Syntax_getHead_x3f___closed__3;
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1489____closed__1;
lean_object* l_Lean_Elab_Term_instToStringPatternVar(lean_object*);
lean_object* l_Lean_mkAtomFrom(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_waitExpectedType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__7___rarg(lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_expandMacrosInPatterns___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_CollectPatternVars_processCtor(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_LocalDecl_type(lean_object*);
lean_object* l_Std_Range_forIn_loop___at___private_Lean_Elab_App_0__Lean_Elab_Term_addLValArg___spec__2___lambda__1___boxed(lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_finalizePatternDecls___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Match_0__Lean_Elab_Term_getMatchAlts___spec__1___closed__3;
lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_Alt_checkAndReplaceFVarId___lambda__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_reportMatcherResultErrors___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_synthesizeSyntheticMVarsUsingDefault(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -698,7 +701,6 @@ lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_withElaboratedLHS_mat
uint8_t l_Lean_Syntax_isNone(lean_object*);
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
lean_object* l_Lean_Meta_inferType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName___boxed(lean_object*);
lean_object* l_Lean_expandMacros(lean_object*, lean_object*, lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_1398____closed__8;
lean_object* l_List_forIn_loop___at_Lean_Elab_Term_reportMatcherResultErrors___spec__1___closed__2;
@ -710,7 +712,6 @@ lean_object* l_List_forIn_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_
lean_object* l_Lean_throwError___at___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_processVar___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_isPatternVar_match__3(lean_object*);
lean_object* l_Lean_mkFreshId___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_FunBinders_elabFunBinderViews___spec__1___rarg(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName___closed__1;
uint8_t l_Lean_Expr_hasLooseBVars(lean_object*);
lean_object* l_Lean_Elab_Term_elabMatch_elabMatchDefault___closed__4;
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_mkMVarSyntax___rarg___boxed(lean_object*, lean_object*);
@ -833,10 +834,10 @@ lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux_match__3
lean_object* l_Lean_Elab_Term_isLocalIdent_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_forIn_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___spec__4___lambda__1___closed__1;
lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_Closure_mkBinding___spec__1(size_t, size_t, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_8715_(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1486_(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_8718_(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1489_(lean_object*);
lean_object* l_Lean_Elab_Term_CollectPatternVars_CtorApp_Context_paramDeclIdx___default;
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990_(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993_(lean_object*);
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_reportMatcherResultErrors___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkSimpleThunk(lean_object*);
@ -2133,7 +2134,7 @@ lean_dec(x_3);
return x_9;
}
}
static lean_object* _init_l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName___closed__1() {
static lean_object* _init_l_Lean_Elab_Term_isAuxDiscrName___closed__1() {
_start:
{
lean_object* x_1;
@ -2141,32 +2142,44 @@ x_1 = lean_mk_string("_discr");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName___closed__2() {
static lean_object* _init_l_Lean_Elab_Term_isAuxDiscrName___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName___closed__1;
x_2 = l_Lean_Elab_Term_isAuxDiscrName___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
uint8_t l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName(lean_object* x_1) {
uint8_t l_Lean_Elab_Term_isAuxDiscrName(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4;
x_2 = lean_erase_macro_scopes(x_1);
x_3 = l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName___closed__2;
x_4 = lean_name_eq(x_2, x_3);
lean_dec(x_2);
return x_4;
uint8_t x_2;
x_2 = l_Lean_Name_hasMacroScopes(x_1);
if (x_2 == 0)
{
uint8_t x_3;
lean_dec(x_1);
x_3 = 0;
return x_3;
}
else
{
lean_object* x_4; lean_object* x_5; uint8_t x_6;
x_4 = lean_erase_macro_scopes(x_1);
x_5 = l_Lean_Elab_Term_isAuxDiscrName___closed__2;
x_6 = lean_name_eq(x_4, x_5);
lean_dec(x_4);
return x_6;
}
}
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName___boxed(lean_object* x_1) {
}
lean_object* l_Lean_Elab_Term_isAuxDiscrName___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName(x_1);
x_2 = l_Lean_Elab_Term_isAuxDiscrName(x_1);
x_3 = lean_box(x_2);
return x_3;
}
@ -2289,7 +2302,7 @@ if (x_20 == 0)
lean_object* x_21; lean_object* x_22; uint8_t x_23;
x_21 = lean_ctor_get(x_19, 0);
x_22 = l_Lean_LocalDecl_userName(x_21);
x_23 = l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName(x_22);
x_23 = l_Lean_Elab_Term_isAuxDiscrName(x_22);
if (x_23 == 0)
{
lean_dec(x_21);
@ -2315,7 +2328,7 @@ lean_inc(x_26);
lean_inc(x_25);
lean_dec(x_19);
x_27 = l_Lean_LocalDecl_userName(x_25);
x_28 = l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName(x_27);
x_28 = l_Lean_Elab_Term_isAuxDiscrName(x_27);
if (x_28 == 0)
{
lean_object* x_29;
@ -3860,7 +3873,7 @@ return x_11;
}
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1486____closed__1() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1489____closed__1() {
_start:
{
lean_object* x_1;
@ -3868,21 +3881,21 @@ x_1 = lean_mk_string("MVarWithIdKind");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1486____closed__2() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1489____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1486____closed__1;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1489____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1486_(lean_object* x_1) {
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1489_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1486____closed__2;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1489____closed__2;
x_3 = l_Lean_Parser_registerBuiltinNodeKind(x_2, x_1);
return x_3;
}
@ -3903,7 +3916,7 @@ lean_ctor_set(x_7, 0, x_5);
lean_ctor_set(x_7, 1, x_6);
x_8 = l_Lean_mkOptionalNode___closed__2;
x_9 = lean_array_push(x_8, x_7);
x_10 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1486____closed__2;
x_10 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1489____closed__2;
x_11 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_11, 0, x_10);
lean_ctor_set(x_11, 1, x_9);
@ -3924,7 +3937,7 @@ lean_ctor_set(x_15, 0, x_12);
lean_ctor_set(x_15, 1, x_14);
x_16 = l_Lean_mkOptionalNode___closed__2;
x_17 = lean_array_push(x_16, x_15);
x_18 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1486____closed__2;
x_18 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1489____closed__2;
x_19 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_19, 0, x_18);
lean_ctor_set(x_19, 1, x_17);
@ -4026,7 +4039,7 @@ _start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_Elab_Term_termElabAttribute;
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1486____closed__2;
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1489____closed__2;
x_4 = l___regBuiltin_Lean_Elab_Term_elabMVarWithIdKind___closed__1;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
@ -15732,7 +15745,7 @@ x_71 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_71, 0, x_70);
x_72 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_72, 0, x_71);
x_73 = l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__5(x_69, x_72, x_2, x_3, x_4, x_5, x_6, x_7, x_46);
x_73 = l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__3(x_69, x_72, x_2, x_3, x_4, x_5, x_6, x_7, x_46);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_4);
@ -15766,7 +15779,7 @@ lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_78 = l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__7___rarg(x_46);
x_78 = l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__5___rarg(x_46);
x_79 = !lean_is_exclusive(x_78);
if (x_79 == 0)
{
@ -22322,7 +22335,7 @@ lean_dec(x_5);
return x_12;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__1() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -22332,7 +22345,7 @@ x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__2() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__2() {
_start:
{
lean_object* x_1;
@ -22340,17 +22353,17 @@ x_1 = lean_mk_string("ignoreUnusedAlts");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__3() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__1;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__2;
x_1 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__1;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__2;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__4() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__4() {
_start:
{
lean_object* x_1;
@ -22358,13 +22371,13 @@ x_1 = lean_mk_string("if true, do not generate error if an alternative is not us
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__5() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__5() {
_start:
{
uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = 0;
x_2 = l_Lean_instInhabitedParserDescr___closed__1;
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__4;
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__4;
x_4 = lean_box(x_1);
x_5 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_5, 0, x_4);
@ -22373,12 +22386,12 @@ lean_ctor_set(x_5, 2, x_3);
return x_5;
}
}
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990_(lean_object* x_1) {
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__3;
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__5;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__3;
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__5;
x_4 = l_Lean_Option_register___at_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_4____spec__1(x_2, x_3, x_1);
return x_4;
}
@ -26540,7 +26553,7 @@ x_26 = lean_ctor_get(x_24, 1);
lean_inc(x_26);
lean_dec(x_24);
x_27 = lean_array_get_size(x_20);
x_28 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__1;
x_28 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__1;
lean_inc(x_5);
x_29 = l_Lean_Elab_Term_mkAuxName(x_28, x_5, x_6, x_7, x_8, x_9, x_10, x_26);
if (lean_obj_tag(x_29) == 0)
@ -27350,7 +27363,7 @@ static lean_object* _init_l___private_Lean_Elab_Match_0__Lean_Elab_Term_expandNo
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName___closed__1;
x_1 = l_Lean_Elab_Term_isAuxDiscrName___closed__1;
x_2 = lean_string_utf8_byte_size(x_1);
return x_2;
}
@ -27359,7 +27372,7 @@ static lean_object* _init_l___private_Lean_Elab_Match_0__Lean_Elab_Term_expandNo
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName___closed__1;
x_1 = l_Lean_Elab_Term_isAuxDiscrName___closed__1;
x_2 = lean_unsigned_to_nat(0u);
x_3 = l___private_Lean_Elab_Match_0__Lean_Elab_Term_expandNonAtomicDiscrs_x3f_loop___closed__1;
x_4 = lean_alloc_ctor(0, 3, 0);
@ -27479,7 +27492,7 @@ lean_inc(x_41);
x_42 = lean_ctor_get(x_40, 1);
lean_inc(x_42);
lean_dec(x_40);
x_43 = l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName___closed__2;
x_43 = l_Lean_Elab_Term_isAuxDiscrName___closed__2;
x_44 = l_Lean_addMacroScope(x_41, x_43, x_38);
x_45 = lean_box(0);
x_46 = l___private_Lean_Elab_Match_0__Lean_Elab_Term_expandNonAtomicDiscrs_x3f_loop___closed__2;
@ -27489,7 +27502,7 @@ lean_ctor_set(x_47, 1, x_46);
lean_ctor_set(x_47, 2, x_44);
lean_ctor_set(x_47, 3, x_45);
x_48 = l_Lean_Syntax_getId(x_47);
x_49 = l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName(x_48);
x_49 = l_Lean_Elab_Term_isAuxDiscrName(x_48);
if (x_49 == 0)
{
lean_object* x_50; lean_object* x_51; uint8_t x_52;
@ -27580,7 +27593,7 @@ lean_inc(x_76);
x_77 = lean_ctor_get(x_75, 1);
lean_inc(x_77);
lean_dec(x_75);
x_78 = l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName___closed__2;
x_78 = l_Lean_Elab_Term_isAuxDiscrName___closed__2;
x_79 = l_Lean_addMacroScope(x_76, x_78, x_73);
x_80 = lean_box(0);
x_81 = l___private_Lean_Elab_Match_0__Lean_Elab_Term_expandNonAtomicDiscrs_x3f_loop___closed__2;
@ -27590,7 +27603,7 @@ lean_ctor_set(x_82, 1, x_81);
lean_ctor_set(x_82, 2, x_79);
lean_ctor_set(x_82, 3, x_80);
x_83 = l_Lean_Syntax_getId(x_82);
x_84 = l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName(x_83);
x_84 = l_Lean_Elab_Term_isAuxDiscrName(x_83);
if (x_84 == 0)
{
lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90;
@ -27720,7 +27733,7 @@ lean_inc(x_120);
x_121 = lean_ctor_get(x_119, 1);
lean_inc(x_121);
lean_dec(x_119);
x_122 = l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName___closed__2;
x_122 = l_Lean_Elab_Term_isAuxDiscrName___closed__2;
x_123 = l_Lean_addMacroScope(x_120, x_122, x_117);
x_124 = lean_box(0);
x_125 = l___private_Lean_Elab_Match_0__Lean_Elab_Term_expandNonAtomicDiscrs_x3f_loop___closed__2;
@ -27730,7 +27743,7 @@ lean_ctor_set(x_126, 1, x_125);
lean_ctor_set(x_126, 2, x_123);
lean_ctor_set(x_126, 3, x_124);
x_127 = l_Lean_Syntax_getId(x_126);
x_128 = l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName(x_127);
x_128 = l_Lean_Elab_Term_isAuxDiscrName(x_127);
if (x_128 == 0)
{
lean_object* x_129; lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; lean_object* x_134;
@ -30533,7 +30546,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_Match___hyg_8715_(lean_object* x_1) {
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_8718_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -30705,10 +30718,10 @@ l_Array_forInUnsafe_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabDi
lean_mark_persistent(l_Array_forInUnsafe_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabDiscrsWitMatchType___spec__1___lambda__1___closed__7);
l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabDiscrsWitMatchType___closed__1 = _init_l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabDiscrsWitMatchType___closed__1();
lean_mark_persistent(l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabDiscrsWitMatchType___closed__1);
l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName___closed__1 = _init_l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName___closed__1();
lean_mark_persistent(l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName___closed__1);
l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName___closed__2 = _init_l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName___closed__2();
lean_mark_persistent(l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName___closed__2);
l_Lean_Elab_Term_isAuxDiscrName___closed__1 = _init_l_Lean_Elab_Term_isAuxDiscrName___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_isAuxDiscrName___closed__1);
l_Lean_Elab_Term_isAuxDiscrName___closed__2 = _init_l_Lean_Elab_Term_isAuxDiscrName___closed__2();
lean_mark_persistent(l_Lean_Elab_Term_isAuxDiscrName___closed__2);
l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabAtomicDiscr___closed__1 = _init_l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabAtomicDiscr___closed__1();
lean_mark_persistent(l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabAtomicDiscr___closed__1);
l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabAtomicDiscr___closed__2 = _init_l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabAtomicDiscr___closed__2();
@ -30729,11 +30742,11 @@ l___private_Lean_Elab_Match_0__Lean_Elab_Term_getMatchAlts___closed__1 = _init_l
lean_mark_persistent(l___private_Lean_Elab_Match_0__Lean_Elab_Term_getMatchAlts___closed__1);
l_Lean_Elab_Term_instToStringPatternVar___closed__1 = _init_l_Lean_Elab_Term_instToStringPatternVar___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_instToStringPatternVar___closed__1);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1486____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1486____closed__1();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1486____closed__1);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1486____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1486____closed__2();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1486____closed__2);
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1486_(lean_io_mk_world());
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1489____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1489____closed__1();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1489____closed__1);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1489____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1489____closed__2();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1489____closed__2);
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_1489_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___regBuiltin_Lean_Elab_Term_elabMVarWithIdKind___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_elabMVarWithIdKind___closed__1();
@ -30938,17 +30951,17 @@ l_Lean_Elab_Term_elabMatchAltView___closed__1 = _init_l_Lean_Elab_Term_elabMatch
lean_mark_persistent(l_Lean_Elab_Term_elabMatchAltView___closed__1);
l_Lean_Elab_Term_elabMatchAltView___closed__2 = _init_l_Lean_Elab_Term_elabMatchAltView___closed__2();
lean_mark_persistent(l_Lean_Elab_Term_elabMatchAltView___closed__2);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__1();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__1);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__2();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__2);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__3 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__3();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__3);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__4 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__4();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__4);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__5 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__5();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__5);
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990_(lean_io_mk_world());
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__1();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__1);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__2();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__2);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__3 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__3();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__3);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__4 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__4();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__4);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__5 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__5();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__5);
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
l_Lean_Elab_Term_match_ignoreUnusedAlts = lean_io_result_get_value(res);
lean_mark_persistent(l_Lean_Elab_Term_match_ignoreUnusedAlts);
@ -31032,7 +31045,7 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabMatch___closed__1);
res = l___regBuiltin_Lean_Elab_Term_elabMatch(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_Match___hyg_8715_(lean_io_mk_world());
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_8718_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_Term_elabNoMatch___closed__1 = _init_l_Lean_Elab_Term_elabNoMatch___closed__1();

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

@ -179,6 +179,7 @@ lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsA
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabFunValues___spec__2___lambda__1___boxed(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_check___lambda__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_string_utf8_byte_size(lean_object*);
lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__3(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_Lean_LocalContext_getFVars___spec__1(size_t, size_t, lean_object*);
extern lean_object* l_Lean_Parser_Command_example___elambda__1___closed__2;
lean_object* l_Lean_Elab_Term_withLevelNames___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -200,7 +201,6 @@ lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_typeHasRecFun_mat
lean_object* l_Lean_Elab_expandDeclId___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___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* l_Array_mapMUnsafe_map___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabFunValues___spec__2(size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_MutualClosure_getModifiersForLetRecs___lambda__2___boxed(lean_object*);
lean_object* l_Lean_throwError___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_MutualClosure_Replacement_apply_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabTypeWithAutoBoundImplicit___rarg(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_check___lambda__5___closed__1;
@ -399,6 +399,7 @@ lean_object* l___private_Init_Util_0__mkPanicMessageWithDecl(lean_object*, lean_
lean_object* l_Array_reverse___rarg(lean_object*);
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_check___lambda__7(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_getAllUserLevelNames___boxed(lean_object*);
lean_object* l_Lean_throwError___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
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;
@ -444,6 +445,7 @@ lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_MutualDef_0__Lean
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabFunValues___spec__2___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_MutualClosure_pushMain___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_expr_update_proj(lean_object*, lean_object*);
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__5___rarg(lean_object*);
lean_object* l_Lean_PersistentEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabBinders___rarg___boxed(lean_object*, 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_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___spec__3(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
@ -459,10 +461,8 @@ lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_Fix
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_checkModifiers___closed__1;
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_isExample___closed__1;
size_t l_USize_mod(size_t, size_t);
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__7___rarg(lean_object*);
lean_object* l_Lean_Elab_Term_MutualClosure_ClosureState_localDecls___default;
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_FixPoint_getUsedFVarsMap(lean_object*);
lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__5(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_checkLetRecsToLiftTypes___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* l_Array_mapMUnsafe_map___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___spec__2___lambda__4(size_t, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Command_elabMutualDef___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -7265,7 +7265,7 @@ x_48 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_48, 0, x_47);
x_49 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_49, 0, x_48);
x_50 = l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__5(x_46, x_49, x_3, x_4, x_5, x_6, x_7, x_8, x_18);
x_50 = l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__3(x_46, x_49, x_3, x_4, x_5, x_6, x_7, x_8, x_18);
lean_dec(x_46);
return x_50;
}
@ -7274,7 +7274,7 @@ else
lean_object* x_51;
lean_dec(x_7);
lean_dec(x_3);
x_51 = l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__7___rarg(x_18);
x_51 = l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__5___rarg(x_18);
return x_51;
}
}
@ -9300,7 +9300,7 @@ x_11 = lean_ctor_get(x_7, 3);
x_12 = l_Lean_replaceRef(x_1, x_11);
lean_dec(x_11);
lean_ctor_set(x_7, 3, x_12);
x_13 = l_Lean_throwError___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__8(x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
x_13 = l_Lean_throwError___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__6(x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
lean_dec(x_7);
return x_13;
}
@ -9335,7 +9335,7 @@ lean_ctor_set(x_23, 4, x_18);
lean_ctor_set(x_23, 5, x_19);
lean_ctor_set(x_23, 6, x_20);
lean_ctor_set(x_23, 7, x_21);
x_24 = l_Lean_throwError___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__8(x_2, x_3, x_4, x_5, x_6, x_23, x_8, x_9);
x_24 = l_Lean_throwError___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__6(x_2, x_3, x_4, x_5, x_6, x_23, x_8, x_9);
lean_dec(x_23);
return x_24;
}

10
stage0/stdlib/Lean/Elab/Quotation.c generated
View file

@ -273,6 +273,7 @@ extern lean_object* l_Std_Format_paren___closed__2;
lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__22___closed__6;
lean_object* lean_string_utf8_byte_size(lean_object*);
lean_object* l_ReaderT_pure___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_pure___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__2(lean_object*);
extern lean_object* l_instReprProd___rarg___closed__1;
lean_object* l_Lean_Elab_Term_Quotation_getPatternsVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -667,7 +668,6 @@ extern lean_object* l_term_x2d_____closed__3;
lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__25;
lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo_match__10___rarg(lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_Quotation_match__syntax_expand___spec__6___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_instToMessageDataOption___rarg___closed__3;
lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__10___closed__5;
extern lean_object* l_Lean_Parser_Term_funBinder_quot___elambda__1___closed__3;
@ -6282,7 +6282,7 @@ lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
x_122 = l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___lambda__5___closed__12;
x_123 = l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__5(x_9, x_122, x_10, x_11, x_12, x_13, x_14, x_15, x_16);
x_123 = l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__3(x_9, x_122, x_10, x_11, x_12, x_13, x_14, x_15, x_16);
lean_dec(x_15);
lean_dec(x_13);
lean_dec(x_12);
@ -6347,7 +6347,7 @@ x_140 = l_Lean_KernelException_toMessageData___closed__3;
x_141 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_141, 0, x_139);
lean_ctor_set(x_141, 1, x_140);
x_142 = l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__5(x_9, x_141, x_10, x_11, x_12, x_13, x_14, x_15, x_16);
x_142 = l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__3(x_9, x_141, x_10, x_11, x_12, x_13, x_14, x_15, x_16);
lean_dec(x_15);
lean_dec(x_13);
lean_dec(x_12);
@ -7244,7 +7244,7 @@ x_534 = l_Lean_KernelException_toMessageData___closed__3;
x_535 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_535, 0, x_533);
lean_ctor_set(x_535, 1, x_534);
x_536 = l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__5(x_9, x_535, x_10, x_11, x_12, x_13, x_14, x_15, x_16);
x_536 = l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__3(x_9, x_535, x_10, x_11, x_12, x_13, x_14, x_15, x_16);
lean_dec(x_15);
lean_dec(x_13);
lean_dec(x_12);
@ -7281,7 +7281,7 @@ x_544 = l_Lean_KernelException_toMessageData___closed__3;
x_545 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_545, 0, x_543);
lean_ctor_set(x_545, 1, x_544);
x_546 = l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__5(x_9, x_545, x_10, x_11, x_12, x_13, x_14, x_15, x_16);
x_546 = l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__3(x_9, x_545, x_10, x_11, x_12, x_13, x_14, x_15, x_16);
lean_dec(x_15);
lean_dec(x_13);
lean_dec(x_12);

8
stage0/stdlib/Lean/Elab/Structure.c generated
View file

@ -192,6 +192,7 @@ lean_object* l_Lean_Elab_Command_accLevelAtCtor(lean_object*, lean_object*, lean
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_addCtorFields_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_myMacro____x40_Init_NotationExtra___hyg_5658____closed__20;
lean_object* lean_string_utf8_byte_size(lean_object*);
lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_checkValidFieldModifier___lambda__2___closed__2;
extern lean_object* l_Lean_MetavarContext_instantiateLevelMVars___at_Lean_Meta_instantiateLevelMVars___spec__1___closed__4;
extern lean_object* l_Lean_Parser_Command_example___elambda__1___closed__2;
@ -448,6 +449,7 @@ lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectLevelPa
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___lambda__4(lean_object*, 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* l_Lean_throwError___at_Lean_Elab_Command_elabStructure___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_addProjections(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__5___rarg(lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withParents(lean_object*);
lean_object* l_Lean_PersistentEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabBinders___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -467,14 +469,12 @@ lean_object* l_Lean_Meta_mkProjection(lean_object*, lean_object*, lean_object*,
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabFieldTypeValue_match__1(lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_processSubfields_loop___rarg___closed__1;
lean_object* l_Lean_mkAtomFrom(lean_object*, lean_object*);
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__7___rarg(lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_levelMVarToParamAux___boxed__const__1;
lean_object* l_Lean_Elab_elabDeclAttrs___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_LocalDecl_type(lean_object*);
lean_object* l_Array_filterM___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__5___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields___rarg___closed__3;
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_levelMVarToParamAux___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_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUsed___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_levelMVarToParam_x27(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields___spec__5___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1333,7 +1333,7 @@ x_75 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_75, 0, x_74);
x_76 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_76, 0, x_75);
x_77 = l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__5(x_73, x_76, x_2, x_3, x_4, x_5, x_6, x_7, x_50);
x_77 = l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__3(x_73, x_76, x_2, x_3, x_4, x_5, x_6, x_7, x_50);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_4);
@ -1367,7 +1367,7 @@ lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_82 = l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__7___rarg(x_50);
x_82 = l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__5___rarg(x_50);
x_83 = !lean_is_exclusive(x_82);
if (x_83 == 0)
{

1705
stage0/stdlib/Lean/Elab/SyntheticMVars.c generated
View file

File diff suppressed because it is too large Load diff

3356
stage0/stdlib/Lean/Elab/Tactic/Basic.c generated
View file

File diff suppressed because it is too large Load diff

41
stage0/stdlib/Lean/Elab/Tactic/ElabTerm.c generated
View file

@ -48,6 +48,7 @@ lean_object* l_Lean_Elab_Tactic_elabTermWithHoles___lambda__2___boxed(lean_objec
lean_object* l_Lean_Elab_Tactic_refineCore_match__1___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_elabTermWithHoles___lambda__2(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___regBuiltin_Lean_Elab_Tactic_evalExistsIntro___closed__1;
lean_object* l_Lean_Elab_Term_ensureHasType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalExistsIntro(lean_object*);
lean_object* l_Lean_Meta_apply(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_elabTerm___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -102,6 +103,7 @@ lean_object* l_Lean_Elab_Tactic_refineCore_match__1(lean_object*);
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_elabAsFVar_match__2(lean_object*);
extern lean_object* l_Lean_Elab_Tactic_evalIntro___closed__4;
lean_object* l_ReaderT_bind___at_Lean_Elab_Tactic_liftMetaTacticAux___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*);
lean_object* l_Lean_Elab_Tactic_refineCore_match__2(lean_object*);
lean_object* l_Lean_Elab_Tactic_setGoals(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_elabTerm___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -119,7 +121,6 @@ lean_object* l___regBuiltin_Lean_Elab_Tactic_evalApply(lean_object*);
lean_object* l_Lean_Elab_Tactic_evalWithReducibleAndInstances___boxed(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_Tactic_refineCore___lambda__1(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getMVarDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_ensureHasType(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_Tactic_elabAsFVar_match__1___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Meta_instantiateMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalApply___closed__1;
@ -128,7 +129,6 @@ uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_withoutErrToSorry___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalRefineBang___closed__1;
extern lean_object* l_Lean_Parser_Tactic_exact___closed__2;
lean_object* l_ReaderT_bind___at_Lean_Elab_Tactic_withMacroExpansion___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_elabTermWithHoles___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_Lean_Elab_Tactic_elabTermWithHoles___closed__2;
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalRefine___closed__1;
@ -299,18 +299,19 @@ lean_inc(x_2);
x_13 = l_Lean_Elab_Tactic_elabTerm(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12);
if (lean_obj_tag(x_13) == 0)
{
lean_object* x_14; lean_object* x_15; lean_object* x_16;
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_14 = lean_ctor_get(x_13, 0);
lean_inc(x_14);
x_15 = lean_ctor_get(x_13, 1);
lean_inc(x_15);
lean_dec(x_13);
x_16 = l_Lean_Elab_Tactic_ensureHasType(x_2, x_14, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_15);
return x_16;
x_16 = lean_box(0);
x_17 = l_Lean_Elab_Term_ensureHasType(x_2, x_14, x_16, x_6, x_7, x_8, x_9, x_10, x_11, x_15);
return x_17;
}
else
{
uint8_t x_17;
uint8_t x_18;
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_9);
@ -318,23 +319,23 @@ lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_2);
x_17 = !lean_is_exclusive(x_13);
if (x_17 == 0)
x_18 = !lean_is_exclusive(x_13);
if (x_18 == 0)
{
return x_13;
}
else
{
lean_object* x_18; lean_object* x_19; lean_object* x_20;
x_18 = lean_ctor_get(x_13, 0);
x_19 = lean_ctor_get(x_13, 1);
lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_19 = lean_ctor_get(x_13, 0);
x_20 = lean_ctor_get(x_13, 1);
lean_inc(x_20);
lean_inc(x_19);
lean_inc(x_18);
lean_dec(x_13);
x_20 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_20, 0, x_18);
lean_ctor_set(x_20, 1, x_19);
return x_20;
x_21 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_21, 0, x_19);
lean_ctor_set(x_21, 1, x_20);
return x_21;
}
}
}
@ -532,7 +533,7 @@ lean_inc(x_19);
x_22 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalExact___lambda__2___boxed), 12, 2);
lean_closure_set(x_22, 0, x_15);
lean_closure_set(x_22, 1, x_19);
x_23 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_withMacroExpansion___spec__2___rarg), 11, 2);
x_23 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_liftMetaTacticAux___spec__1___rarg), 11, 2);
lean_closure_set(x_23, 0, x_21);
lean_closure_set(x_23, 1, x_22);
lean_inc(x_9);
@ -1833,7 +1834,7 @@ lean_closure_set(x_20, 1, x_2);
lean_closure_set(x_20, 2, x_19);
lean_closure_set(x_20, 3, x_16);
lean_closure_set(x_20, 4, x_17);
x_21 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_withMacroExpansion___spec__2___rarg), 11, 2);
x_21 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_liftMetaTacticAux___spec__1___rarg), 11, 2);
lean_closure_set(x_21, 0, x_18);
lean_closure_set(x_21, 1, x_20);
x_22 = l_Lean_Meta_withMVarContext___at_Lean_Elab_Tactic_withMainMVarContext___spec__1___rarg(x_16, x_21, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_15);
@ -2205,7 +2206,7 @@ x_18 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalApplyLikeTactic___lambd
lean_closure_set(x_18, 0, x_2);
lean_closure_set(x_18, 1, x_1);
lean_closure_set(x_18, 2, x_15);
x_19 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_withMacroExpansion___spec__2___rarg), 11, 2);
x_19 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_liftMetaTacticAux___spec__1___rarg), 11, 2);
lean_closure_set(x_19, 0, x_17);
lean_closure_set(x_19, 1, x_18);
lean_inc(x_10);
@ -3475,7 +3476,7 @@ x_21 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_elabAsFVar___lambda__1___bo
lean_closure_set(x_21, 0, x_2);
lean_closure_set(x_21, 1, x_15);
lean_closure_set(x_21, 2, x_16);
x_22 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_withMacroExpansion___spec__2___rarg), 11, 2);
x_22 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_liftMetaTacticAux___spec__1___rarg), 11, 2);
lean_closure_set(x_22, 0, x_20);
lean_closure_set(x_22, 1, x_21);
x_23 = l_Lean_Meta_withMVarContext___at_Lean_Elab_Tactic_withMainMVarContext___spec__1___rarg(x_15, x_22, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_14);

16
stage0/stdlib/Lean/Elab/Tactic/Generalize.c generated
View file

@ -52,6 +52,7 @@ lean_object* l_Lean_Elab_Tactic_evalGeneralizeAux(lean_object*, lean_object*, le
lean_object* l_Lean_Meta_assignExprMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_assertExt___lambda__1___closed__1;
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalGeneralize(lean_object*);
lean_object* l_ReaderT_bind___at_Lean_Elab_Tactic_liftMetaTacticAux___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*);
lean_object* l_Lean_Elab_Tactic_saveBacktrackableState___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withMVarContext___at_Lean_Elab_Tactic_withMainMVarContext___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*);
lean_object* l_Lean_throwError___at___private_Lean_Elab_Tactic_Generalize_0__Lean_Elab_Tactic_evalGeneralizeWithEq___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -63,7 +64,6 @@ uint8_t l_Lean_Syntax_isNone(lean_object*);
lean_object* l_Lean_Meta_inferType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Tactic_Generalize_0__Lean_Elab_Tactic_evalGeneralizeWithEq_match__1___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Meta_getMVarDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_bind___at_Lean_Elab_Tactic_withMacroExpansion___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalGeneralizeAux_match__1___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Tactic_Generalize_0__Lean_Elab_Tactic_evalGeneralizeFinalize(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -73,8 +73,8 @@ lean_object* l_Lean_Elab_Tactic_evalGeneralizeAux_match__2(lean_object*);
lean_object* l_Lean_mkAppB(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalGeneralizeAux_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_liftMetaTacticAux___rarg___lambda__2___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___private_Lean_Elab_Tactic_Generalize_0__Lean_Elab_Tactic_getAuxHypothesisName(lean_object*);
lean_object* l_Lean_Elab_Tactic_liftMetaTacticAux___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Tactic_Generalize_0__Lean_Elab_Tactic_evalGeneralizeWithEq_match__2(lean_object*);
lean_object* l_Lean_mkApp3(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Tactic_Generalize_0__Lean_Elab_Tactic_getVarName(lean_object*);
@ -879,9 +879,9 @@ lean_closure_set(x_18, 0, x_16);
lean_closure_set(x_18, 1, x_2);
lean_closure_set(x_18, 2, x_3);
lean_closure_set(x_18, 3, x_1);
x_19 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_liftMetaTacticAux___rarg___lambda__2___boxed), 11, 1);
x_19 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_liftMetaTacticAux___rarg___lambda__1___boxed), 11, 1);
lean_closure_set(x_19, 0, x_17);
x_20 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_withMacroExpansion___spec__2___rarg), 11, 2);
x_20 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_liftMetaTacticAux___spec__1___rarg), 11, 2);
lean_closure_set(x_20, 0, x_18);
lean_closure_set(x_20, 1, x_19);
x_21 = l_Lean_Meta_withMVarContext___at_Lean_Elab_Tactic_withMainMVarContext___spec__1___rarg(x_16, x_20, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_15);
@ -1179,9 +1179,9 @@ lean_closure_set(x_18, 0, x_2);
lean_closure_set(x_18, 1, x_16);
lean_closure_set(x_18, 2, x_1);
lean_closure_set(x_18, 3, x_3);
x_19 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_liftMetaTacticAux___rarg___lambda__2___boxed), 11, 1);
x_19 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_liftMetaTacticAux___rarg___lambda__1___boxed), 11, 1);
lean_closure_set(x_19, 0, x_17);
x_20 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_withMacroExpansion___spec__2___rarg), 11, 2);
x_20 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_liftMetaTacticAux___spec__1___rarg), 11, 2);
lean_closure_set(x_20, 0, x_18);
lean_closure_set(x_20, 1, x_19);
x_21 = l_Lean_Meta_withMVarContext___at_Lean_Elab_Tactic_withMainMVarContext___spec__1___rarg(x_16, x_20, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_15);
@ -1460,9 +1460,9 @@ x_18 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalGeneralizeAux___lambda_
lean_closure_set(x_18, 0, x_16);
lean_closure_set(x_18, 1, x_2);
lean_closure_set(x_18, 2, x_3);
x_19 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_liftMetaTacticAux___rarg___lambda__2___boxed), 11, 1);
x_19 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_liftMetaTacticAux___rarg___lambda__1___boxed), 11, 1);
lean_closure_set(x_19, 0, x_17);
x_20 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_withMacroExpansion___spec__2___rarg), 11, 2);
x_20 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_liftMetaTacticAux___spec__1___rarg), 11, 2);
lean_closure_set(x_20, 0, x_18);
lean_closure_set(x_20, 1, x_19);
x_21 = l_Lean_Meta_withMVarContext___at_Lean_Elab_Tactic_withMainMVarContext___spec__1___rarg(x_16, x_20, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_15);

1861
stage0/stdlib/Lean/Elab/Tactic/Induction.c generated
View file

File diff suppressed because it is too large Load diff

8
stage0/stdlib/Lean/Elab/Tactic/Injection.c generated
View file

@ -37,6 +37,7 @@ lean_object* l_Lean_Meta_throwTacticEx___rarg(lean_object*, lean_object*, lean_o
lean_object* l___private_Lean_Elab_Tactic_Injection_0__Lean_Elab_Tactic_getInjectionNewIds___boxed(lean_object*);
lean_object* l_Lean_Elab_Tactic_evalInjection(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getArgs(lean_object*);
lean_object* l_ReaderT_bind___at_Lean_Elab_Tactic_liftMetaTacticAux___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*);
lean_object* l_Lean_Elab_Tactic_evalInjection_match__1(lean_object*);
lean_object* l___private_Lean_Elab_Tactic_Injection_0__Lean_Elab_Tactic_checkUnusedIds(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withMVarContext___at_Lean_Elab_Tactic_withMainMVarContext___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*);
@ -44,12 +45,11 @@ lean_object* l_Lean_Elab_Tactic_evalInjection___lambda__1___boxed(lean_object*,
lean_object* l_Lean_Elab_Tactic_elabAsFVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isNone(lean_object*);
lean_object* l_Lean_Elab_Tactic_evalInjection___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_bind___at_Lean_Elab_Tactic_withMacroExpansion___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalInjection___closed__1;
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
lean_object* l_Lean_Meta_injection(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_List_isEmpty___rarg(lean_object*);
lean_object* l_Lean_Elab_Tactic_liftMetaTacticAux___rarg___lambda__2___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_Tactic_liftMetaTacticAux___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_map___at___private_Lean_Elab_Tactic_Injection_0__Lean_Elab_Tactic_getInjectionNewIds___spec__1(lean_object* x_1) {
_start:
{
@ -700,9 +700,9 @@ x_25 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalInjection___lambda__1__
lean_closure_set(x_25, 0, x_19);
lean_closure_set(x_25, 1, x_23);
lean_closure_set(x_25, 2, x_15);
x_26 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_liftMetaTacticAux___rarg___lambda__2___boxed), 11, 1);
x_26 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_liftMetaTacticAux___rarg___lambda__1___boxed), 11, 1);
lean_closure_set(x_26, 0, x_24);
x_27 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_withMacroExpansion___spec__2___rarg), 11, 2);
x_27 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_liftMetaTacticAux___spec__1___rarg), 11, 2);
lean_closure_set(x_27, 0, x_25);
lean_closure_set(x_27, 1, x_26);
x_28 = l_Lean_Meta_withMVarContext___at_Lean_Elab_Tactic_withMainMVarContext___spec__1___rarg(x_23, x_27, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_22);

4
stage0/stdlib/Lean/Elab/Tactic/Match.c generated
View file

@ -65,7 +65,7 @@ lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Match_0__Lea
lean_object* l_Lean_Syntax_setKind(lean_object*, lean_object*);
lean_object* l_Lean_Name_appendIndexAfter(lean_object*, lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_12938____closed__10;
extern lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__1;
extern lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__1;
lean_object* l_Lean_Elab_Term_getCurrMacroScope(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Tactic_Match_0__Lean_Elab_Tactic_mkAuxiliaryMatchTerm___closed__1;
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalMatch___closed__1;
@ -511,7 +511,7 @@ lean_dec(x_107);
x_146 = lean_ctor_get(x_6, 0);
lean_inc(x_146);
lean_dec(x_6);
x_147 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5990____closed__1;
x_147 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5993____closed__1;
x_148 = l_Lean_Name_appendIndexAfter(x_147, x_146);
x_149 = l_Lean_Name_append(x_1, x_148);
x_150 = l_Lean_mkIdentFrom(x_30, x_149);

14
stage0/stdlib/Lean/Elab/Tactic/Rewrite.c generated
View file

@ -28,7 +28,6 @@ lean_object* l_Lean_Elab_Tactic_rewriteAll___lambda__1___closed__1;
lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
lean_object* l_Lean_Elab_Tactic_rewriteLocalDeclFVarId_match__1(lean_object*);
lean_object* l_Lean_Elab_Tactic_rewriteAll(lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_withMacroExpansionInfo___at_Lean_Elab_Tactic_withMacroExpansion___spec__1___rarg___closed__1;
extern lean_object* l_Lean_Meta_rewrite___closed__1;
lean_object* l___regBuiltin_Lean_Elab_Tactic_expandRewriteTactic(lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_evalRewriteCore___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*, lean_object*, lean_object*, lean_object*);
@ -60,6 +59,7 @@ lean_object* l_Lean_Elab_Tactic_rewriteTarget_match__1(lean_object*);
lean_object* l_Lean_Elab_Tactic_rewriteAll___lambda__1___closed__3;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_evalRewriteCore___spec__3(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* l_Lean_Elab_Tactic_rewriteTarget___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_sortFVarIds___closed__1;
lean_object* l_Array_forM___at_Lean_Elab_Tactic_evalTacticAux___spec__10___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Tactic_rewrite___closed__2;
lean_object* l_Lean_Elab_Tactic_evalRewriteCore___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -93,6 +93,7 @@ lean_object* l_Lean_Meta_getLocalDecl(lean_object*, lean_object*, lean_object*,
extern lean_object* l_Lean_Parser_Tactic_erewrite___closed__3;
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Tactic_expandERewriteTactic(lean_object*);
lean_object* l_ReaderT_bind___at_Lean_Elab_Tactic_liftMetaTacticAux___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*);
lean_object* l_Lean_Elab_Tactic_rewriteAll_match__1___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_rewriteLocalDecl___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_Lean_Elab_Tactic_setGoals(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -108,7 +109,6 @@ lean_object* l_Array_foldlMUnsafe___at_Lean_Elab_Tactic_evalRewriteCore___spec__
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalERewrite(lean_object*);
lean_object* l_Lean_Meta_instantiateMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_rewriteLocalDeclFVarId_match__1___rarg(lean_object*, lean_object*);
lean_object* l_ReaderT_bind___at_Lean_Elab_Tactic_withMacroExpansion___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalRewriteCore___lambda__2(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Tactic_expandRewriteTactic___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -595,7 +595,7 @@ lean_closure_set(x_24, 0, x_16);
lean_closure_set(x_24, 1, x_22);
lean_closure_set(x_24, 2, x_23);
lean_closure_set(x_24, 3, x_17);
x_25 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_withMacroExpansion___spec__2___rarg), 11, 2);
x_25 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_liftMetaTacticAux___spec__1___rarg), 11, 2);
lean_closure_set(x_25, 0, x_21);
lean_closure_set(x_25, 1, x_24);
x_26 = l_Lean_Meta_withMVarContext___at_Lean_Elab_Tactic_withMainMVarContext___spec__1___rarg(x_16, x_25, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_15);
@ -874,7 +874,7 @@ lean_closure_set(x_25, 1, x_17);
lean_closure_set(x_25, 2, x_23);
lean_closure_set(x_25, 3, x_24);
lean_closure_set(x_25, 4, x_18);
x_26 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_withMacroExpansion___spec__2___rarg), 11, 2);
x_26 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_liftMetaTacticAux___spec__1___rarg), 11, 2);
lean_closure_set(x_26, 0, x_22);
lean_closure_set(x_26, 1, x_25);
x_27 = l_Lean_Meta_withMVarContext___at_Lean_Elab_Tactic_withMainMVarContext___spec__1___rarg(x_17, x_26, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_16);
@ -971,7 +971,7 @@ x_17 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_rewriteLocalDecl___lambda__
lean_closure_set(x_17, 0, x_1);
lean_closure_set(x_17, 1, x_15);
lean_closure_set(x_17, 2, x_16);
x_18 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_withMacroExpansion___spec__2___rarg), 11, 2);
x_18 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_liftMetaTacticAux___spec__1___rarg), 11, 2);
lean_closure_set(x_18, 0, x_14);
lean_closure_set(x_18, 1, x_17);
x_19 = l_Lean_Elab_Tactic_withMainMVarContext___rarg(x_18, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13);
@ -1296,8 +1296,8 @@ lean_closure_set(x_21, 0, x_1);
lean_closure_set(x_21, 1, x_19);
lean_closure_set(x_21, 2, x_20);
lean_closure_set(x_21, 3, x_17);
x_22 = l_Lean_Elab_withMacroExpansionInfo___at_Lean_Elab_Tactic_withMacroExpansion___spec__1___rarg___closed__1;
x_23 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_withMacroExpansion___spec__2___rarg), 11, 2);
x_22 = l___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_sortFVarIds___closed__1;
x_23 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_liftMetaTacticAux___spec__1___rarg), 11, 2);
lean_closure_set(x_23, 0, x_22);
lean_closure_set(x_23, 1, x_21);
x_24 = l_Lean_Elab_Tactic_withMainMVarContext___rarg(x_23, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_18);

16
stage0/stdlib/Lean/Elab/Tactic/Simp.c generated
View file

@ -42,7 +42,6 @@ lean_object* l_Lean_Elab_Tactic_elabSimpConfig___closed__1;
lean_object* l_Lean_Elab_Tactic_simpTarget(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpLemmas___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*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Tactic_simpPost___closed__2;
extern lean_object* l_Lean_Elab_withMacroExpansionInfo___at_Lean_Elab_Tactic_withMacroExpansion___spec__1___rarg___closed__1;
extern lean_object* l_Array_empty___closed__1;
lean_object* lean_environment_find(lean_object*, lean_object*);
lean_object* l_Lean_throwError___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpLemmas_resolveSimpIdLemma_x3f___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -94,6 +93,7 @@ lean_object* l_Lean_Elab_Tactic_elabSimpConfig(lean_object*, lean_object*, lean_
extern lean_object* l_Lean_Meta_Simp_DefaultMethods_methods;
lean_object* l_Lean_Elab_Tactic_evalSimpConfigUnsafe___closed__3;
extern lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_550____closed__1;
extern lean_object* l___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_sortFVarIds___closed__1;
lean_object* l_Lean_Syntax_getId(lean_object*);
lean_object* l_Lean_Elab_Tactic_evalSimp___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_simpLocalDeclFVarId___lambda__2(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*);
@ -147,6 +147,7 @@ uint8_t lean_nat_dec_le(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_simpAll(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_Tactic_evalSimp_match__1(lean_object*);
lean_object* l_Lean_Elab_Tactic_simpLocalDeclFVarId_match__1(lean_object*);
lean_object* l_ReaderT_bind___at_Lean_Elab_Tactic_liftMetaTacticAux___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*);
lean_object* l_Lean_Syntax_getKind(lean_object*);
lean_object* l_Lean_Elab_Tactic_saveBacktrackableState___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_elabSimpConfig___closed__3;
@ -183,7 +184,6 @@ lean_object* l_Lean_Elab_Tactic_evalSimpConfig___boxed(lean_object*, lean_object
lean_object* l_Lean_Meta_instantiateMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_getConstInfo___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpLemmas___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* l_Array_foldlMUnsafe___at_Lean_Elab_Tactic_evalSimp___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*, lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_bind___at_Lean_Elab_Tactic_withMacroExpansion___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forM___at_Lean_Elab_Tactic_evalSimp___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*, lean_object*);
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
lean_object* l_Lean_resolveGlobalConstNoOverload___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpLemmas_resolveSimpIdLemma_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -502,7 +502,7 @@ x_17 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_simpTarget___lambda__1___bo
lean_closure_set(x_17, 0, x_1);
lean_closure_set(x_17, 1, x_14);
lean_closure_set(x_17, 2, x_15);
x_18 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_withMacroExpansion___spec__2___rarg), 11, 2);
x_18 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_liftMetaTacticAux___spec__1___rarg), 11, 2);
lean_closure_set(x_18, 0, x_16);
lean_closure_set(x_18, 1, x_17);
x_19 = l_Lean_Meta_withMVarContext___at_Lean_Elab_Tactic_withMainMVarContext___spec__1___rarg(x_14, x_18, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_13);
@ -817,7 +817,7 @@ lean_closure_set(x_18, 0, x_1);
lean_closure_set(x_18, 1, x_15);
lean_closure_set(x_18, 2, x_2);
lean_closure_set(x_18, 3, x_16);
x_19 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_withMacroExpansion___spec__2___rarg), 11, 2);
x_19 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_liftMetaTacticAux___spec__1___rarg), 11, 2);
lean_closure_set(x_19, 0, x_17);
lean_closure_set(x_19, 1, x_18);
x_20 = l_Lean_Meta_withMVarContext___at_Lean_Elab_Tactic_withMainMVarContext___spec__1___rarg(x_15, x_19, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_14);
@ -910,7 +910,7 @@ x_12 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_simpLocalDecl___lambda__1__
lean_closure_set(x_12, 0, x_2);
x_13 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_simpLocalDecl___lambda__2___boxed), 11, 1);
lean_closure_set(x_13, 0, x_1);
x_14 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_withMacroExpansion___spec__2___rarg), 11, 2);
x_14 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_liftMetaTacticAux___spec__1___rarg), 11, 2);
lean_closure_set(x_14, 0, x_12);
lean_closure_set(x_14, 1, x_13);
x_15 = l_Lean_Elab_Tactic_withMainMVarContext___rarg(x_14, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
@ -1207,8 +1207,8 @@ lean_dec(x_12);
x_15 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_simpAll___lambda__1___boxed), 12, 2);
lean_closure_set(x_15, 0, x_1);
lean_closure_set(x_15, 1, x_13);
x_16 = l_Lean_Elab_withMacroExpansionInfo___at_Lean_Elab_Tactic_withMacroExpansion___spec__1___rarg___closed__1;
x_17 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_withMacroExpansion___spec__2___rarg), 11, 2);
x_16 = l___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_sortFVarIds___closed__1;
x_17 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_liftMetaTacticAux___spec__1___rarg), 11, 2);
lean_closure_set(x_17, 0, x_16);
lean_closure_set(x_17, 1, x_15);
x_18 = l_Lean_Elab_Tactic_withMainMVarContext___rarg(x_17, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_14);
@ -2975,7 +2975,7 @@ lean_closure_set(x_27, 2, x_26);
lean_closure_set(x_27, 3, x_22);
x_28 = lean_alloc_closure((void*)(l___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpLemmas___lambda__1___boxed), 11, 1);
lean_closure_set(x_28, 0, x_2);
x_29 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_withMacroExpansion___spec__2___rarg), 11, 2);
x_29 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_liftMetaTacticAux___spec__1___rarg), 11, 2);
lean_closure_set(x_29, 0, x_27);
lean_closure_set(x_29, 1, x_28);
x_30 = l_Lean_Meta_withMVarContext___at_Lean_Elab_Tactic_withMainMVarContext___spec__1___rarg(x_16, x_29, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_15);

7480
stage0/stdlib/Lean/Elab/Term.c generated
View file

File diff suppressed because it is too large Load diff

376
stage0/stdlib/Lean/Parser/Tactic.c generated
View file

@ -20,7 +20,9 @@ lean_object* l_Lean_Parser_nonReservedSymbol_formatter___boxed(lean_object*, lea
lean_object* l_Lean_Parser_Tactic_matchRhs_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Tactic_match___closed__7;
lean_object* l___regBuiltin_Lean_Parser_Tactic_match_formatter(lean_object*);
lean_object* l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__2;
lean_object* l_Lean_Parser_Tactic_unknown___elambda__1___lambda__1___closed__1;
lean_object* l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__1;
lean_object* l_Lean_Parser_Tactic_match;
lean_object* l_Lean_Parser_Tactic_unknown___elambda__1___closed__2;
lean_object* l_Lean_Parser_andthenInfo(lean_object*, lean_object*);
@ -32,7 +34,9 @@ lean_object* l_Lean_Parser_Tactic_introMatch_parenthesizer___closed__1;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_match___elambda__1___closed__7;
extern lean_object* l_Lean_initFn____x40_Lean_Parser_Extra___hyg_1057____closed__11;
lean_object* l_Lean_Parser_symbol_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_orelse_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_eraseAuxDiscrs;
extern lean_object* l_Lean_Parser_Term_simpleBinder_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Tactic_introMatch_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_match_formatter___closed__4;
@ -59,7 +63,9 @@ lean_object* l_Lean_Parser_Tactic_matchAlts_formatter(lean_object*, lean_object*
lean_object* l_Lean_Parser_Tactic_matchRhs_formatter___closed__1;
lean_object* l_Lean_Parser_Tactic_introMatch_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Tactic_introMatch___elambda__1___closed__7;
lean_object* l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__4;
lean_object* l_Lean_Parser_Tactic_tacticSeqBracketed_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Parser_Tactic_eraseAuxDiscrs_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Tactic_match_formatter___closed__2;
extern lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__3;
lean_object* l_Lean_Parser_nonReservedSymbol(lean_object*, uint8_t);
@ -71,6 +77,7 @@ lean_object* l_Lean_Parser_Tactic_matchRhs___closed__4;
extern lean_object* l_Lean_Parser_Term_match___elambda__1___closed__3;
lean_object* l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_nestedTactic_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__8;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Tactic_case___closed__10;
lean_object* l_Lean_Parser_Tactic_matchRhs___closed__2;
@ -86,6 +93,8 @@ extern lean_object* l_Lean_PrettyPrinter_parenthesizerAttribute;
extern lean_object* l_Lean_Parser_Term_hole___closed__4;
lean_object* l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_5____closed__1;
lean_object* l_Lean_Parser_Tactic_unknown_formatter___closed__3;
lean_object* l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__5;
lean_object* l_Lean_Parser_Tactic_eraseAuxDiscrs_parenthesizer___closed__1;
lean_object* l_Lean_PrettyPrinter_Formatter_errorAtSavedPos_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_byTactic___elambda__1___closed__8;
extern lean_object* l_Lean_Parser_Term_structInst_formatter___closed__2;
@ -98,19 +107,26 @@ lean_object* l_Lean_Parser_Tactic_introMatch___elambda__1___closed__2;
lean_object* l___regBuiltin_Lean_Parser_Tactic_nestedTactic_parenthesizer(lean_object*);
lean_object* l_Lean_Parser_nodeInfo(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_introMatch___closed__6;
lean_object* l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__2;
lean_object* l_Lean_Parser_Tactic_unknown___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__3;
lean_object* l_Lean_Parser_Tactic_introMatch___elambda__1___closed__5;
lean_object* l_Lean_Parser_Tactic_match___elambda__1___closed__2;
lean_object* l_Lean_Parser_Tactic_match___elambda__1___closed__8;
lean_object* l_Lean_Parser_symbol(lean_object*);
extern lean_object* l_Lean_Parser_Term_byTactic_formatter___closed__3;
lean_object* l_Lean_Parser_Tactic_match_parenthesizer___closed__7;
lean_object* l_Lean_Parser_Tactic_introMatch___closed__1;
lean_object* l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__4;
lean_object* l___regBuiltinParser_Lean_Parser_Tactic_eraseAuxDiscrs(lean_object*);
lean_object* l___regBuiltin_Lean_Parser_Tactic_introMatch_formatter___closed__1;
lean_object* l_Lean_Parser_Tactic_introMatch___closed__2;
lean_object* l_Lean_Parser_Tactic_match___elambda__1___closed__3;
extern lean_object* l_Lean_Parser_Term_syntheticHole___closed__6;
lean_object* l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__1;
extern lean_object* l_Lean_Parser_Term_byTactic_parenthesizer___closed__2;
lean_object* l_Lean_Parser_errorAtSavedPosFn(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__6;
lean_object* l___regBuiltin_Lean_Parser_Tactic_match_formatter___closed__1;
extern lean_object* l_Lean_initFn____x40_Lean_Parser_Extra___hyg_938____closed__19;
extern lean_object* l_Lean_Parser_parserAliasesRef;
@ -121,16 +137,20 @@ lean_object* l___regBuiltin_Lean_Parser_Tactic_nestedTactic_formatter___closed__
lean_object* l_Lean_Parser_Tactic_match_parenthesizer___closed__5;
lean_object* l_Lean_Parser_Tactic_introMatch_formatter___closed__3;
extern lean_object* l___regBuiltin_Lean_Parser_Term_syntheticHole_parenthesizer___closed__1;
extern lean_object* l_Lean_Parser_maxPrec;
lean_object* l_Lean_Parser_Tactic_match___elambda__1___closed__5;
lean_object* l___regBuiltin_Lean_Parser_Tactic_unknown_formatter___closed__1;
lean_object* l_Lean_Parser_Tactic_match_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Tactic_eraseAuxDiscrs_parenthesizer___closed__2;
extern lean_object* l_Lean_PrettyPrinter_formatterAttribute;
lean_object* l_Lean_Parser_Tactic_match___closed__8;
lean_object* l_Lean_Parser_Tactic_match_parenthesizer___closed__1;
extern lean_object* l_Lean_Parser_Term_simpleBinder_formatter___closed__2;
lean_object* l_Lean_Parser_Tactic_eraseAuxDiscrs_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_introMatch___elambda__1___closed__3;
lean_object* l_Lean_Parser_Tactic_match_formatter___closed__3;
lean_object* l_Lean_Parser_Tactic_unknown_formatter___closed__1;
lean_object* l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__3;
lean_object* l_Lean_Parser_Tactic_match___closed__9;
extern lean_object* l_Lean_Parser_Term_match_formatter___closed__4;
lean_object* l_Lean_Parser_Tactic_introMatch___closed__4;
@ -141,14 +161,17 @@ lean_object* l_Lean_Parser_Tactic_matchRhs___elambda__1___closed__1;
lean_object* l_Lean_Parser_Tactic_unknown_parenthesizer___closed__4;
extern lean_object* l_Lean_Parser_mkAntiquot_parenthesizer___rarg___closed__5;
lean_object* l_Lean_Parser_Tactic_match___closed__2;
lean_object* l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__5;
lean_object* l_Lean_Parser_Tactic_unknown_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_unknown___closed__7;
lean_object* l___regBuiltin_Lean_Parser_Tactic_eraseAuxDiscrs_parenthesizer(lean_object*);
lean_object* l_Lean_Parser_Tactic_matchRhs_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_withPosition_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinParser_Lean_Parser_Tactic_nestedTactic(lean_object*);
lean_object* l_Lean_Parser_Tactic_tacticSeqBracketed_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_unknown_formatter___closed__5;
lean_object* l_Lean_Parser_Tactic_match___elambda__1___closed__9;
extern lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__7;
lean_object* l_Lean_Parser_Tactic_unknown_formatter___closed__4;
lean_object* l___regBuiltinParser_Lean_Parser_Tactic_match(lean_object*);
lean_object* l_Lean_Parser_Tactic_match___closed__4;
@ -167,11 +190,14 @@ lean_object* l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_5____cl
extern lean_object* l_Lean_PrettyPrinter_Formatter_formatterAliasesRef;
lean_object* l___regBuiltin_Lean_Parser_Tactic_nestedTactic_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Tactic_match___closed__5;
lean_object* l___regBuiltin_Lean_Parser_Tactic_eraseAuxDiscrs_formatter___closed__1;
lean_object* l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__7;
lean_object* l_Lean_Parser_Tactic_introMatch_formatter___closed__2;
lean_object* l_Lean_Parser_Tactic_match_parenthesizer___closed__6;
lean_object* l_Lean_Parser_Tactic_match___elambda__1___closed__4;
lean_object* l_Lean_Parser_Tactic_matchRhs___closed__3;
lean_object* l___regBuiltin_Lean_Parser_Tactic_unknown_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Tactic_eraseAuxDiscrs_formatter___closed__3;
lean_object* l_Lean_Parser_errorAtSavedPos(lean_object*, uint8_t);
lean_object* l_Lean_Parser_Tactic_match_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_match___elambda__1___closed__9;
@ -189,12 +215,15 @@ extern lean_object* l_Lean_Parser_Term_match_parenthesizer___closed__3;
extern lean_object* l_Lean_Parser_Tactic_tactic___x3c_x3b_x3e_____closed__6;
lean_object* l_Lean_Parser_Tactic_nestedTactic_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_hole;
lean_object* l___regBuiltin_Lean_Parser_Tactic_eraseAuxDiscrs_formatter(lean_object*);
extern lean_object* l___regBuiltin_Lean_Parser_Term_hole_formatter___closed__1;
extern lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__8;
lean_object* l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_nodeFn(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_unknown___closed__6;
lean_object* l_Lean_Parser_Tactic_match_formatter___closed__6;
extern lean_object* l_Lean_PrettyPrinter_Parenthesizer_parenthesizerAliasesRef;
lean_object* l_Lean_Parser_Tactic_eraseAuxDiscrs_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_initFn____x40_Lean_Parser_Tactic___hyg_5_(lean_object*);
lean_object* l_Lean_Parser_Tactic_match_parenthesizer___closed__4;
lean_object* l_Lean_Parser_Tactic_unknown_parenthesizer___closed__5;
@ -203,6 +232,7 @@ extern lean_object* l_Lean_Parser_Tactic_intro___closed__2;
lean_object* l_Lean_Parser_mkAntiquot(lean_object*, lean_object*, uint8_t);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_withPosition_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_unknown___closed__3;
lean_object* l_Lean_Parser_Tactic_eraseAuxDiscrs_formatter___closed__2;
lean_object* l___regBuiltin_Lean_Parser_Tactic_match_parenthesizer___closed__1;
extern lean_object* l_Lean_Parser_mkAntiquot_parenthesizer___rarg___closed__1;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -223,6 +253,7 @@ lean_object* l_Lean_Parser_Tactic_matchAlts_formatter___closed__1;
lean_object* l_Lean_Parser_mkAntiquot_parenthesizer___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_introMatch___elambda__1___closed__4;
lean_object* l_Lean_Parser_Tactic_match___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_eraseAuxDiscrs_formatter___closed__1;
lean_object* l_Lean_Parser_Tactic_introMatch_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_andthenFn(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_syntheticHole;
@ -1052,6 +1083,300 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("eraseAuxDiscrs");
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_intro___closed__2;
x_2 = l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__2;
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__1;
x_2 = l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__3;
x_3 = 1;
x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("eraseAuxDiscrs!");
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__5;
x_2 = l_Lean_Parser_symbol(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__6;
x_2 = lean_ctor_get(x_1, 1);
lean_inc(x_2);
x_3 = l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__2;
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_nodeFn), 4, 2);
lean_closure_set(x_4, 0, x_3);
lean_closure_set(x_4, 1, x_2);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_fun___elambda__1___closed__7;
x_2 = l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__7;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; uint8_t x_6; lean_object* x_7;
x_3 = l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__4;
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
x_5 = l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__8;
x_6 = 1;
x_7 = l_Lean_Parser_orelseFnCore(x_4, x_5, x_6, x_1, x_2);
return x_7;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__6;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__2;
x_4 = l_Lean_Parser_nodeInfo(x_3, x_2);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_epsilonInfo;
x_2 = l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__1;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__4;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__2;
x_4 = l_Lean_Parser_orelseInfo(x_2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__4() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1), 2, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__3;
x_2 = l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__4;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_eraseAuxDiscrs() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__5;
return x_1;
}
}
lean_object* l___regBuiltinParser_Lean_Parser_Tactic_eraseAuxDiscrs(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_Tactic_tactic___x3c_x3b_x3e_____closed__6;
x_3 = l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Tactic_eraseAuxDiscrs;
x_6 = lean_unsigned_to_nat(1000u);
x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
return x_7;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_eraseAuxDiscrs_formatter___closed__1() {
_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_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__1;
x_2 = l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__3;
x_3 = 1;
x_4 = lean_box(x_3);
x_5 = lean_alloc_closure((void*)(l_Lean_Parser_mkAntiquot_formatter___boxed), 8, 3);
lean_closure_set(x_5, 0, x_1);
lean_closure_set(x_5, 1, x_2);
lean_closure_set(x_5, 2, x_4);
return x_5;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_eraseAuxDiscrs_formatter___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__5;
x_2 = lean_alloc_closure((void*)(l_Lean_Parser_symbol_formatter), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_eraseAuxDiscrs_formatter___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__2;
x_2 = l_Lean_Parser_maxPrec;
x_3 = l_Lean_Parser_Tactic_eraseAuxDiscrs_formatter___closed__2;
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
lean_closure_set(x_4, 2, x_3);
return x_4;
}
}
lean_object* l_Lean_Parser_Tactic_eraseAuxDiscrs_formatter(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Tactic_eraseAuxDiscrs_formatter___closed__1;
x_7 = l_Lean_Parser_Tactic_eraseAuxDiscrs_formatter___closed__3;
x_8 = l_Lean_PrettyPrinter_Formatter_orelse_formatter(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
}
}
static lean_object* _init_l___regBuiltin_Lean_Parser_Tactic_eraseAuxDiscrs_formatter___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_eraseAuxDiscrs_formatter), 5, 0);
return x_1;
}
}
lean_object* l___regBuiltin_Lean_Parser_Tactic_eraseAuxDiscrs_formatter(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_PrettyPrinter_formatterAttribute;
x_3 = l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__2;
x_4 = l___regBuiltin_Lean_Parser_Tactic_eraseAuxDiscrs_formatter___closed__1;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_eraseAuxDiscrs_parenthesizer___closed__1() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__3;
x_2 = 1;
x_3 = lean_box(x_2);
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_mkAntiquot_parenthesizer___rarg___boxed), 7, 2);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_eraseAuxDiscrs_parenthesizer___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__2;
x_2 = l_Lean_Parser_maxPrec;
x_3 = l_Lean_Parser_mkAntiquot_parenthesizer___rarg___closed__1;
x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
lean_closure_set(x_4, 2, x_3);
return x_4;
}
}
lean_object* l_Lean_Parser_Tactic_eraseAuxDiscrs_parenthesizer(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Tactic_eraseAuxDiscrs_parenthesizer___closed__1;
x_7 = l_Lean_Parser_Tactic_eraseAuxDiscrs_parenthesizer___closed__2;
x_8 = l_Lean_PrettyPrinter_Parenthesizer_orelse_parenthesizer(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
}
}
static lean_object* _init_l___regBuiltin_Lean_Parser_Tactic_eraseAuxDiscrs_parenthesizer___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_eraseAuxDiscrs_parenthesizer), 5, 0);
return x_1;
}
}
lean_object* l___regBuiltin_Lean_Parser_Tactic_eraseAuxDiscrs_parenthesizer(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_PrettyPrinter_parenthesizerAttribute;
x_3 = l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__2;
x_4 = l___regBuiltin_Lean_Parser_Tactic_eraseAuxDiscrs_parenthesizer___closed__1;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_matchRhs___elambda__1___closed__1() {
_start:
{
@ -2145,6 +2470,57 @@ lean_mark_persistent(l___regBuiltin_Lean_Parser_Tactic_nestedTactic_parenthesize
res = l___regBuiltin_Lean_Parser_Tactic_nestedTactic_parenthesizer(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__1 = _init_l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__1);
l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__2 = _init_l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__2();
lean_mark_persistent(l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__2);
l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__3 = _init_l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__3();
lean_mark_persistent(l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__3);
l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__4 = _init_l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__4();
lean_mark_persistent(l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__4);
l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__5 = _init_l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__5();
lean_mark_persistent(l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__5);
l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__6 = _init_l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__6();
lean_mark_persistent(l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__6);
l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__7 = _init_l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__7();
lean_mark_persistent(l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__7);
l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__8 = _init_l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__8();
lean_mark_persistent(l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__8);
l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__1 = _init_l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__1);
l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__2 = _init_l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__2();
lean_mark_persistent(l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__2);
l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__3 = _init_l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__3();
lean_mark_persistent(l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__3);
l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__4 = _init_l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__4();
lean_mark_persistent(l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__4);
l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__5 = _init_l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__5();
lean_mark_persistent(l_Lean_Parser_Tactic_eraseAuxDiscrs___closed__5);
l_Lean_Parser_Tactic_eraseAuxDiscrs = _init_l_Lean_Parser_Tactic_eraseAuxDiscrs();
lean_mark_persistent(l_Lean_Parser_Tactic_eraseAuxDiscrs);
res = l___regBuiltinParser_Lean_Parser_Tactic_eraseAuxDiscrs(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_Tactic_eraseAuxDiscrs_formatter___closed__1 = _init_l_Lean_Parser_Tactic_eraseAuxDiscrs_formatter___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_eraseAuxDiscrs_formatter___closed__1);
l_Lean_Parser_Tactic_eraseAuxDiscrs_formatter___closed__2 = _init_l_Lean_Parser_Tactic_eraseAuxDiscrs_formatter___closed__2();
lean_mark_persistent(l_Lean_Parser_Tactic_eraseAuxDiscrs_formatter___closed__2);
l_Lean_Parser_Tactic_eraseAuxDiscrs_formatter___closed__3 = _init_l_Lean_Parser_Tactic_eraseAuxDiscrs_formatter___closed__3();
lean_mark_persistent(l_Lean_Parser_Tactic_eraseAuxDiscrs_formatter___closed__3);
l___regBuiltin_Lean_Parser_Tactic_eraseAuxDiscrs_formatter___closed__1 = _init_l___regBuiltin_Lean_Parser_Tactic_eraseAuxDiscrs_formatter___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Tactic_eraseAuxDiscrs_formatter___closed__1);
res = l___regBuiltin_Lean_Parser_Tactic_eraseAuxDiscrs_formatter(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_Tactic_eraseAuxDiscrs_parenthesizer___closed__1 = _init_l_Lean_Parser_Tactic_eraseAuxDiscrs_parenthesizer___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_eraseAuxDiscrs_parenthesizer___closed__1);
l_Lean_Parser_Tactic_eraseAuxDiscrs_parenthesizer___closed__2 = _init_l_Lean_Parser_Tactic_eraseAuxDiscrs_parenthesizer___closed__2();
lean_mark_persistent(l_Lean_Parser_Tactic_eraseAuxDiscrs_parenthesizer___closed__2);
l___regBuiltin_Lean_Parser_Tactic_eraseAuxDiscrs_parenthesizer___closed__1 = _init_l___regBuiltin_Lean_Parser_Tactic_eraseAuxDiscrs_parenthesizer___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Tactic_eraseAuxDiscrs_parenthesizer___closed__1);
res = l___regBuiltin_Lean_Parser_Tactic_eraseAuxDiscrs_parenthesizer(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_Tactic_matchRhs___elambda__1___closed__1 = _init_l_Lean_Parser_Tactic_matchRhs___elambda__1___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_matchRhs___elambda__1___closed__1);
l_Lean_Parser_Tactic_matchRhs___closed__1 = _init_l_Lean_Parser_Tactic_matchRhs___closed__1();