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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-02 13:17:50 -07:00
parent 379e34a910
commit 04eda60451
8 changed files with 2575 additions and 1192 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

41
stage0/src/Lean/Elab/Do.lean generated
View file

@ -90,7 +90,7 @@ partial def toMessageDataAux (updateVars : MessageData) : Code → MessageData
| Code.«break» _ => "break " ++ updateVars
| Code.«continue» _ => "continue " ++ updateVars
| Code.«return» _ none => "return " ++ updateVars
| Code.«return» _ (some x) => "return " ++ x ++ " " ++ updateVars
| Code.«return» _ (some x) => "return " ++ x.simpMacroScopes ++ " " ++ updateVars
| Code.«match» _ ds t alts =>
"match " ++ MessageData.joinSep (ds.toList.map MessageData.ofSyntax) ", " ++ " with " ++
alts.foldl
@ -176,13 +176,13 @@ partial def pullExitPointsAux : NameSet → Code → StateRefT (Array JPDecl) Te
| rs, Code.«continue» ref => do let xs := nameSetToArray rs; jp ← addFreshJP xs (Code.«continue» ref); pure $ Code.jmp ref jp xs
| rs, Code.«return» ref y? => do
let xs := nameSetToArray rs;
(ps, xs) ← match y? with
| none => pure (xs, xs)
(ps, xs, y?) ← match y? with
| none => pure (xs, xs, none)
| some y =>
if rs.contains y then pure (xs, xs)
if rs.contains y then pure (xs, xs, some y)
else do {
yFresh ← mkFreshUserName y;
pure (xs.push y, xs.push yFresh)
pure (xs.push yFresh, xs.push y, some yFresh)
};
jp ← addFreshJP ps (Code.«return» ref y?);
pure $ Code.jmp ref jp xs
@ -500,11 +500,6 @@ private partial def expandDoElems : Bool → Array Syntax → Nat → MacroM Syn
else
Macro.throwUnsupported
@[builtinMacro Lean.Parser.Term.do] def expandDo : Macro :=
fun stx =>
let doElems := getDoElems stx;
expandDoElems false doElems 0
structure ProcessedDoElem :=
(action : Expr)
(var : Expr)
@ -574,17 +569,25 @@ private partial def processDoElemsAux (doElems : Array Syntax) (m bindInstVal :
private def processDoElems (doElems : Array Syntax) (m bindInstVal : Expr) (expectedType : Expr) : TermElabM Expr :=
processDoElemsAux doElems m bindInstVal expectedType 0 #[]
def expandDo? (stx : Syntax) : MacroM (Option Syntax) :=
let doElems := getDoElems stx;
catch
(do stx ← expandDoElems false doElems 0; pure $ some stx)
(fun _ => pure none)
@[builtinTermElab «do»] def elabDo : TermElab :=
fun stx expectedType? => do
tryPostponeIfNoneOrMVar expectedType?;
let doElems := getDoElems stx;
trace `Elab.do $ fun _ => stx;
let doElems := doElems.getSepElems;
trace `Elab.do $ fun _ => "doElems: " ++ toString doElems;
{ m := m, hasBindInst := bindInstVal, .. } ← extractBind expectedType?;
result ← processDoElems doElems m bindInstVal expectedType?.get!;
-- dbgTrace ("result: " ++ toString result);
pure result
stxNew? ← liftMacroM $ expandDo? stx;
match stxNew? with
| some stxNew => withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
| none => do
tryPostponeIfNoneOrMVar expectedType?;
let doElems := getDoElems stx;
trace `Elab.do $ fun _ => stx;
let doElems := doElems.getSepElems;
trace `Elab.do $ fun _ => "doElems: " ++ toString doElems;
{ m := m, hasBindInst := bindInstVal, .. } ← extractBind expectedType?;
processDoElems doElems m bindInstVal expectedType?.get!
@[builtinTermElab liftMethod] def elabLiftMethod : TermElab :=
fun stx _ =>

3
stage0/src/Lean/Elab/SyntheticMVars.lean generated
View file

@ -151,7 +151,8 @@ newSyntheticMVars ← s.syntheticMVars.filterM $ fun mvarDecl =>
val ← instantiateMVars (mkMVar mvarDecl.mvarId);
when val.getAppFn.isMVar $
unlessM (isDefEq val defaultVal) $
throwError "failed to assign default value to metavariable"; -- TODO: better error message
-- TODO: better error message
throwError ("failed to assign default value to metavariable" ++ indentExpr val ++ Format.line ++ "default value" ++ indentExpr defaultVal) ;
pure false
| _ => pure true;
modify $ fun s => { s with syntheticMVars := newSyntheticMVars };

33
stage0/src/Lean/Elab/Term.lean generated
View file

@ -66,9 +66,6 @@ namespace Term
Haskell would work on this example since it always uses
first-order unification.
We do not change the
-/
def setElabConfig (cfg : Meta.Config) : Meta.Config :=
{ cfg with foApprox := true, ctxApprox := true, constApprox := false, quasiPatternApprox := false }
@ -520,19 +517,18 @@ if hasCDot stx then do
else
pure none
def mkTypeMismatchError (e : Expr) (eType : Expr) (expectedType : Expr) (header : String := "type mismatch") : MessageData :=
header ++ indentExpr e
++ Format.line ++ "has type" ++ indentExpr eType
++ Format.line ++ "but it is expected to have type" ++ indentExpr expectedType
def throwTypeMismatchError {α} (expectedType : Expr) (eType : Expr) (e : Expr)
(f? : Option Expr := none) (extraMsg? : Option MessageData := none) : TermElabM α :=
let extraMsg : MessageData := match extraMsg? with
| none => Format.nil
| some extraMsg => Format.line ++ extraMsg;
match f? with
| none =>
let msg : MessageData :=
"type mismatch" ++ indentExpr e
++ Format.line ++ "has type" ++ indentExpr eType
++ Format.line ++ "but it is expected to have type" ++ indentExpr expectedType
++ extraMsg;
throwError msg
| none => throwError $ mkTypeMismatchError e eType expectedType ++ extraMsg
| some f => Meta.throwAppTypeMismatch f e extraMsg
@[inline] def withoutMacroStackAtErr {α} (x : TermElabM α) : TermElabM α :=
@ -1277,6 +1273,23 @@ fun stx _ =>
| some val => pure $ toExpr val
| none => throwIllFormedSyntax
@[builtinTermElab typeOf] def elabTypeOf : TermElab :=
fun stx _ => do
e ← elabTerm (stx.getArg 1) none;
inferType e
@[builtinTermElab ensureTypeOf] def elabEnsureTypeOf : TermElab :=
fun stx expectedType? =>
match (stx.getArg 2).isStrLit? with
| none => throwIllFormedSyntax
| some msg => do
refTerm ← elabTerm (stx.getArg 1) none;
refTermType ← inferType refTerm;
e ← elabTerm (stx.getArg 3) expectedType?;
eType ← inferType e;
unlessM (isDefEq eType refTermType) $ throwError $ mkTypeMismatchError e eType refTermType msg;
pure e
private def mkSomeContext : Context :=
{ fileName := "<TermElabM>",
fileMap := arbitrary _,

8
stage0/src/Lean/Parser/Do.lean generated
View file

@ -25,11 +25,13 @@ def doSeqIndent := many1Indent $ doElemParser >> optional "; "
def doSeqBracketed := parser! "{" >> sepBy1 doElemParser "; " true >> "}"
def doSeq := doSeqBracketed <|> doSeqIndent
@[builtinDoElemParser] def doLet := parser! "let " >> letDecl
@[builtinDoElemParser] def doLetRec := parser! group ("let " >> nonReservedSymbol "rec ") >> letRecDecls
@[builtinDoElemParser] def doLet := parser! "let " >> letDecl
@[builtinDoElemParser] def doLetRec := parser! group ("let " >> nonReservedSymbol "rec ") >> letRecDecls
def doId := parser! «try» (ident >> optType >> leftArrow) >> termParser
def doPat := parser! «try» (termParser >> leftArrow) >> termParser >> optional (" | " >> termParser)
@[builtinDoElemParser] def doLetArrow := parser! "let " >> (doId <|> doPat)
@[builtinDoElemParser] def doLetArrow := parser! "let " >> (doId <|> doPat)
@[builtinDoElemParser] def doReassign := parser! letIdDecl <|> letPatDecl
@[builtinDoElemParser] def doReassignArrow := doId <|> doPat
@[builtinDoElemParser] def doHave := parser! "have " >> Term.haveDecl
/-
In `do` blocks, we support `if` without an `else`. Thus, we use indentation to prevent examples such as

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

File diff suppressed because it is too large Load diff

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

@ -28,6 +28,7 @@ lean_object* l___private_Lean_Elab_SyntheticMVars_7__synthesizeSyntheticMVarsSte
extern lean_object* l_Lean_withIncRecDepth___rarg___lambda__2___closed__2;
lean_object* l_unreachable_x21___rarg(lean_object*);
lean_object* l_Lean_Elab_Term_liftTacticElabM___rarg___lambda__1(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_MessageData_ofList___closed__3;
lean_object* l_Lean_Elab_Term_runTactic___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_ensureAssignmentHasNoMVars___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_liftTacticElabM___rarg___closed__1;
@ -50,6 +51,7 @@ lean_object* l_Lean_Elab_Term_getMVarDecl(lean_object*, lean_object*, lean_objec
lean_object* l_List_find_x3f___main___rarg(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_SyntheticMVars_2__resumePostponed___lambda__1(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_Expr_getAppFn___main(lean_object*);
lean_object* l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_8__synthesizeUsingDefault___spec__1___lambda__1___closed__4;
lean_object* l_List_forM___main___at___private_Lean_Elab_SyntheticMVars_9__reportStuckSyntheticMVars___spec__1___closed__1;
lean_object* l_List_forM___main___at___private_Lean_Elab_SyntheticMVars_9__reportStuckSyntheticMVars___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_7__synthesizeSyntheticMVarsStep___spec__2___closed__1;
@ -132,12 +134,14 @@ lean_object* l_Lean_Elab_Term_synthesizeSyntheticMVarsNoPostponing(lean_object*,
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_SyntheticMVars_2__resumePostponed(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* l_Lean_Elab_Term_withSynthesize___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_8__synthesizeUsingDefault___spec__1___lambda__1___closed__6;
lean_object* l_Lean_Elab_Term_reportUnsolvedGoals(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_SyntheticMVars_7__synthesizeSyntheticMVarsStep___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_throwTypeMismatchError___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_SyntheticMVars_7__synthesizeSyntheticMVarsStep___closed__1;
lean_object* l___private_Lean_Elab_SyntheticMVars_11__synthesizeSyntheticMVarsAux(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MetavarContext_instantiateMVarDeclMVars(lean_object*, lean_object*);
lean_object* l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_8__synthesizeUsingDefault___spec__1___lambda__1___closed__5;
uint8_t l___private_Lean_Elab_SyntheticMVars_10__getSomeSynthethicMVarsRef___rarg___lambda__1(lean_object*);
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_SyntheticMVars_7__synthesizeSyntheticMVarsStep___closed__2;
@ -3392,6 +3396,34 @@ lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_8__synthesizeUsingDefault___spec__1___lambda__1___closed__4() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("default value");
return x_1;
}
}
lean_object* _init_l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_8__synthesizeUsingDefault___spec__1___lambda__1___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_8__synthesizeUsingDefault___spec__1___lambda__1___closed__4;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_8__synthesizeUsingDefault___spec__1___lambda__1___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_8__synthesizeUsingDefault___spec__1___lambda__1___closed__5;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_8__synthesizeUsingDefault___spec__1___lambda__1(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, lean_object* x_8, lean_object* x_9) {
_start:
{
@ -3423,6 +3455,8 @@ lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_1);
lean_inc(x_2);
x_15 = l_Lean_Meta_isExprDefEq___at_Lean_Elab_Term_synthesizeInstMVarCore___spec__3(x_2, x_1, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
if (lean_obj_tag(x_15) == 0)
{
@ -3433,69 +3467,51 @@ x_17 = lean_unbox(x_16);
lean_dec(x_16);
if (x_17 == 0)
{
lean_object* x_18; lean_object* x_19; lean_object* x_20; uint8_t x_21;
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; uint8_t x_29;
x_18 = lean_ctor_get(x_15, 1);
lean_inc(x_18);
lean_dec(x_15);
x_19 = l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_8__synthesizeUsingDefault___spec__1___lambda__1___closed__3;
x_20 = l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1___rarg(x_19, x_3, x_4, x_5, x_6, x_7, x_8, x_18);
x_19 = l_Lean_indentExpr(x_2);
x_20 = l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_8__synthesizeUsingDefault___spec__1___lambda__1___closed__3;
x_21 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_19);
x_22 = l_Lean_MessageData_ofList___closed__3;
x_23 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_23, 0, x_21);
lean_ctor_set(x_23, 1, x_22);
x_24 = l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_8__synthesizeUsingDefault___spec__1___lambda__1___closed__6;
x_25 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_25, 0, x_23);
lean_ctor_set(x_25, 1, x_24);
x_26 = l_Lean_indentExpr(x_1);
x_27 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_27, 0, x_25);
lean_ctor_set(x_27, 1, x_26);
x_28 = l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1___rarg(x_27, x_3, x_4, x_5, x_6, x_7, x_8, x_18);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
x_21 = !lean_is_exclusive(x_20);
if (x_21 == 0)
x_29 = !lean_is_exclusive(x_28);
if (x_29 == 0)
{
return x_20;
return x_28;
}
else
{
lean_object* x_22; lean_object* x_23; lean_object* x_24;
x_22 = lean_ctor_get(x_20, 0);
x_23 = lean_ctor_get(x_20, 1);
lean_inc(x_23);
lean_inc(x_22);
lean_dec(x_20);
x_24 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_24, 0, x_22);
lean_ctor_set(x_24, 1, x_23);
return x_24;
}
}
else
{
uint8_t x_25;
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_3);
x_25 = !lean_is_exclusive(x_15);
if (x_25 == 0)
{
lean_object* x_26; uint8_t x_27; lean_object* x_28;
x_26 = lean_ctor_get(x_15, 0);
lean_dec(x_26);
x_27 = 0;
x_28 = lean_box(x_27);
lean_ctor_set(x_15, 0, x_28);
return x_15;
}
else
{
lean_object* x_29; uint8_t x_30; lean_object* x_31; lean_object* x_32;
x_29 = lean_ctor_get(x_15, 1);
lean_inc(x_29);
lean_dec(x_15);
x_30 = 0;
x_31 = lean_box(x_30);
x_32 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_32, 0, x_31);
lean_ctor_set(x_32, 1, x_29);
lean_object* x_30; lean_object* x_31; lean_object* x_32;
x_30 = lean_ctor_get(x_28, 0);
x_31 = lean_ctor_get(x_28, 1);
lean_inc(x_31);
lean_inc(x_30);
lean_dec(x_28);
x_32 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_32, 0, x_30);
lean_ctor_set(x_32, 1, x_31);
return x_32;
}
}
}
else
{
uint8_t x_33;
@ -3504,23 +3520,61 @@ lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_33 = !lean_is_exclusive(x_15);
if (x_33 == 0)
{
lean_object* x_34; uint8_t x_35; lean_object* x_36;
x_34 = lean_ctor_get(x_15, 0);
lean_dec(x_34);
x_35 = 0;
x_36 = lean_box(x_35);
lean_ctor_set(x_15, 0, x_36);
return x_15;
}
else
{
lean_object* x_37; uint8_t x_38; lean_object* x_39; lean_object* x_40;
x_37 = lean_ctor_get(x_15, 1);
lean_inc(x_37);
lean_dec(x_15);
x_38 = 0;
x_39 = lean_box(x_38);
x_40 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_40, 0, x_39);
lean_ctor_set(x_40, 1, x_37);
return x_40;
}
}
}
else
{
uint8_t x_41;
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_41 = !lean_is_exclusive(x_15);
if (x_41 == 0)
{
return x_15;
}
else
{
lean_object* x_34; lean_object* x_35; lean_object* x_36;
x_34 = lean_ctor_get(x_15, 0);
x_35 = lean_ctor_get(x_15, 1);
lean_inc(x_35);
lean_inc(x_34);
lean_object* x_42; lean_object* x_43; lean_object* x_44;
x_42 = lean_ctor_get(x_15, 0);
x_43 = lean_ctor_get(x_15, 1);
lean_inc(x_43);
lean_inc(x_42);
lean_dec(x_15);
x_36 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_36, 0, x_34);
lean_ctor_set(x_36, 1, x_35);
return x_36;
x_44 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_44, 0, x_42);
lean_ctor_set(x_44, 1, x_43);
return x_44;
}
}
}
@ -6688,6 +6742,12 @@ l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_8__synthesizeUs
lean_mark_persistent(l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_8__synthesizeUsingDefault___spec__1___lambda__1___closed__2);
l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_8__synthesizeUsingDefault___spec__1___lambda__1___closed__3 = _init_l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_8__synthesizeUsingDefault___spec__1___lambda__1___closed__3();
lean_mark_persistent(l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_8__synthesizeUsingDefault___spec__1___lambda__1___closed__3);
l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_8__synthesizeUsingDefault___spec__1___lambda__1___closed__4 = _init_l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_8__synthesizeUsingDefault___spec__1___lambda__1___closed__4();
lean_mark_persistent(l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_8__synthesizeUsingDefault___spec__1___lambda__1___closed__4);
l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_8__synthesizeUsingDefault___spec__1___lambda__1___closed__5 = _init_l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_8__synthesizeUsingDefault___spec__1___lambda__1___closed__5();
lean_mark_persistent(l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_8__synthesizeUsingDefault___spec__1___lambda__1___closed__5);
l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_8__synthesizeUsingDefault___spec__1___lambda__1___closed__6 = _init_l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_8__synthesizeUsingDefault___spec__1___lambda__1___closed__6();
lean_mark_persistent(l_List_filterAuxM___main___at___private_Lean_Elab_SyntheticMVars_8__synthesizeUsingDefault___spec__1___lambda__1___closed__6);
l_List_forM___main___at___private_Lean_Elab_SyntheticMVars_9__reportStuckSyntheticMVars___spec__1___lambda__1___closed__1 = _init_l_List_forM___main___at___private_Lean_Elab_SyntheticMVars_9__reportStuckSyntheticMVars___spec__1___lambda__1___closed__1();
lean_mark_persistent(l_List_forM___main___at___private_Lean_Elab_SyntheticMVars_9__reportStuckSyntheticMVars___spec__1___lambda__1___closed__1);
l_List_forM___main___at___private_Lean_Elab_SyntheticMVars_9__reportStuckSyntheticMVars___spec__1___lambda__1___closed__2 = _init_l_List_forM___main___at___private_Lean_Elab_SyntheticMVars_9__reportStuckSyntheticMVars___spec__1___lambda__1___closed__2();

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

@ -22,6 +22,8 @@ lean_object* l_Lean_getConstInfo___at_Lean_Elab_Term_mkConst___spec__1(lean_obje
lean_object* l___regBuiltin_Lean_Elab_Term_elabByTactic___closed__3;
lean_object* l___private_Lean_Elab_Term_27__mkFreshLevelMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_elabStrLit___closed__1;
lean_object* l_Lean_Elab_Term_elabTypeOf___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_elabEnsureTypeOf___closed__2;
lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___closed__1;
lean_object* l_Lean_mkAppStx(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_monadQuotation;
@ -122,6 +124,7 @@ lean_object* l___regBuiltin_Lean_Elab_Term_elabQuotedName___closed__1;
extern lean_object* l_Std_HashMap_inhabited___closed__1;
lean_object* l_Lean_Elab_Term_expandArrayLit___closed__7;
lean_object* l___private_Lean_Elab_Term_23__mkPairsAux___main___closed__1;
lean_object* l___regBuiltin_Lean_Elab_Term_elabEnsureTypeOf___closed__1;
lean_object* l___private_Lean_Elab_Term_11__elabUsingElabFns___closed__1;
lean_object* l___private_Lean_Elab_Term_18__elabImplicitLambda___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_MonadLiftT___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -135,6 +138,7 @@ lean_object* l_Lean_Meta_getMVarsAtDeclImp(lean_object*, lean_object*, lean_obje
lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Prod_HasRepr___rarg___closed__1;
lean_object* l___private_Lean_Elab_Term_9__postponeElabTerm___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_elabTypeOf(lean_object*);
lean_object* l_Lean_Elab_Term_elabQuotedName___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withLocalDecl___at___private_Lean_Elab_Term_18__elabImplicitLambda___main___spec__1___rarg___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_MacroScopesView_format(lean_object*, lean_object*);
@ -227,6 +231,7 @@ extern lean_object* l_List_repr___rarg___closed__3;
extern lean_object* l_Lean_unitToExpr___lambda__1___closed__3;
lean_object* l___regBuiltin_Lean_Elab_Term_elabTypeStx___closed__2;
lean_object* l_Lean_Elab_Term_elabSort___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabTypeOf(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
size_t l_USize_shiftRight(size_t, size_t);
lean_object* l___private_Lean_Elab_Term_7__tryPureCoe_x3f(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_synthesizeInst(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -370,6 +375,7 @@ lean_object* l_Array_anyRangeMAux___main___at___private_Lean_Elab_Term_14__isLam
lean_object* l_Lean_Elab_Term_mkFreshInstanceName(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_append___main(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Term_25__resolveLocalNameAux___main(lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_elabEnsureTypeOf___closed__3;
lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___closed__3;
lean_object* l_Lean_Elab_Term_withMacroExpansion___rarg(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_elabByTactic___closed__2;
@ -415,7 +421,6 @@ uint8_t l_Lean_Elab_Term_blockImplicitLambda(lean_object*);
lean_object* l_Lean_Elab_Term_elabTypeStx(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_assignLevelMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_setMCtx___at_Lean_Elab_Term_savingMCtx___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_throwTypeMismatchError___rarg___closed__3;
lean_object* l_Lean_Elab_Term_monadLog___closed__6;
lean_object* l_Lean_Elab_Term_levelMVarToParam___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Term_1__liftAttrM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -448,6 +453,7 @@ lean_object* l_Lean_Elab_Term_liftLevelM___rarg(lean_object*, lean_object*, lean
lean_object* l_Lean_Syntax_getId(lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_elabParen___closed__1;
lean_object* l_Lean_Elab_Term_Lean_Elab_MonadMacroAdapter;
lean_object* l_Lean_Elab_Term_mkTypeMismatchError(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_throwPostpone___at_Lean_Elab_Term_tryPostpone___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Term_9__postponeElabTerm(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -507,6 +513,7 @@ lean_object* l_Lean_Elab_Term_MVarErrorInfo_logError___closed__5;
lean_object* l_Lean_LocalDecl_toExpr(lean_object*);
extern lean_object* l_Lean_firstFrontendMacroScope;
lean_object* l___private_Lean_Elab_Term_10__elabUsingElabFnsAux___main___closed__1;
lean_object* l___regBuiltin_Lean_Elab_Term_elabTypeOf___closed__3;
lean_object* l_Lean_Elab_Term_expandArrayLit___closed__8;
lean_object* l_Lean_Elab_Term_ensureHasType___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_isType___at_Lean_Elab_Term_ensureType___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -572,7 +579,6 @@ lean_object* l_Lean_Elab_Term_mkConst___closed__3;
lean_object* l_Lean_Elab_Term_resolveName___closed__4;
extern lean_object* l_Lean_nullKind___closed__2;
uint8_t l_Array_anyRangeMAux___main___at___private_Lean_Elab_Term_14__isLambdaWithImplicit___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_throwTypeMismatchError___rarg___closed__2;
lean_object* l_Lean_Elab_Term_elabCharLit(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Term_MVarErrorInfo_logError___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_expandListLit___boxed(lean_object*, lean_object*, lean_object*);
@ -598,8 +604,10 @@ lean_object* l_Lean_Elab_Term_mkTermElabAttribute___closed__9;
lean_object* l_Lean_Meta_whnfForall___at___private_Lean_Elab_Term_16__useImplicitLambda_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_log___at_Lean_Elab_Term_traceAtCmdPos___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Term_MVarErrorInfo_logError___spec__2___closed__1;
lean_object* l___regBuiltin_Lean_Elab_Term_elabEnsureTypeOf(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_Elab_Term_Lean_Ref___closed__4;
lean_object* l_Lean_Elab_Term_elabEnsureTypeOf___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Option_HasRepr___rarg___closed__3;
lean_object* l_Lean_Elab_Term_resetMessageLog(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_traceAtCmdPos___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -681,6 +689,7 @@ lean_object* l_Lean_Elab_Term_registerMVarErrorCustomInfo(lean_object*, lean_obj
extern lean_object* l_Std_PersistentHashMap_mkCollisionNode___rarg___closed__1;
lean_object* l_Lean_Meta_getMVarsImp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_toExprAux___main(lean_object*);
lean_object* l_Lean_Elab_Term_elabEnsureTypeOf(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_elabBadCDot(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*);
uint8_t l___private_Lean_Elab_Term_14__isLambdaWithImplicit(lean_object*);
@ -949,6 +958,7 @@ lean_object* l_Lean_Elab_throwAbort___at_Lean_Elab_Term_ensureNoUnassignedMVars_
lean_object* l_Lean_Elab_Term_elabTermWithoutImplicitLambdas___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_mkFreshInstanceName___closed__1;
lean_object* l_Lean_mkApp3(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_elabTypeOf___closed__2;
lean_object* l_Lean_Meta_mkFreshExprMVar___at_Lean_Elab_Term_tryCoe___spec__2(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabSyntheticHole___closed__7;
lean_object* l_Lean_Elab_Term_monadLog___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -971,6 +981,7 @@ lean_object* l_Lean_Elab_Term_resolveGlobalConstNoOverload___closed__5;
lean_object* l_Lean_Elab_Term_expandArrayLit___closed__5;
uint8_t l_Lean_Syntax_isIdent(lean_object*);
extern lean_object* l_Lean_Elab_registerPostponeId___closed__1;
lean_object* l___regBuiltin_Lean_Elab_Term_elabTypeOf___closed__1;
extern lean_object* l_Lean_KernelException_toMessageData___closed__39;
lean_object* l_Lean_Elab_Term_tryCoe___closed__3;
lean_object* l_Lean_Elab_Term_setElabConfig(lean_object* x_1) {
@ -8114,6 +8125,44 @@ return x_45;
}
}
}
lean_object* l_Lean_Elab_Term_mkTypeMismatchError(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_5 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_5, 0, x_4);
x_6 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_6, 0, x_5);
x_7 = l_Lean_indentExpr(x_1);
x_8 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_8, 0, x_6);
lean_ctor_set(x_8, 1, x_7);
x_9 = l_Lean_MessageData_ofList___closed__3;
x_10 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_10, 0, x_8);
lean_ctor_set(x_10, 1, x_9);
x_11 = l_Lean_KernelException_toMessageData___closed__12;
x_12 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_12, 0, x_10);
lean_ctor_set(x_12, 1, x_11);
x_13 = l_Lean_indentExpr(x_2);
x_14 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_14, 0, x_12);
lean_ctor_set(x_14, 1, x_13);
x_15 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_15, 0, x_14);
lean_ctor_set(x_15, 1, x_9);
x_16 = l_Lean_KernelException_toMessageData___closed__15;
x_17 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_17, 0, x_15);
lean_ctor_set(x_17, 1, x_16);
x_18 = l_Lean_indentExpr(x_3);
x_19 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_19, 0, x_17);
lean_ctor_set(x_19, 1, x_18);
return x_19;
}
}
lean_object* l_Lean_Meta_inferType___at_Lean_Elab_Term_throwTypeMismatchError___spec__2(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, lean_object* x_8) {
_start:
{
@ -8534,121 +8583,78 @@ x_1 = lean_mk_string("type mismatch");
return x_1;
}
}
lean_object* _init_l_Lean_Elab_Term_throwTypeMismatchError___rarg___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_throwTypeMismatchError___rarg___closed__1;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Elab_Term_throwTypeMismatchError___rarg___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_throwTypeMismatchError___rarg___closed__2;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* l_Lean_Elab_Term_throwTypeMismatchError___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, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12) {
_start:
{
lean_object* x_13;
if (lean_obj_tag(x_5) == 0)
{
if (lean_obj_tag(x_4) == 0)
{
lean_object* x_31;
x_31 = l_Lean_MessageData_Inhabited___closed__1;
x_13 = x_31;
goto block_30;
}
else
{
lean_object* x_32; lean_object* x_33; lean_object* x_34;
lean_dec(x_2);
lean_dec(x_1);
x_32 = lean_ctor_get(x_4, 0);
lean_inc(x_32);
lean_dec(x_4);
x_33 = l_Lean_MessageData_Inhabited___closed__1;
x_34 = l_Lean_Meta_throwAppTypeMismatch___at_Lean_Elab_Term_throwTypeMismatchError___spec__1___rarg(x_32, x_3, x_33, x_6, x_7, x_8, x_9, x_10, x_11, x_12);
return x_34;
}
}
else
{
lean_object* x_35; lean_object* x_36; lean_object* x_37;
x_35 = lean_ctor_get(x_5, 0);
x_36 = l_Lean_MessageData_ofList___closed__3;
lean_inc(x_35);
x_37 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_37, 0, x_36);
lean_ctor_set(x_37, 1, x_35);
if (lean_obj_tag(x_4) == 0)
{
x_13 = x_37;
goto block_30;
}
else
{
lean_object* x_38; lean_object* x_39;
lean_dec(x_2);
lean_dec(x_1);
x_38 = lean_ctor_get(x_4, 0);
lean_inc(x_38);
lean_dec(x_4);
x_39 = l_Lean_Meta_throwAppTypeMismatch___at_Lean_Elab_Term_throwTypeMismatchError___spec__3___rarg(x_38, x_3, x_37, x_6, x_7, x_8, x_9, x_10, x_11, x_12);
return x_39;
}
}
block_30:
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29;
x_14 = l_Lean_indentExpr(x_3);
x_15 = l_Lean_Elab_Term_throwTypeMismatchError___rarg___closed__3;
lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_13 = l_Lean_Elab_Term_throwTypeMismatchError___rarg___closed__1;
x_14 = l_Lean_Elab_Term_mkTypeMismatchError(x_3, x_2, x_1, x_13);
x_15 = l_Lean_MessageData_Inhabited___closed__1;
x_16 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_16, 0, x_15);
lean_ctor_set(x_16, 1, x_14);
x_17 = l_Lean_MessageData_ofList___closed__3;
x_18 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_18, 0, x_16);
lean_ctor_set(x_18, 1, x_17);
x_19 = l_Lean_KernelException_toMessageData___closed__12;
x_20 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_20, 0, x_18);
lean_ctor_set(x_20, 1, x_19);
x_21 = l_Lean_indentExpr(x_2);
x_22 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_22, 0, x_20);
lean_ctor_set(x_22, 1, x_21);
x_23 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_23, 0, x_22);
lean_ctor_set(x_23, 1, x_17);
x_24 = l_Lean_KernelException_toMessageData___closed__15;
x_25 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_25, 0, x_23);
lean_ctor_set(x_25, 1, x_24);
x_26 = l_Lean_indentExpr(x_1);
x_27 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_27, 0, x_25);
lean_ctor_set(x_27, 1, x_26);
x_28 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_28, 0, x_27);
lean_ctor_set(x_28, 1, x_13);
x_29 = l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1___rarg(x_28, x_6, x_7, x_8, x_9, x_10, x_11, x_12);
lean_ctor_set(x_16, 0, x_14);
lean_ctor_set(x_16, 1, x_15);
x_17 = l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1___rarg(x_16, x_6, x_7, x_8, x_9, x_10, x_11, x_12);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_8);
return x_17;
}
else
{
lean_object* x_18; lean_object* x_19; lean_object* x_20;
lean_dec(x_2);
lean_dec(x_1);
x_18 = lean_ctor_get(x_4, 0);
lean_inc(x_18);
lean_dec(x_4);
x_19 = l_Lean_MessageData_Inhabited___closed__1;
x_20 = l_Lean_Meta_throwAppTypeMismatch___at_Lean_Elab_Term_throwTypeMismatchError___spec__1___rarg(x_18, x_3, x_19, x_6, x_7, x_8, x_9, x_10, x_11, x_12);
return x_20;
}
}
else
{
lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_21 = lean_ctor_get(x_5, 0);
x_22 = l_Lean_MessageData_ofList___closed__3;
lean_inc(x_21);
x_23 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_23, 0, x_22);
lean_ctor_set(x_23, 1, x_21);
if (lean_obj_tag(x_4) == 0)
{
lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27;
x_24 = l_Lean_Elab_Term_throwTypeMismatchError___rarg___closed__1;
x_25 = l_Lean_Elab_Term_mkTypeMismatchError(x_3, x_2, x_1, x_24);
x_26 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_26, 0, x_25);
lean_ctor_set(x_26, 1, x_23);
x_27 = l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1___rarg(x_26, x_6, x_7, x_8, x_9, x_10, x_11, x_12);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_8);
return x_27;
}
else
{
lean_object* x_28; lean_object* x_29;
lean_dec(x_2);
lean_dec(x_1);
x_28 = lean_ctor_get(x_4, 0);
lean_inc(x_28);
lean_dec(x_4);
x_29 = l_Lean_Meta_throwAppTypeMismatch___at_Lean_Elab_Term_throwTypeMismatchError___spec__3___rarg(x_28, x_3, x_23, x_6, x_7, x_8, x_9, x_10, x_11, x_12);
return x_29;
}
}
}
}
lean_object* l_Lean_Elab_Term_throwTypeMismatchError(lean_object* x_1) {
_start:
{
@ -28873,6 +28879,486 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* l_Lean_Elab_Term_elabTypeOf(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, lean_object* x_8, lean_object* x_9) {
_start:
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; uint8_t x_13; lean_object* x_14;
x_10 = lean_unsigned_to_nat(1u);
x_11 = l_Lean_Syntax_getArg(x_1, x_10);
x_12 = lean_box(0);
x_13 = 1;
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
x_14 = l_Lean_Elab_Term_elabTerm(x_11, x_12, x_13, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
if (lean_obj_tag(x_14) == 0)
{
lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
x_16 = lean_ctor_get(x_14, 1);
lean_inc(x_16);
lean_dec(x_14);
x_17 = l_Lean_Meta_inferType___at_Lean_Elab_Term_throwTypeMismatchError___spec__2(x_15, x_3, x_4, x_5, x_6, x_7, x_8, x_16);
lean_dec(x_4);
lean_dec(x_3);
return x_17;
}
else
{
uint8_t x_18;
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_18 = !lean_is_exclusive(x_14);
if (x_18 == 0)
{
return x_14;
}
else
{
lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_19 = lean_ctor_get(x_14, 0);
x_20 = lean_ctor_get(x_14, 1);
lean_inc(x_20);
lean_inc(x_19);
lean_dec(x_14);
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;
}
}
}
}
lean_object* l_Lean_Elab_Term_elabTypeOf___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, lean_object* x_8, lean_object* x_9) {
_start:
{
lean_object* x_10;
x_10 = l_Lean_Elab_Term_elabTypeOf(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
lean_dec(x_2);
lean_dec(x_1);
return x_10;
}
}
lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabTypeOf___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("typeOf");
return x_1;
}
}
lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabTypeOf___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_mkAppStx___closed__6;
x_2 = l___regBuiltin_Lean_Elab_Term_elabTypeOf___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabTypeOf___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabTypeOf___boxed), 9, 0);
return x_1;
}
}
lean_object* l___regBuiltin_Lean_Elab_Term_elabTypeOf(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_Elab_Term_termElabAttribute;
x_3 = l___regBuiltin_Lean_Elab_Term_elabTypeOf___closed__2;
x_4 = l___regBuiltin_Lean_Elab_Term_elabTypeOf___closed__3;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* l_Lean_Elab_Term_elabEnsureTypeOf(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, lean_object* x_8, lean_object* x_9) {
_start:
{
lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_10 = lean_unsigned_to_nat(2u);
x_11 = l_Lean_Syntax_getArg(x_1, x_10);
x_12 = l_Lean_Syntax_isStrLit_x3f(x_11);
lean_dec(x_11);
if (lean_obj_tag(x_12) == 0)
{
lean_object* x_13;
lean_dec(x_2);
x_13 = l_Lean_Elab_throwIllFormedSyntax___at_Lean_Elab_Term_elabStrLit___spec__1(x_3, x_4, x_5, x_6, x_7, x_8, x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
return x_13;
}
else
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18; lean_object* x_19;
x_14 = lean_ctor_get(x_12, 0);
lean_inc(x_14);
lean_dec(x_12);
x_15 = lean_unsigned_to_nat(1u);
x_16 = l_Lean_Syntax_getArg(x_1, x_15);
x_17 = lean_box(0);
x_18 = 1;
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
x_19 = l_Lean_Elab_Term_elabTerm(x_16, x_17, x_18, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
if (lean_obj_tag(x_19) == 0)
{
lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_20 = lean_ctor_get(x_19, 0);
lean_inc(x_20);
x_21 = lean_ctor_get(x_19, 1);
lean_inc(x_21);
lean_dec(x_19);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
x_22 = l_Lean_Meta_inferType___at_Lean_Elab_Term_throwTypeMismatchError___spec__2(x_20, x_3, x_4, x_5, x_6, x_7, x_8, x_21);
if (lean_obj_tag(x_22) == 0)
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27;
x_23 = lean_ctor_get(x_22, 0);
lean_inc(x_23);
x_24 = lean_ctor_get(x_22, 1);
lean_inc(x_24);
lean_dec(x_22);
x_25 = lean_unsigned_to_nat(3u);
x_26 = l_Lean_Syntax_getArg(x_1, x_25);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
x_27 = l_Lean_Elab_Term_elabTerm(x_26, x_2, x_18, x_3, x_4, x_5, x_6, x_7, x_8, x_24);
if (lean_obj_tag(x_27) == 0)
{
lean_object* x_28; lean_object* x_29; lean_object* x_30;
x_28 = lean_ctor_get(x_27, 0);
lean_inc(x_28);
x_29 = lean_ctor_get(x_27, 1);
lean_inc(x_29);
lean_dec(x_27);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_28);
x_30 = l_Lean_Meta_inferType___at_Lean_Elab_Term_throwTypeMismatchError___spec__2(x_28, x_3, x_4, x_5, x_6, x_7, x_8, x_29);
if (lean_obj_tag(x_30) == 0)
{
lean_object* x_31; lean_object* x_32; lean_object* x_33;
x_31 = lean_ctor_get(x_30, 0);
lean_inc(x_31);
x_32 = lean_ctor_get(x_30, 1);
lean_inc(x_32);
lean_dec(x_30);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_23);
lean_inc(x_31);
x_33 = l_Lean_Meta_isExprDefEq___at_Lean_Elab_Term_synthesizeInstMVarCore___spec__3(x_31, x_23, x_3, x_4, x_5, x_6, x_7, x_8, x_32);
if (lean_obj_tag(x_33) == 0)
{
lean_object* x_34; uint8_t x_35;
x_34 = lean_ctor_get(x_33, 0);
lean_inc(x_34);
x_35 = lean_unbox(x_34);
lean_dec(x_34);
if (x_35 == 0)
{
lean_object* x_36; lean_object* x_37; lean_object* x_38; uint8_t x_39;
x_36 = lean_ctor_get(x_33, 1);
lean_inc(x_36);
lean_dec(x_33);
x_37 = l_Lean_Elab_Term_mkTypeMismatchError(x_28, x_31, x_23, x_14);
x_38 = l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1___rarg(x_37, x_3, x_4, x_5, x_6, x_7, x_8, x_36);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
x_39 = !lean_is_exclusive(x_38);
if (x_39 == 0)
{
return x_38;
}
else
{
lean_object* x_40; lean_object* x_41; lean_object* x_42;
x_40 = lean_ctor_get(x_38, 0);
x_41 = lean_ctor_get(x_38, 1);
lean_inc(x_41);
lean_inc(x_40);
lean_dec(x_38);
x_42 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_42, 0, x_40);
lean_ctor_set(x_42, 1, x_41);
return x_42;
}
}
else
{
uint8_t x_43;
lean_dec(x_31);
lean_dec(x_23);
lean_dec(x_14);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_43 = !lean_is_exclusive(x_33);
if (x_43 == 0)
{
lean_object* x_44;
x_44 = lean_ctor_get(x_33, 0);
lean_dec(x_44);
lean_ctor_set(x_33, 0, x_28);
return x_33;
}
else
{
lean_object* x_45; lean_object* x_46;
x_45 = lean_ctor_get(x_33, 1);
lean_inc(x_45);
lean_dec(x_33);
x_46 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_46, 0, x_28);
lean_ctor_set(x_46, 1, x_45);
return x_46;
}
}
}
else
{
uint8_t x_47;
lean_dec(x_31);
lean_dec(x_28);
lean_dec(x_23);
lean_dec(x_14);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_47 = !lean_is_exclusive(x_33);
if (x_47 == 0)
{
return x_33;
}
else
{
lean_object* x_48; lean_object* x_49; lean_object* x_50;
x_48 = lean_ctor_get(x_33, 0);
x_49 = lean_ctor_get(x_33, 1);
lean_inc(x_49);
lean_inc(x_48);
lean_dec(x_33);
x_50 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_50, 0, x_48);
lean_ctor_set(x_50, 1, x_49);
return x_50;
}
}
}
else
{
uint8_t x_51;
lean_dec(x_28);
lean_dec(x_23);
lean_dec(x_14);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_51 = !lean_is_exclusive(x_30);
if (x_51 == 0)
{
return x_30;
}
else
{
lean_object* x_52; lean_object* x_53; lean_object* x_54;
x_52 = lean_ctor_get(x_30, 0);
x_53 = lean_ctor_get(x_30, 1);
lean_inc(x_53);
lean_inc(x_52);
lean_dec(x_30);
x_54 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_54, 0, x_52);
lean_ctor_set(x_54, 1, x_53);
return x_54;
}
}
}
else
{
uint8_t x_55;
lean_dec(x_23);
lean_dec(x_14);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_55 = !lean_is_exclusive(x_27);
if (x_55 == 0)
{
return x_27;
}
else
{
lean_object* x_56; lean_object* x_57; lean_object* x_58;
x_56 = lean_ctor_get(x_27, 0);
x_57 = lean_ctor_get(x_27, 1);
lean_inc(x_57);
lean_inc(x_56);
lean_dec(x_27);
x_58 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_58, 0, x_56);
lean_ctor_set(x_58, 1, x_57);
return x_58;
}
}
}
else
{
uint8_t x_59;
lean_dec(x_14);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_59 = !lean_is_exclusive(x_22);
if (x_59 == 0)
{
return x_22;
}
else
{
lean_object* x_60; lean_object* x_61; lean_object* x_62;
x_60 = lean_ctor_get(x_22, 0);
x_61 = lean_ctor_get(x_22, 1);
lean_inc(x_61);
lean_inc(x_60);
lean_dec(x_22);
x_62 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_62, 0, x_60);
lean_ctor_set(x_62, 1, x_61);
return x_62;
}
}
}
else
{
uint8_t x_63;
lean_dec(x_14);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_63 = !lean_is_exclusive(x_19);
if (x_63 == 0)
{
return x_19;
}
else
{
lean_object* x_64; lean_object* x_65; lean_object* x_66;
x_64 = lean_ctor_get(x_19, 0);
x_65 = lean_ctor_get(x_19, 1);
lean_inc(x_65);
lean_inc(x_64);
lean_dec(x_19);
x_66 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_66, 0, x_64);
lean_ctor_set(x_66, 1, x_65);
return x_66;
}
}
}
}
}
lean_object* l_Lean_Elab_Term_elabEnsureTypeOf___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, lean_object* x_8, lean_object* x_9) {
_start:
{
lean_object* x_10;
x_10 = l_Lean_Elab_Term_elabEnsureTypeOf(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
lean_dec(x_1);
return x_10;
}
}
lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabEnsureTypeOf___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("ensureTypeOf");
return x_1;
}
}
lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabEnsureTypeOf___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_mkAppStx___closed__6;
x_2 = l___regBuiltin_Lean_Elab_Term_elabEnsureTypeOf___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabEnsureTypeOf___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabEnsureTypeOf___boxed), 9, 0);
return x_1;
}
}
lean_object* l___regBuiltin_Lean_Elab_Term_elabEnsureTypeOf(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_Elab_Term_termElabAttribute;
x_3 = l___regBuiltin_Lean_Elab_Term_elabEnsureTypeOf___closed__2;
x_4 = l___regBuiltin_Lean_Elab_Term_elabEnsureTypeOf___closed__3;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* _init_l___private_Lean_Elab_Term_29__mkSomeContext___closed__1() {
_start:
{
@ -30730,10 +31216,6 @@ l___private_Lean_Elab_Term_4__expandCDot___main___closed__3 = _init_l___private_
lean_mark_persistent(l___private_Lean_Elab_Term_4__expandCDot___main___closed__3);
l_Lean_Elab_Term_throwTypeMismatchError___rarg___closed__1 = _init_l_Lean_Elab_Term_throwTypeMismatchError___rarg___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_throwTypeMismatchError___rarg___closed__1);
l_Lean_Elab_Term_throwTypeMismatchError___rarg___closed__2 = _init_l_Lean_Elab_Term_throwTypeMismatchError___rarg___closed__2();
lean_mark_persistent(l_Lean_Elab_Term_throwTypeMismatchError___rarg___closed__2);
l_Lean_Elab_Term_throwTypeMismatchError___rarg___closed__3 = _init_l_Lean_Elab_Term_throwTypeMismatchError___rarg___closed__3();
lean_mark_persistent(l_Lean_Elab_Term_throwTypeMismatchError___rarg___closed__3);
l_Lean_Elab_Term_synthesizeInstMVarCore___closed__1 = _init_l_Lean_Elab_Term_synthesizeInstMVarCore___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_synthesizeInstMVarCore___closed__1);
l_Lean_Elab_Term_synthesizeInstMVarCore___closed__2 = _init_l_Lean_Elab_Term_synthesizeInstMVarCore___closed__2();
@ -31068,6 +31550,24 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabQuotedName___closed__3);
res = l___regBuiltin_Lean_Elab_Term_elabQuotedName(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___regBuiltin_Lean_Elab_Term_elabTypeOf___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_elabTypeOf___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabTypeOf___closed__1);
l___regBuiltin_Lean_Elab_Term_elabTypeOf___closed__2 = _init_l___regBuiltin_Lean_Elab_Term_elabTypeOf___closed__2();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabTypeOf___closed__2);
l___regBuiltin_Lean_Elab_Term_elabTypeOf___closed__3 = _init_l___regBuiltin_Lean_Elab_Term_elabTypeOf___closed__3();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabTypeOf___closed__3);
res = l___regBuiltin_Lean_Elab_Term_elabTypeOf(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___regBuiltin_Lean_Elab_Term_elabEnsureTypeOf___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_elabEnsureTypeOf___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabEnsureTypeOf___closed__1);
l___regBuiltin_Lean_Elab_Term_elabEnsureTypeOf___closed__2 = _init_l___regBuiltin_Lean_Elab_Term_elabEnsureTypeOf___closed__2();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabEnsureTypeOf___closed__2);
l___regBuiltin_Lean_Elab_Term_elabEnsureTypeOf___closed__3 = _init_l___regBuiltin_Lean_Elab_Term_elabEnsureTypeOf___closed__3();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabEnsureTypeOf___closed__3);
res = l___regBuiltin_Lean_Elab_Term_elabEnsureTypeOf(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___private_Lean_Elab_Term_29__mkSomeContext___closed__1 = _init_l___private_Lean_Elab_Term_29__mkSomeContext___closed__1();
lean_mark_persistent(l___private_Lean_Elab_Term_29__mkSomeContext___closed__1);
l___private_Lean_Elab_Term_29__mkSomeContext___closed__2 = _init_l___private_Lean_Elab_Term_29__mkSomeContext___closed__2();

761
stage0/stdlib/Lean/Parser/Do.c generated
View file

@ -13,6 +13,7 @@
#ifdef __cplusplus
extern "C" {
#endif
lean_object* l_Lean_Parser_Term_doReassign___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_do___closed__4;
extern lean_object* l_Lean_Parser_Term_match___elambda__1___closed__6;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_visitToken___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -23,6 +24,7 @@ lean_object* l_Lean_Parser_Term_liftMethod_parenthesizer(lean_object*, lean_obje
lean_object* l_Lean_Parser_Term_doSeqBracketed_formatter___closed__2;
lean_object* l_Lean_Parser_Term_doIf_parenthesizer___closed__9;
lean_object* l_Lean_Parser_Term_doCatch___closed__1;
extern lean_object* l_Lean_Parser_Term_letIdDecl;
lean_object* l_Lean_Parser_many1Indent_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_binderType_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doDbgTrace_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -31,6 +33,7 @@ lean_object* l_Lean_Parser_Term_doPat_formatter(lean_object*, lean_object*, lean
lean_object* l_Lean_Parser_doElemParser(lean_object*);
lean_object* l_Lean_Parser_Term_doUnless_formatter___closed__2;
lean_object* l_Lean_Parser_Term_doSeqBracketed___closed__1;
extern lean_object* l_Lean_Parser_Term_letDecl_formatter___closed__6;
lean_object* l_Lean_Parser_Term_doMatch_parenthesizer___closed__5;
lean_object* l_Lean_Parser_Term_doSeqBracketed___closed__2;
extern lean_object* l_Lean_Parser_manyAux___main___closed__1;
@ -49,6 +52,7 @@ lean_object* l___regBuiltin_Lean_Parser_Term_do_parenthesizer(lean_object*);
lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_doIf___elambda__1___spec__1___closed__6;
lean_object* l_Lean_Parser_Term_continue_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doId_parenthesizer___closed__3;
extern lean_object* l_Lean_Parser_Term_letDecl_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Term_doPat___closed__3;
extern lean_object* l_Lean_Parser_Term_matchAlt___closed__3;
extern lean_object* l_Lean_Parser_Term_matchAlts_formatter___closed__10;
@ -68,6 +72,7 @@ lean_object* l_Lean_Parser_Term_doUnless___closed__6;
lean_object* l_Lean_Parser_Term_doIf_formatter___closed__20;
extern lean_object* l_Lean_nullKind;
lean_object* l_Lean_Parser_Term_doMatch_formatter___closed__6;
lean_object* l_Lean_Parser_Term_doReassign___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_continue_formatter___closed__1;
lean_object* l___regBuiltinParser_Lean_Parser_Term_doHave(lean_object*);
extern lean_object* l_Lean_Parser_Term_letrec___elambda__1___closed__6;
@ -79,7 +84,9 @@ lean_object* l_Lean_Parser_Term_doTry___closed__4;
lean_object* l_Lean_Parser_Term_doLetArrow___closed__1;
lean_object* l_Lean_Parser_Term_doSeqBracketed___closed__4;
lean_object* l_Lean_Parser_Term_doDbgTrace_formatter___closed__2;
extern lean_object* l_Lean_Parser_Term_letDecl_parenthesizer___closed__5;
lean_object* l_Lean_Parser_Term_doHave_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doReassign___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doFor___elambda__1___closed__8;
lean_object* l_Lean_Parser_Term_doExpr___elambda__1___closed__11;
lean_object* l_Lean_PrettyPrinter_Formatter_many_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -128,6 +135,7 @@ extern lean_object* l_Lean_Parser_Term_match___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_doDbgTrace___closed__4;
lean_object* l_Lean_Parser_Term_doCatchMatch_formatter___closed__1;
lean_object* l_Lean_Parser_Term_break___closed__6;
extern lean_object* l_Lean_Parser_Term_letPatDecl;
lean_object* l___regBuiltin_Lean_Parser_Term_doLetArrow_parenthesizer(lean_object*);
lean_object* l_Lean_Parser_Term_doFinally___closed__5;
extern lean_object* l_Lean_Parser_Term_binderTactic_parenthesizer___closed__2;
@ -137,6 +145,7 @@ lean_object* l_Lean_Parser_Term_doMatchAlts___elambda__1___closed__7;
lean_object* l_Lean_Parser_Term_doIf_parenthesizer___closed__4;
lean_object* l_Lean_Parser_Term_doAssert___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doCatch___closed__6;
lean_object* l_Lean_Parser_Term_doReassignArrow;
lean_object* l_Lean_Parser_Term_continue___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_doSeqBracketed___closed__8;
lean_object* l_Lean_Parser_Term_doUnless_parenthesizer___closed__3;
@ -170,6 +179,7 @@ lean_object* l_Lean_Parser_Term_doFor___closed__1;
extern lean_object* l_Lean_Parser_darrow;
lean_object* l_Lean_Parser_Term_return_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_doCatch___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_doReassign___closed__4;
lean_object* l_Lean_Parser_Term_doPat___closed__2;
lean_object* l_Lean_Parser_Term_doMatchAlts___closed__4;
extern lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___spec__1___closed__1;
@ -201,9 +211,11 @@ lean_object* l_Lean_Parser_Term_doExpr___closed__6;
lean_object* l_Lean_Parser_Term_doSeqBracketed_formatter___closed__1;
lean_object* l_Lean_Parser_Term_doDbgTrace___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doFor___closed__8;
lean_object* l___regBuiltin_Lean_Parser_Term_doReassignArrow_formatter(lean_object*);
lean_object* l_Lean_Parser_Term_doTry___elambda__1___closed__2;
lean_object* l___regBuiltin_Lean_Parser_Term_doFor_parenthesizer___closed__1;
lean_object* l_Lean_Parser_regDoElemParserAttribute___closed__1;
lean_object* l_Lean_Parser_Term_doReassignArrow_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Parser_Term_doLetRec_formatter___closed__1;
extern lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Term_matchAlts___spec__2___closed__2;
lean_object* l_Lean_Parser_Term_return_parenthesizer___closed__2;
@ -217,6 +229,7 @@ extern lean_object* l_Lean_Parser_Term_subtype_formatter___closed__6;
lean_object* l_Lean_Parser_Term_leftArrow_parenthesizer___boxed(lean_object*);
lean_object* lean_string_append(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doIf___closed__13;
lean_object* l_Lean_Parser_Term_doReassign___closed__1;
lean_object* l_Lean_Parser_Term_break___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_return_formatter___closed__3;
extern lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__18;
@ -242,6 +255,7 @@ lean_object* l_Lean_Parser_Term_doTry_parenthesizer___closed__5;
lean_object* l_Lean_Parser_Term_doMatchAlts_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Term_liftMethod___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_return;
lean_object* l_Lean_Parser_Term_doReassign___closed__2;
lean_object* l_Lean_Parser_Term_doCatch_parenthesizer___closed__8;
lean_object* l_Lean_Parser_Term_doId_parenthesizer___closed__5;
lean_object* l_Lean_Parser_Term_break___closed__3;
@ -263,6 +277,7 @@ lean_object* l_Lean_Parser_Term_doFor_formatter___closed__2;
lean_object* l_Lean_Parser_Term_doFor___elambda__1___closed__14;
lean_object* l_Lean_Parser_Term_doCatch___closed__2;
lean_object* l_Lean_Parser_Term_doAssert___closed__4;
lean_object* l_Lean_Parser_Term_doReassign;
lean_object* l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doTry_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_do___elambda__1___closed__2;
@ -291,7 +306,9 @@ lean_object* l_Lean_Parser_Term_liftMethod___closed__5;
lean_object* l_Lean_Parser_Term_doIf;
lean_object* l_Lean_Parser_checkPrecFn(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_return_formatter___closed__2;
lean_object* l___regBuiltin_Lean_Parser_Term_doReassignArrow_formatter___closed__1;
lean_object* l_Lean_Parser_Term_doIf_parenthesizer___closed__12;
lean_object* l_Lean_Parser_Term_doReassign___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_doIf___closed__4;
lean_object* l_Lean_Parser_Term_doLetArrow_parenthesizer___closed__4;
lean_object* l_Lean_Parser_Term_doUnless___elambda__1___closed__2;
@ -309,6 +326,7 @@ lean_object* l_Lean_Parser_Term_doIf___closed__5;
lean_object* l___regBuiltin_Lean_Parser_Term_doLetRec_parenthesizer(lean_object*);
lean_object* l_Lean_Parser_Term_return_formatter___closed__1;
extern lean_object* l_Lean_Parser_Term_assert___closed__2;
lean_object* l_Lean_Parser_Term_doReassignArrow___elambda__1(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Tactic_tacticSeqBracketed___elambda__1___closed__6;
lean_object* l_Lean_Parser_Term_doIf___closed__9;
lean_object* l_Lean_Parser_Term_doIf_parenthesizer___closed__14;
@ -316,6 +334,8 @@ lean_object* l_Lean_Parser_Term_doLetArrow_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_doLet_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doUnless___closed__9;
lean_object* l_Lean_Parser_Term_continue___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_doReassignArrow_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Parser_Term_doReassign_formatter(lean_object*);
lean_object* l_Lean_Parser_Term_doUnless___elambda__1___closed__1;
lean_object* l___regBuiltin_Lean_Parser_Term_doLet_formatter(lean_object*);
extern lean_object* l_Lean___kind_term____x40_Lean_Util_Trace___hyg_3____closed__15;
@ -329,10 +349,12 @@ extern lean_object* l_Lean_PrettyPrinter_parenthesizerAttribute;
lean_object* l_Lean_Parser_Term_liftMethod_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doLetRec___elambda__1(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_let___closed__2;
lean_object* l_Lean_Parser_Term_doReassign___closed__5;
lean_object* l_Lean_Parser_Term_leftArrow_parenthesizer___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doLetRec___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_doSeq_formatter___closed__1;
lean_object* l_Lean_Parser_Term_break___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doReassign_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Term_doMatchAlts_parenthesizer___closed__5;
lean_object* l_Lean_Parser_Term_doId_formatter___closed__4;
lean_object* l_Lean_Parser_Term_doIf___closed__8;
@ -364,6 +386,7 @@ lean_object* l___regBuiltin_Lean_Parser_Term_doTry_formatter(lean_object*);
lean_object* l_Lean_Parser_Term_doFor___closed__4;
extern lean_object* l_Lean_Parser_Term_structInst_parenthesizer___closed__6;
lean_object* l_Lean_Parser_regBuiltinDoElemParserAttr___closed__3;
lean_object* l___regBuiltin_Lean_Parser_Term_doReassignArrow_parenthesizer(lean_object*);
lean_object* l_Lean_Parser_Term_doMatch___elambda__1___closed__4;
lean_object* l_Lean_Parser_nodeInfo(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_continue_parenthesizer___closed__1;
@ -420,6 +443,7 @@ lean_object* l_Lean_Parser_Term_doFor___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_doMatchAlts_formatter___closed__6;
lean_object* l_Lean_Parser_Term_doExpr_formatter___closed__3;
lean_object* l_Lean_Parser_Term_doHave_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_letIdDecl___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_return___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_doMatch_parenthesizer___closed__4;
lean_object* l_Lean_Parser_Term_doAssert_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -438,6 +462,7 @@ lean_object* l_Lean_Parser_Term_doMatch___closed__3;
extern lean_object* l_Lean_Parser_Term_if___elambda__1___closed__6;
lean_object* l_Lean_Parser_Term_doHave_formatter___closed__1;
lean_object* l_Lean_Parser_Term_doId___elambda__1___closed__2;
lean_object* l___regBuiltinParser_Lean_Parser_Term_doReassignArrow___closed__1;
lean_object* l_Lean_Parser_Term_doSeqIndent___closed__4;
lean_object* l_Lean_Parser_Term_doLetArrow___closed__6;
lean_object* l_Lean_Parser_Term_doTry_parenthesizer___closed__9;
@ -470,10 +495,12 @@ lean_object* l_Lean_Parser_Term_doUnless___elambda__1___closed__8;
lean_object* l___regBuiltin_Lean_Parser_Term_break_formatter(lean_object*);
lean_object* l_Lean_Parser_doElemParser_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Char_HasRepr___closed__1;
lean_object* l_Lean_Parser_Term_doReassign___closed__3;
lean_object* l_Lean_Parser_Term_doSeqIndent___closed__5;
lean_object* l_Lean_Parser_Term_doExpr___elambda__1___closed__24;
lean_object* l_Lean_Parser_Term_doFor_formatter___closed__5;
lean_object* l___regBuiltin_Lean_Parser_Term_doFor_formatter(lean_object*);
lean_object* l___regBuiltinParser_Lean_Parser_Term_doReassignArrow___closed__2;
lean_object* l_Lean_Parser_Term_doCatch___elambda__1___closed__7;
lean_object* l_Lean_Parser_Term_continue___elambda__1___closed__1;
lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Term_tupleTail___elambda__1___spec__1(uint8_t, lean_object*, lean_object*);
@ -547,6 +574,7 @@ lean_object* l_Lean_Parser_Term_leftArrow___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_doCatchMatch___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_doExpr_formatter___closed__8;
lean_object* l_Lean_Parser_Term_do;
lean_object* l_Lean_Parser_Term_doReassign_formatter___closed__2;
lean_object* l_Lean_Parser_Term_doLetRec___closed__5;
lean_object* l_Lean_Parser_Term_doMatchAlts___closed__5;
lean_object* l_Lean_Parser_registerBuiltinParserAttribute(lean_object*, lean_object*, uint8_t, lean_object*);
@ -577,6 +605,7 @@ extern lean_object* l_Lean_Parser_Tactic_tacticSeqBracketed_formatter___closed__
lean_object* l_Lean_Parser_Term_doLetArrow_formatter___closed__6;
lean_object* l_Lean_Parser_Term_doUnless___closed__3;
lean_object* l_Lean_Parser_Term_doSeq_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_doReassign_formatter___closed__1;
lean_object* l_Lean_Parser_Term_doId_formatter___closed__5;
lean_object* l_Lean_Parser_Term_doLetArrow_parenthesizer___closed__6;
lean_object* l_Lean_Parser_Term_doAssert___elambda__1___closed__4;
@ -632,7 +661,9 @@ lean_object* l_Lean_Parser_Term_doLetRec_formatter(lean_object*, lean_object*, l
lean_object* l_Lean_Parser_Term_doUnless_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doAssert___elambda__1___closed__2;
lean_object* l_Lean_PrettyPrinter_Formatter_withPosition_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doReassign_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Term_optType___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doReassign_formatter___closed__3;
lean_object* l___regBuiltin_Lean_Parser_Term_doExpr_formatter(lean_object*);
lean_object* l_Lean_Parser_Term_liftMethod___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_doHave___closed__2;
@ -694,6 +725,8 @@ lean_object* l_Lean_Parser_Term_doAssert___closed__5;
lean_object* l_Lean_Parser_Term_doPat_formatter___closed__9;
extern lean_object* l_Lean_Parser_Term_matchAlt_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_ident___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doReassignArrow___closed__1;
lean_object* l___regBuiltin_Lean_Parser_Term_doReassign_parenthesizer(lean_object*);
extern lean_object* l_Lean_Parser_Term_match_formatter___closed__2;
lean_object* l_Lean_Parser_Term_doPat___closed__10;
lean_object* l_Lean_Parser_Term_doCatch_parenthesizer___closed__6;
@ -714,8 +747,10 @@ lean_object* l_Lean_Parser_Term_doIf_parenthesizer___closed__18;
lean_object* l_Lean_Parser_Term_doFor___closed__10;
lean_object* l_Lean_Parser_Term_doLetArrow_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Term_doLetArrow_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doReassign___closed__6;
lean_object* l_Lean_Parser_Term_doLetArrow___closed__7;
extern lean_object* l_Lean_Parser_Tactic_tacticSeqBracketed___elambda__1___closed__5;
extern lean_object* l_Lean_Parser_Term_letDecl_formatter___closed__3;
lean_object* l_Lean_Parser_Term_doAssert_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Term_doHave___closed__4;
lean_object* l_Lean_Parser_Term_liftMethod_parenthesizer___closed__1;
@ -795,6 +830,7 @@ extern lean_object* l_Lean_Parser_Term_if___elambda__1___closed__8;
lean_object* l_Lean_Parser_Term_doFor___elambda__1___closed__11;
lean_object* l___regBuiltin_Lean_Parser_Term_doMatch_parenthesizer(lean_object*);
extern lean_object* l_Lean_Parser_Term_matchAlts___closed__9;
lean_object* l_Lean_Parser_Term_doReassign___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_doIf_parenthesizer___closed__3;
lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Term_doMatchAlts___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doCatch_formatter___closed__6;
@ -828,6 +864,7 @@ lean_object* l_Lean_Parser_Term_doFor_formatter___closed__1;
lean_object* l_Lean_Parser_Term_doExpr_formatter___closed__9;
lean_object* l_Lean_Parser_Term_doSeqBracketed___elambda__1___closed__3;
extern lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_many1Indent___spec__1___closed__1;
lean_object* l_Lean_Parser_Term_doReassignArrow___closed__2;
lean_object* l_Lean_Parser_Term_doMatchAlts_parenthesizer___closed__6;
lean_object* l_Lean_Parser_Term_doTry___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_doIf_formatter___closed__3;
@ -864,6 +901,7 @@ lean_object* l_String_trim(lean_object*);
lean_object* l_Lean_Parser_Term_doSeq_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_continue___closed__5;
lean_object* l_Lean_Parser_Term_doExpr___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_doReassign_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_darrow___elambda__1(lean_object*, lean_object*);
lean_object* l___regBuiltinParser_Lean_Parser_Term_doLetRec(lean_object*);
lean_object* l_Lean_Parser_Term_doPat_parenthesizer___closed__6;
@ -916,8 +954,10 @@ lean_object* l_Lean_Parser_Term_doTry_parenthesizer___closed__7;
lean_object* l_Lean_Parser_Term_doId_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_regBuiltinDoElemParserAttr___closed__2;
lean_object* l_Lean_Parser_Term_doId_formatter___closed__1;
lean_object* l___regBuiltinParser_Lean_Parser_Term_doReassignArrow(lean_object*);
lean_object* l_Lean_Parser_Term_doPat_formatter___closed__8;
lean_object* l_Lean_Parser_Term_doSeqBracketed_parenthesizer___closed__5;
lean_object* l_Lean_Parser_Term_letPatDecl___elambda__1(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_have_formatter___closed__4;
extern lean_object* l_Lean_Parser_Term_if_formatter___closed__2;
lean_object* l_Lean_Parser_Term_doExpr___elambda__1___closed__13;
@ -926,6 +966,7 @@ lean_object* l_Lean_Parser_Term_doLet___elambda__1___closed__2;
lean_object* l_Lean_Parser_mkAntiquot(lean_object*, lean_object*, uint8_t);
lean_object* l___regBuiltin_Lean_Parser_Term_doExpr_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_doFor___elambda__1___closed__6;
lean_object* l___regBuiltin_Lean_Parser_Term_doReassignArrow_parenthesizer___closed__1;
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_Term_doExpr_formatter___closed__11;
lean_object* l_Lean_Parser_Term_doIf_formatter___closed__15;
@ -1002,11 +1043,15 @@ lean_object* l_Lean_Parser_Term_doIf_parenthesizer___closed__10;
lean_object* l_Lean_Parser_Term_doExpr___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_doLetArrow_formatter___closed__2;
lean_object* l_Lean_Parser_Term_doUnless_formatter___closed__4;
lean_object* l_Lean_Parser_Term_doReassign_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doMatchAlts___closed__6;
lean_object* l_Lean_Parser_Term_doIf___closed__19;
lean_object* l___regBuiltin_Lean_Parser_Term_doReassign_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_doPat___closed__5;
lean_object* l___regBuiltin_Lean_Parser_Term_doReassign_formatter___closed__1;
lean_object* l_Lean_Parser_Term_doMatch___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_doSeqBracketed___elambda__1___closed__4;
lean_object* l___regBuiltinParser_Lean_Parser_Term_doReassign(lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_notFollowedBy_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doHave_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_do___elambda__1(lean_object*, lean_object*);
@ -1068,6 +1113,7 @@ lean_object* l_Lean_Parser_Term_doHave___elambda__1(lean_object*, lean_object*);
extern lean_object* l___regBuiltin_Lean_Parser_Term_ident_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_Term_doTry___closed__5;
lean_object* l_Lean_Parser_Term_doReassign_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_doIf___closed__11;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_try_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_regDoElemParserAttribute(lean_object*);
@ -6909,6 +6955,651 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* _init_l_Lean_Parser_Term_doReassign___elambda__1___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("doReassign");
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Term_doReassign___elambda__1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_mkAppStx___closed__6;
x_2 = l_Lean_Parser_Term_doReassign___elambda__1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_doReassign___elambda__1___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Term_doReassign___elambda__1___closed__2;
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Parser_Term_doReassign___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_Term_doReassign___elambda__1___closed__1;
x_2 = l_Lean_Parser_Term_doReassign___elambda__1___closed__3;
x_3 = 1;
x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
return x_4;
}
}
lean_object* l_Lean_Parser_Term_doReassign___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; uint8_t x_5;
x_3 = l_Lean_Parser_Term_doReassign___elambda__1___closed__4;
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
lean_inc(x_2);
lean_inc(x_1);
x_5 = l_Lean_Parser_tryAnti(x_1, x_2);
if (x_5 == 0)
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
lean_dec(x_4);
x_6 = lean_unsigned_to_nat(1024u);
x_7 = l_Lean_Parser_checkPrecFn(x_6, x_1, x_2);
x_8 = lean_ctor_get(x_7, 3);
lean_inc(x_8);
if (lean_obj_tag(x_8) == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_9 = lean_ctor_get(x_7, 0);
lean_inc(x_9);
x_10 = lean_array_get_size(x_9);
lean_dec(x_9);
x_11 = lean_ctor_get(x_7, 1);
lean_inc(x_11);
lean_inc(x_1);
x_12 = l_Lean_Parser_Term_letIdDecl___elambda__1(x_1, x_7);
x_13 = lean_ctor_get(x_12, 3);
lean_inc(x_13);
if (lean_obj_tag(x_13) == 0)
{
lean_object* x_14; lean_object* x_15;
lean_dec(x_11);
lean_dec(x_1);
x_14 = l_Lean_Parser_Term_doReassign___elambda__1___closed__2;
x_15 = l_Lean_Parser_ParserState_mkNode(x_12, x_14, x_10);
return x_15;
}
else
{
lean_object* x_16; lean_object* x_17; uint8_t x_18;
x_16 = lean_ctor_get(x_13, 0);
lean_inc(x_16);
lean_dec(x_13);
x_17 = lean_ctor_get(x_12, 1);
lean_inc(x_17);
x_18 = lean_nat_dec_eq(x_17, x_11);
lean_dec(x_17);
if (x_18 == 0)
{
lean_object* x_19; lean_object* x_20;
lean_dec(x_16);
lean_dec(x_11);
lean_dec(x_1);
x_19 = l_Lean_Parser_Term_doReassign___elambda__1___closed__2;
x_20 = l_Lean_Parser_ParserState_mkNode(x_12, x_19, x_10);
return x_20;
}
else
{
lean_object* x_21; lean_object* x_22; uint8_t x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
lean_inc(x_11);
x_21 = l_Lean_Parser_ParserState_restore(x_12, x_10, x_11);
x_22 = l_Lean_Parser_Term_letPatDecl___elambda__1(x_1, x_21);
x_23 = 1;
x_24 = l_Lean_Parser_mergeOrElseErrors(x_22, x_16, x_11, x_23);
lean_dec(x_11);
x_25 = l_Lean_Parser_Term_doReassign___elambda__1___closed__2;
x_26 = l_Lean_Parser_ParserState_mkNode(x_24, x_25, x_10);
return x_26;
}
}
}
else
{
lean_dec(x_8);
lean_dec(x_1);
return x_7;
}
}
else
{
lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31;
x_27 = lean_ctor_get(x_2, 0);
lean_inc(x_27);
x_28 = lean_array_get_size(x_27);
lean_dec(x_27);
x_29 = lean_ctor_get(x_2, 1);
lean_inc(x_29);
lean_inc(x_1);
x_30 = lean_apply_2(x_4, x_1, x_2);
x_31 = lean_ctor_get(x_30, 3);
lean_inc(x_31);
if (lean_obj_tag(x_31) == 0)
{
lean_dec(x_29);
lean_dec(x_28);
lean_dec(x_1);
return x_30;
}
else
{
lean_object* x_32; lean_object* x_33; uint8_t x_34;
x_32 = lean_ctor_get(x_31, 0);
lean_inc(x_32);
lean_dec(x_31);
x_33 = lean_ctor_get(x_30, 1);
lean_inc(x_33);
x_34 = lean_nat_dec_eq(x_33, x_29);
lean_dec(x_33);
if (x_34 == 0)
{
lean_dec(x_32);
lean_dec(x_29);
lean_dec(x_28);
lean_dec(x_1);
return x_30;
}
else
{
lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38;
lean_inc(x_29);
x_35 = l_Lean_Parser_ParserState_restore(x_30, x_28, x_29);
lean_dec(x_28);
x_36 = lean_unsigned_to_nat(1024u);
x_37 = l_Lean_Parser_checkPrecFn(x_36, x_1, x_35);
x_38 = lean_ctor_get(x_37, 3);
lean_inc(x_38);
if (lean_obj_tag(x_38) == 0)
{
lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43;
x_39 = lean_ctor_get(x_37, 0);
lean_inc(x_39);
x_40 = lean_array_get_size(x_39);
lean_dec(x_39);
x_41 = lean_ctor_get(x_37, 1);
lean_inc(x_41);
lean_inc(x_1);
x_42 = l_Lean_Parser_Term_letIdDecl___elambda__1(x_1, x_37);
x_43 = lean_ctor_get(x_42, 3);
lean_inc(x_43);
if (lean_obj_tag(x_43) == 0)
{
lean_object* x_44; lean_object* x_45; uint8_t x_46; lean_object* x_47;
lean_dec(x_41);
lean_dec(x_1);
x_44 = l_Lean_Parser_Term_doReassign___elambda__1___closed__2;
x_45 = l_Lean_Parser_ParserState_mkNode(x_42, x_44, x_40);
x_46 = 1;
x_47 = l_Lean_Parser_mergeOrElseErrors(x_45, x_32, x_29, x_46);
lean_dec(x_29);
return x_47;
}
else
{
lean_object* x_48; lean_object* x_49; uint8_t x_50;
x_48 = lean_ctor_get(x_43, 0);
lean_inc(x_48);
lean_dec(x_43);
x_49 = lean_ctor_get(x_42, 1);
lean_inc(x_49);
x_50 = lean_nat_dec_eq(x_49, x_41);
lean_dec(x_49);
if (x_50 == 0)
{
lean_object* x_51; lean_object* x_52; uint8_t x_53; lean_object* x_54;
lean_dec(x_48);
lean_dec(x_41);
lean_dec(x_1);
x_51 = l_Lean_Parser_Term_doReassign___elambda__1___closed__2;
x_52 = l_Lean_Parser_ParserState_mkNode(x_42, x_51, x_40);
x_53 = 1;
x_54 = l_Lean_Parser_mergeOrElseErrors(x_52, x_32, x_29, x_53);
lean_dec(x_29);
return x_54;
}
else
{
lean_object* x_55; lean_object* x_56; uint8_t x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61;
lean_inc(x_41);
x_55 = l_Lean_Parser_ParserState_restore(x_42, x_40, x_41);
x_56 = l_Lean_Parser_Term_letPatDecl___elambda__1(x_1, x_55);
x_57 = 1;
x_58 = l_Lean_Parser_mergeOrElseErrors(x_56, x_48, x_41, x_57);
lean_dec(x_41);
x_59 = l_Lean_Parser_Term_doReassign___elambda__1___closed__2;
x_60 = l_Lean_Parser_ParserState_mkNode(x_58, x_59, x_40);
x_61 = l_Lean_Parser_mergeOrElseErrors(x_60, x_32, x_29, x_57);
lean_dec(x_29);
return x_61;
}
}
}
else
{
uint8_t x_62; lean_object* x_63;
lean_dec(x_38);
lean_dec(x_1);
x_62 = 1;
x_63 = l_Lean_Parser_mergeOrElseErrors(x_37, x_32, x_29, x_62);
lean_dec(x_29);
return x_63;
}
}
}
}
}
}
lean_object* _init_l_Lean_Parser_Term_doReassign___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_Parser_Term_letIdDecl;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Term_letPatDecl;
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
x_5 = l_Lean_Parser_orelseInfo(x_2, x_4);
return x_5;
}
}
lean_object* _init_l_Lean_Parser_Term_doReassign___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_doReassign___elambda__1___closed__2;
x_2 = l_Lean_Parser_Term_doReassign___closed__1;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_doReassign___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_epsilonInfo;
x_2 = l_Lean_Parser_Term_doReassign___closed__2;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_doReassign___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_doReassign___elambda__1___closed__4;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Term_doReassign___closed__3;
x_4 = l_Lean_Parser_orelseInfo(x_2, x_3);
return x_4;
}
}
lean_object* _init_l_Lean_Parser_Term_doReassign___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_doReassign___elambda__1), 2, 0);
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Term_doReassign___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_doReassign___closed__4;
x_2 = l_Lean_Parser_Term_doReassign___closed__5;
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;
}
}
lean_object* _init_l_Lean_Parser_Term_doReassign() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Term_doReassign___closed__6;
return x_1;
}
}
lean_object* l___regBuiltinParser_Lean_Parser_Term_doReassign(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_regBuiltinDoElemParserAttr___closed__4;
x_3 = l_Lean_Parser_Term_doReassign___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Term_doReassign;
x_6 = lean_unsigned_to_nat(0u);
x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
return x_7;
}
}
lean_object* _init_l_Lean_Parser_Term_doReassign_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_Term_doReassign___elambda__1___closed__1;
x_2 = l_Lean_Parser_Term_doReassign___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;
}
}
lean_object* _init_l_Lean_Parser_Term_doReassign_formatter___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_letDecl_formatter___closed__6;
x_2 = l_Lean_Parser_Term_letDecl_formatter___closed__3;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_orelse_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_doReassign_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_Term_doReassign___elambda__1___closed__2;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Term_doReassign_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_Term_doReassign_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_Term_doReassign_formatter___closed__1;
x_7 = l_Lean_Parser_Term_doReassign_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;
}
}
lean_object* _init_l___regBuiltin_Lean_Parser_Term_doReassign_formatter___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_doReassign_formatter), 5, 0);
return x_1;
}
}
lean_object* l___regBuiltin_Lean_Parser_Term_doReassign_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_Term_doReassign___elambda__1___closed__2;
x_4 = l___regBuiltin_Lean_Parser_Term_doReassign_formatter___closed__1;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* _init_l_Lean_Parser_Term_doReassign_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_Term_doReassign___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;
}
}
lean_object* _init_l_Lean_Parser_Term_doReassign_parenthesizer___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_letDecl_parenthesizer___closed__5;
x_2 = l_Lean_Parser_Term_letDecl_parenthesizer___closed__2;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_orelse_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_doReassign_parenthesizer___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_doReassign___elambda__1___closed__2;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Term_doReassign_parenthesizer___closed__2;
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_Term_doReassign_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_Term_doReassign_parenthesizer___closed__1;
x_7 = l_Lean_Parser_Term_doReassign_parenthesizer___closed__3;
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;
}
}
lean_object* _init_l___regBuiltin_Lean_Parser_Term_doReassign_parenthesizer___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_doReassign_parenthesizer), 5, 0);
return x_1;
}
}
lean_object* l___regBuiltin_Lean_Parser_Term_doReassign_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_Term_doReassign___elambda__1___closed__2;
x_4 = l___regBuiltin_Lean_Parser_Term_doReassign_parenthesizer___closed__1;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* l_Lean_Parser_Term_doReassignArrow___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
x_4 = lean_array_get_size(x_3);
lean_dec(x_3);
x_5 = lean_ctor_get(x_2, 1);
lean_inc(x_5);
lean_inc(x_1);
x_6 = l_Lean_Parser_Term_doId___elambda__1(x_1, x_2);
x_7 = lean_ctor_get(x_6, 3);
lean_inc(x_7);
if (lean_obj_tag(x_7) == 0)
{
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_1);
return x_6;
}
else
{
lean_object* x_8; lean_object* x_9; uint8_t x_10;
x_8 = lean_ctor_get(x_7, 0);
lean_inc(x_8);
lean_dec(x_7);
x_9 = lean_ctor_get(x_6, 1);
lean_inc(x_9);
x_10 = lean_nat_dec_eq(x_9, x_5);
lean_dec(x_9);
if (x_10 == 0)
{
lean_dec(x_8);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_1);
return x_6;
}
else
{
lean_object* x_11; lean_object* x_12; uint8_t x_13; lean_object* x_14;
lean_inc(x_5);
x_11 = l_Lean_Parser_ParserState_restore(x_6, x_4, x_5);
lean_dec(x_4);
x_12 = l_Lean_Parser_Term_doPat___elambda__1(x_1, x_11);
x_13 = 1;
x_14 = l_Lean_Parser_mergeOrElseErrors(x_12, x_8, x_5, x_13);
lean_dec(x_5);
return x_14;
}
}
}
}
lean_object* _init_l_Lean_Parser_Term_doReassignArrow___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_doReassignArrow___elambda__1), 2, 0);
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Term_doReassignArrow___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_doLetArrow___closed__1;
x_2 = l_Lean_Parser_Term_doReassignArrow___closed__1;
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;
}
}
lean_object* _init_l_Lean_Parser_Term_doReassignArrow() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Term_doReassignArrow___closed__2;
return x_1;
}
}
lean_object* _init_l___regBuiltinParser_Lean_Parser_Term_doReassignArrow___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("doReassignArrow");
return x_1;
}
}
lean_object* _init_l___regBuiltinParser_Lean_Parser_Term_doReassignArrow___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_mkAppStx___closed__6;
x_2 = l___regBuiltinParser_Lean_Parser_Term_doReassignArrow___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l___regBuiltinParser_Lean_Parser_Term_doReassignArrow(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_regBuiltinDoElemParserAttr___closed__4;
x_3 = l___regBuiltinParser_Lean_Parser_Term_doReassignArrow___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Term_doReassignArrow;
x_6 = lean_unsigned_to_nat(0u);
x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
return x_7;
}
}
lean_object* l_Lean_Parser_Term_doReassignArrow_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_Term_doLetArrow_formatter___closed__2;
x_7 = l_Lean_Parser_Term_doLetArrow_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;
}
}
lean_object* _init_l___regBuiltin_Lean_Parser_Term_doReassignArrow_formatter___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_doReassignArrow_formatter), 5, 0);
return x_1;
}
}
lean_object* l___regBuiltin_Lean_Parser_Term_doReassignArrow_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___regBuiltinParser_Lean_Parser_Term_doReassignArrow___closed__2;
x_4 = l___regBuiltin_Lean_Parser_Term_doReassignArrow_formatter___closed__1;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* l_Lean_Parser_Term_doReassignArrow_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_Term_doLetArrow_parenthesizer___closed__2;
x_7 = l_Lean_Parser_Term_doLetArrow_parenthesizer___closed__3;
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;
}
}
lean_object* _init_l___regBuiltin_Lean_Parser_Term_doReassignArrow_parenthesizer___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_doReassignArrow_parenthesizer), 5, 0);
return x_1;
}
}
lean_object* l___regBuiltin_Lean_Parser_Term_doReassignArrow_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___regBuiltinParser_Lean_Parser_Term_doReassignArrow___closed__2;
x_4 = l___regBuiltin_Lean_Parser_Term_doReassignArrow_parenthesizer___closed__1;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* _init_l_Lean_Parser_Term_doHave___elambda__1___closed__1() {
_start:
{
@ -24586,6 +25277,76 @@ lean_mark_persistent(l___regBuiltin_Lean_Parser_Term_doLetArrow_parenthesizer___
res = l___regBuiltin_Lean_Parser_Term_doLetArrow_parenthesizer(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_Term_doReassign___elambda__1___closed__1 = _init_l_Lean_Parser_Term_doReassign___elambda__1___closed__1();
lean_mark_persistent(l_Lean_Parser_Term_doReassign___elambda__1___closed__1);
l_Lean_Parser_Term_doReassign___elambda__1___closed__2 = _init_l_Lean_Parser_Term_doReassign___elambda__1___closed__2();
lean_mark_persistent(l_Lean_Parser_Term_doReassign___elambda__1___closed__2);
l_Lean_Parser_Term_doReassign___elambda__1___closed__3 = _init_l_Lean_Parser_Term_doReassign___elambda__1___closed__3();
lean_mark_persistent(l_Lean_Parser_Term_doReassign___elambda__1___closed__3);
l_Lean_Parser_Term_doReassign___elambda__1___closed__4 = _init_l_Lean_Parser_Term_doReassign___elambda__1___closed__4();
lean_mark_persistent(l_Lean_Parser_Term_doReassign___elambda__1___closed__4);
l_Lean_Parser_Term_doReassign___closed__1 = _init_l_Lean_Parser_Term_doReassign___closed__1();
lean_mark_persistent(l_Lean_Parser_Term_doReassign___closed__1);
l_Lean_Parser_Term_doReassign___closed__2 = _init_l_Lean_Parser_Term_doReassign___closed__2();
lean_mark_persistent(l_Lean_Parser_Term_doReassign___closed__2);
l_Lean_Parser_Term_doReassign___closed__3 = _init_l_Lean_Parser_Term_doReassign___closed__3();
lean_mark_persistent(l_Lean_Parser_Term_doReassign___closed__3);
l_Lean_Parser_Term_doReassign___closed__4 = _init_l_Lean_Parser_Term_doReassign___closed__4();
lean_mark_persistent(l_Lean_Parser_Term_doReassign___closed__4);
l_Lean_Parser_Term_doReassign___closed__5 = _init_l_Lean_Parser_Term_doReassign___closed__5();
lean_mark_persistent(l_Lean_Parser_Term_doReassign___closed__5);
l_Lean_Parser_Term_doReassign___closed__6 = _init_l_Lean_Parser_Term_doReassign___closed__6();
lean_mark_persistent(l_Lean_Parser_Term_doReassign___closed__6);
l_Lean_Parser_Term_doReassign = _init_l_Lean_Parser_Term_doReassign();
lean_mark_persistent(l_Lean_Parser_Term_doReassign);
res = l___regBuiltinParser_Lean_Parser_Term_doReassign(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_Term_doReassign_formatter___closed__1 = _init_l_Lean_Parser_Term_doReassign_formatter___closed__1();
lean_mark_persistent(l_Lean_Parser_Term_doReassign_formatter___closed__1);
l_Lean_Parser_Term_doReassign_formatter___closed__2 = _init_l_Lean_Parser_Term_doReassign_formatter___closed__2();
lean_mark_persistent(l_Lean_Parser_Term_doReassign_formatter___closed__2);
l_Lean_Parser_Term_doReassign_formatter___closed__3 = _init_l_Lean_Parser_Term_doReassign_formatter___closed__3();
lean_mark_persistent(l_Lean_Parser_Term_doReassign_formatter___closed__3);
l___regBuiltin_Lean_Parser_Term_doReassign_formatter___closed__1 = _init_l___regBuiltin_Lean_Parser_Term_doReassign_formatter___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Term_doReassign_formatter___closed__1);
res = l___regBuiltin_Lean_Parser_Term_doReassign_formatter(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_Term_doReassign_parenthesizer___closed__1 = _init_l_Lean_Parser_Term_doReassign_parenthesizer___closed__1();
lean_mark_persistent(l_Lean_Parser_Term_doReassign_parenthesizer___closed__1);
l_Lean_Parser_Term_doReassign_parenthesizer___closed__2 = _init_l_Lean_Parser_Term_doReassign_parenthesizer___closed__2();
lean_mark_persistent(l_Lean_Parser_Term_doReassign_parenthesizer___closed__2);
l_Lean_Parser_Term_doReassign_parenthesizer___closed__3 = _init_l_Lean_Parser_Term_doReassign_parenthesizer___closed__3();
lean_mark_persistent(l_Lean_Parser_Term_doReassign_parenthesizer___closed__3);
l___regBuiltin_Lean_Parser_Term_doReassign_parenthesizer___closed__1 = _init_l___regBuiltin_Lean_Parser_Term_doReassign_parenthesizer___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Term_doReassign_parenthesizer___closed__1);
res = l___regBuiltin_Lean_Parser_Term_doReassign_parenthesizer(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_Term_doReassignArrow___closed__1 = _init_l_Lean_Parser_Term_doReassignArrow___closed__1();
lean_mark_persistent(l_Lean_Parser_Term_doReassignArrow___closed__1);
l_Lean_Parser_Term_doReassignArrow___closed__2 = _init_l_Lean_Parser_Term_doReassignArrow___closed__2();
lean_mark_persistent(l_Lean_Parser_Term_doReassignArrow___closed__2);
l_Lean_Parser_Term_doReassignArrow = _init_l_Lean_Parser_Term_doReassignArrow();
lean_mark_persistent(l_Lean_Parser_Term_doReassignArrow);
l___regBuiltinParser_Lean_Parser_Term_doReassignArrow___closed__1 = _init_l___regBuiltinParser_Lean_Parser_Term_doReassignArrow___closed__1();
lean_mark_persistent(l___regBuiltinParser_Lean_Parser_Term_doReassignArrow___closed__1);
l___regBuiltinParser_Lean_Parser_Term_doReassignArrow___closed__2 = _init_l___regBuiltinParser_Lean_Parser_Term_doReassignArrow___closed__2();
lean_mark_persistent(l___regBuiltinParser_Lean_Parser_Term_doReassignArrow___closed__2);
res = l___regBuiltinParser_Lean_Parser_Term_doReassignArrow(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___regBuiltin_Lean_Parser_Term_doReassignArrow_formatter___closed__1 = _init_l___regBuiltin_Lean_Parser_Term_doReassignArrow_formatter___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Term_doReassignArrow_formatter___closed__1);
res = l___regBuiltin_Lean_Parser_Term_doReassignArrow_formatter(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___regBuiltin_Lean_Parser_Term_doReassignArrow_parenthesizer___closed__1 = _init_l___regBuiltin_Lean_Parser_Term_doReassignArrow_parenthesizer___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Term_doReassignArrow_parenthesizer___closed__1);
res = l___regBuiltin_Lean_Parser_Term_doReassignArrow_parenthesizer(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_Term_doHave___elambda__1___closed__1 = _init_l_Lean_Parser_Term_doHave___elambda__1___closed__1();
lean_mark_persistent(l_Lean_Parser_Term_doHave___elambda__1___closed__1);
l_Lean_Parser_Term_doHave___elambda__1___closed__2 = _init_l_Lean_Parser_Term_doHave___elambda__1___closed__2();