From e8b58abffcf2eadc436435cf6e6733827d818ed6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 2 Dec 2020 15:32:17 -0800 Subject: [PATCH] chore: update stage0 --- stage0/src/Lean/Elab/Term.lean | 24 +- stage0/src/Lean/Parser.lean | 2 + stage0/src/Lean/Parser/Basic.lean | 2 +- .../PrettyPrinter/Delaborator/Builtins.lean | 9 + stage0/stdlib/Lean/Elab/Binders.c | 44 +- stage0/stdlib/Lean/Elab/Term.c | 1047 ++++++++++------- stage0/stdlib/Lean/Parser.c | 75 ++ stage0/stdlib/Lean/Parser/Basic.c | 78 +- .../Lean/PrettyPrinter/Delaborator/Builtins.c | 359 +++++- 9 files changed, 1178 insertions(+), 462 deletions(-) diff --git a/stage0/src/Lean/Elab/Term.lean b/stage0/src/Lean/Elab/Term.lean index e7595a937d..a7d66f4b7b 100644 --- a/stage0/src/Lean/Elab/Term.lean +++ b/stage0/src/Lean/Elab/Term.lean @@ -1253,16 +1253,19 @@ def resolveName (n : Name) (preresolved : List (Name × List String)) (explicitL | some val => pure $ mkStrLit val | none => throwIllFormedSyntax -@[builtinTermElab numLit] def elabNumLit : TermElab := fun stx expectedType? => do - let val ← match stx.isNatLit? with - | some val => pure val - | none => throwIllFormedSyntax +private def mkFreshTypeMVarFor (expectedType? : Option Expr) : TermElabM Expr := do let typeMVar ← mkFreshTypeMVar MetavarKind.synthetic match expectedType? with | some expectedType => isDefEq expectedType typeMVar; pure () | _ => pure () - let u ← getLevel typeMVar - let u ← decLevel u + return typeMVar + +@[builtinTermElab numLit] def elabNumLit : TermElab := fun stx expectedType? => do + let val ← match stx.isNatLit? with + | some val => pure val + | none => throwIllFormedSyntax + let typeMVar ← mkFreshTypeMVarFor expectedType? + let u ← getDecLevel typeMVar let mvar ← mkInstMVar (mkApp2 (Lean.mkConst `OfNat [u]) typeMVar (mkNatLit val)) return mkApp3 (Lean.mkConst `OfNat.ofNat [u]) typeMVar (mkNatLit val) mvar @@ -1271,6 +1274,15 @@ def resolveName (n : Name) (preresolved : List (Name × List String)) (explicitL | some val => return mkNatLit val | none => throwIllFormedSyntax +@[builtinTermElab decimalLit] def elabDecimalLit : TermElab := fun stx expectedType? => do + match stx.isDecimalLit? with + | none => throwIllFormedSyntax + | some (m, e) => + let typeMVar ← mkFreshTypeMVarFor expectedType? + let u ← getDecLevel typeMVar + let mvar ← mkInstMVar (mkApp (Lean.mkConst `OfDecimal [u]) typeMVar) + return mkApp4 (Lean.mkConst `OfDecimal.ofDecimal [u]) typeMVar mvar (mkNatLit m) (mkNatLit e) + @[builtinTermElab charLit] def elabCharLit : TermElab := fun stx _ => do match stx.isCharLit? with | some val => return mkApp (Lean.mkConst `Char.ofNat) (mkNatLit val.toNat) diff --git a/stage0/src/Lean/Parser.lean b/stage0/src/Lean/Parser.lean index 57c34a6279..5f30dfd520 100644 --- a/stage0/src/Lean/Parser.lean +++ b/stage0/src/Lean/Parser.lean @@ -25,6 +25,7 @@ def mkAntiquot.parenthesizer (name : String) (kind : Option SyntaxNodeKind) (ano -- (e.g. `ident`) is not equal to the parser name `Lean.Parser.Term.ident`. @[builtinParenthesizer ident] def ident.parenthesizer : Parenthesizer := Parser.Term.ident.parenthesizer @[builtinParenthesizer numLit] def numLit.parenthesizer : Parenthesizer := Parser.Term.num.parenthesizer +@[builtinParenthesizer decimalLit] def decimalLit.parenthesizer : Parenthesizer := Parser.Term.decimal.parenthesizer @[builtinParenthesizer charLit] def charLit.parenthesizer : Parenthesizer := Parser.Term.char.parenthesizer @[builtinParenthesizer strLit] def strLit.parenthesizer : Parenthesizer := Parser.Term.str.parenthesizer @@ -38,6 +39,7 @@ def mkAntiquot.formatter (name : String) (kind : Option SyntaxNodeKind) (anonymo @[builtinFormatter ident] def ident.formatter : Formatter := Parser.Term.ident.formatter @[builtinFormatter numLit] def numLit.formatter : Formatter := Parser.Term.num.formatter +@[builtinFormatter decimalLit] def decimalLit.formatter : Formatter := Parser.Term.decimal.formatter @[builtinFormatter charLit] def charLit.formatter : Formatter := Parser.Term.char.formatter @[builtinFormatter strLit] def strLit.formatter : Formatter := Parser.Term.str.formatter diff --git a/stage0/src/Lean/Parser/Basic.lean b/stage0/src/Lean/Parser/Basic.lean index 3bbc621874..ed3f36ad5b 100644 --- a/stage0/src/Lean/Parser/Basic.lean +++ b/stage0/src/Lean/Parser/Basic.lean @@ -819,7 +819,7 @@ def decimalNumberFn (startPos : Nat) : ParserFn := fun c s => if curr.isDigit then takeWhileFn (fun c => c.isDigit) c (s.setPos i) else - s + s.setPos i mkNodeToken decimalLitKind startPos c s else mkNodeToken numLitKind startPos c s diff --git a/stage0/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/stage0/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index 73fa494a3e..bb57f94ca5 100644 --- a/stage0/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/stage0/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -368,6 +368,15 @@ def delabOfNat : Delab := whenPPOption getPPCoercions do let (Expr.app (Expr.app _ (Expr.lit (Literal.natVal n) _) _) _ _) ← getExpr | failure return quote n +-- `@OfDecimal.ofDecimal _ _ m e` ~> `m*10^(-e)` +@[builtinDelab app.OfDecimal.ofDecimal] +def delabOfDecimal : Delab := whenPPOption getPPCoercions do + let (Expr.app (Expr.app _ (Expr.lit (Literal.natVal m) _) _) (Expr.lit (Literal.natVal e) _) _) ← getExpr | failure + let str := toString m + let mStr := str.extract 0 (str.length - e) + let eStr := str.extract (str.length - e) str.length + return Syntax.mkDecimalLit (mStr ++ "." ++ eStr) + /-- Delaborate a projection primitive. These do not usually occur in user code, but are pretty-printed when e.g. `#print`ing a projection diff --git a/stage0/stdlib/Lean/Elab/Binders.c b/stage0/stdlib/Lean/Elab/Binders.c index 7e5f350b38..b8af69ec55 100644 --- a/stage0/stdlib/Lean/Elab/Binders.c +++ b/stage0/stdlib/Lean/Elab/Binders.c @@ -18,6 +18,7 @@ lean_object* l_Lean_Elab_Term_elabLetDeclCore_match__2___rarg(uint8_t, uint8_t, lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandLetEqnsDeclVal_match__1(lean_object*); lean_object* l_Lean_Elab_Term_elabBinder___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabLetDeclCore_match__1(lean_object*); +lean_object* l_Lean_Meta_withLetDecl___at_Lean_Elab_Term_elabLetDeclAux___spec__4(lean_object*); lean_object* l_Lean_Elab_Term_elabBinders(lean_object*); lean_object* l_Lean_Elab_Term_quoteAutoTactic___closed__6; lean_object* l_Lean_Elab_Term_expandWhereDecls___boxed(lean_object*, lean_object*, lean_object*); @@ -29,6 +30,7 @@ extern lean_object* l_Lean_expandExplicitBindersAux_loop___closed__5; extern lean_object* l_Lean_Syntax_strLitToAtom___closed__3; lean_object* l_Lean_registerTraceClass(lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabLetDeclAux___lambda__1___closed__3; +lean_object* l_Lean_Meta_isExprDefEq___at_Lean_Elab_Term_elabLetDeclAux___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabDepArrow___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_matchBinder___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_expandFunBinders_loop_match__2(lean_object*); @@ -53,6 +55,7 @@ lean_object* l___regBuiltin_Lean_Elab_Term_elabDepArrow___closed__1; extern lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___closed__8; lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_mkMatch___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_append___rarg(lean_object*, lean_object*); +lean_object* l_Lean_Meta_forallBoundedTelescope___at_Lean_Elab_Term_elabLetDeclAux___spec__3___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_Meta_withoutPostponingUniverseConstraintsImp___at_Lean_Elab_Term_elabBinders___spec__1___rarg(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Syntax_mkSep(lean_object*, lean_object*); extern lean_object* l_Lean_Elab_throwUnsupportedSyntax___rarg___closed__1; @@ -153,6 +156,7 @@ lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_FunBinders_elabFunB lean_object* l___regBuiltin_Lean_Elab_Term_elabArrow(lean_object*); lean_object* l_Lean_Elab_Term_expandFunBinders_loop___closed__10; lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandBinderModifier___closed__10; +lean_object* l_Lean_Meta_isExprDefEq___at_Lean_Elab_Term_elabLetDeclAux___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_829____closed__1; lean_object* l_Lean_Elab_Term_elabLetDeclAux___lambda__2___closed__1; lean_object* l_Lean_Elab_Term_mkLetRec___boxed(lean_object*, lean_object*, lean_object*); @@ -178,7 +182,6 @@ extern lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_ lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_getBinderIds___spec__1(size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Expr_getOptParamDefault_x3f___closed__2; lean_object* l_Lean_Elab_Term_elabLetDeclAux___lambda__2___closed__2; -lean_object* l_Lean_Meta_forallBoundedTelescope___at_Lean_Elab_Term_elabLetDeclAux___spec__2(lean_object*); uint8_t lean_nat_dec_eq(lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabLetDeclAux___closed__2; extern lean_object* l_Array_forInUnsafe_loop___at___private_Init_NotationExtra_0__Lean_mkHintBody___spec__1___closed__2; @@ -198,7 +201,6 @@ lean_object* l_Lean_Elab_Term_quoteAutoTactic___closed__14; lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_getBinderIds___spec__1___closed__1; lean_object* l_Lean_Elab_Term_expandMatchAltsWhereDecls_loop(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_getLocalInstances___at_Lean_Elab_Term_elabFunBinders___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Meta_withLetDecl___at_Lean_Elab_Term_elabLetDeclAux___spec__3(lean_object*); lean_object* l_Lean_Elab_Term_elabLetDeclAux___closed__1; lean_object* l_Lean_KernelException_toMessageData(lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Elab_Term_elabFun___closed__1; @@ -411,10 +413,11 @@ lean_object* l_Lean_Elab_Term_elabType(lean_object*, lean_object*, lean_object*, lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabLetDeclCore___closed__4; lean_object* l_Lean_Elab_Term_expandFunBinders(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Meta_forallBoundedTelescope___at_Lean_Elab_Term_elabLetDeclAux___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabLetBangDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandBinderModifier___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_withLetDecl___at_Lean_Elab_Term_elabLetDeclAux___spec__4___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_getLocalInstances___at_Lean_Elab_Term_elabFunBinders___spec__1(lean_object*, lean_object*); +lean_object* l_Lean_Meta_forallBoundedTelescope___at_Lean_Elab_Term_elabLetDeclAux___spec__3(lean_object*); lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandMatchAltsIntoMatchAux_match__1(lean_object*); lean_object* l_Lean_Elab_Term_expandFunBinders_loop___closed__2; lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandOptIdent(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -428,7 +431,6 @@ lean_object* l_Lean_Elab_Term_quoteAutoTactic___closed__1; lean_object* l_Lean_mkFreshId___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_FunBinders_elabFunBinderViews___spec__1___rarg(lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_expandFunBinders_loop___closed__5; extern lean_object* l_myMacro____x40_Init_Notation___hyg_11163____closed__7; -lean_object* l_Lean_Meta_withLetDecl___at_Lean_Elab_Term_elabLetDeclAux___spec__3___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_myMacro____x40_Init_Notation___hyg_14258____closed__4; lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_elabBinderViews_loop___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabLetDeclAux___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -18684,7 +18686,15 @@ x_10 = l_Lean_Meta_mkLambdaFVarsImp(x_1, x_2, x_5, x_6, x_7, x_8, x_9); return x_10; } } -lean_object* l_Lean_Meta_forallBoundedTelescope___at_Lean_Elab_Term_elabLetDeclAux___spec__2___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* l_Lean_Meta_isExprDefEq___at_Lean_Elab_Term_elabLetDeclAux___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, lean_object* x_9) { +_start: +{ +lean_object* x_10; +x_10 = l_Lean_Meta_isExprDefEqImp(x_1, x_2, x_5, x_6, x_7, x_8, x_9); +return x_10; +} +} +lean_object* l_Lean_Meta_forallBoundedTelescope___at_Lean_Elab_Term_elabLetDeclAux___spec__3___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) { _start: { lean_object* x_11; lean_object* x_12; @@ -18739,15 +18749,15 @@ return x_20; } } } -lean_object* l_Lean_Meta_forallBoundedTelescope___at_Lean_Elab_Term_elabLetDeclAux___spec__2(lean_object* x_1) { +lean_object* l_Lean_Meta_forallBoundedTelescope___at_Lean_Elab_Term_elabLetDeclAux___spec__3(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_Lean_Meta_forallBoundedTelescope___at_Lean_Elab_Term_elabLetDeclAux___spec__2___rarg), 10, 0); +x_2 = lean_alloc_closure((void*)(l_Lean_Meta_forallBoundedTelescope___at_Lean_Elab_Term_elabLetDeclAux___spec__3___rarg), 10, 0); return x_2; } } -lean_object* l_Lean_Meta_withLetDecl___at_Lean_Elab_Term_elabLetDeclAux___spec__3___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* l_Lean_Meta_withLetDecl___at_Lean_Elab_Term_elabLetDeclAux___spec__4___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) { _start: { lean_object* x_12; lean_object* x_13; @@ -18802,11 +18812,11 @@ return x_21; } } } -lean_object* l_Lean_Meta_withLetDecl___at_Lean_Elab_Term_elabLetDeclAux___spec__3(lean_object* x_1) { +lean_object* l_Lean_Meta_withLetDecl___at_Lean_Elab_Term_elabLetDeclAux___spec__4(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_Lean_Meta_withLetDecl___at_Lean_Elab_Term_elabLetDeclAux___spec__3___rarg), 11, 0); +x_2 = lean_alloc_closure((void*)(l_Lean_Meta_withLetDecl___at_Lean_Elab_Term_elabLetDeclAux___spec__4___rarg), 11, 0); return x_2; } } @@ -19394,7 +19404,7 @@ lean_ctor_set(x_15, 0, x_2); x_16 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabLetDeclAux___lambda__2), 11, 2); lean_closure_set(x_16, 0, x_3); lean_closure_set(x_16, 1, x_4); -x_17 = l_Lean_Meta_forallBoundedTelescope___at_Lean_Elab_Term_elabLetDeclAux___spec__2___rarg(x_5, x_15, x_16, x_7, x_8, x_9, x_10, x_11, x_12, x_13); +x_17 = l_Lean_Meta_forallBoundedTelescope___at_Lean_Elab_Term_elabLetDeclAux___spec__3___rarg(x_5, x_15, x_16, x_7, x_8, x_9, x_10, x_11, x_12, x_13); if (lean_obj_tag(x_17) == 0) { uint8_t x_18; @@ -19719,7 +19729,7 @@ lean_inc(x_10); lean_inc(x_9); lean_inc(x_24); lean_inc(x_23); -x_39 = l_Lean_Meta_withLetDecl___at_Lean_Elab_Term_elabLetDeclAux___spec__3___rarg(x_1, x_23, x_24, x_38, x_9, x_10, x_11, x_12, x_13, x_14, x_26); +x_39 = l_Lean_Meta_withLetDecl___at_Lean_Elab_Term_elabLetDeclAux___spec__4___rarg(x_1, x_23, x_24, x_38, x_9, x_10, x_11, x_12, x_13, x_14, x_26); if (lean_obj_tag(x_39) == 0) { lean_object* x_40; lean_object* x_41; lean_object* x_42; @@ -19862,6 +19872,16 @@ lean_dec(x_3); return x_10; } } +lean_object* l_Lean_Meta_isExprDefEq___at_Lean_Elab_Term_elabLetDeclAux___spec__2___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_Meta_isExprDefEq___at_Lean_Elab_Term_elabLetDeclAux___spec__2(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9); +lean_dec(x_4); +lean_dec(x_3); +return x_10; +} +} lean_object* l_Lean_Elab_Term_elabLetDeclAux___lambda__1___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, lean_object* x_10, lean_object* x_11) { _start: { diff --git a/stage0/stdlib/Lean/Elab/Term.c b/stage0/stdlib/Lean/Elab/Term.c index 59b3e0f81b..c9850fbe0a 100644 --- a/stage0/stdlib/Lean/Elab/Term.c +++ b/stage0/stdlib/Lean/Elab/Term.c @@ -46,6 +46,7 @@ lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_exceptionToSorry(lean_ size_t l_USize_add(size_t, size_t); lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAuxAux___rarg(uint8_t, 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(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_Term_elabDecimalLit___closed__2; lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFnsAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_tryPostponeIfHasMVars_match__1(lean_object*); lean_object* l_Lean_Expr_mvarId_x21(lean_object*); @@ -62,6 +63,8 @@ lean_object* l_ReaderT_read___at_Lean_Elab_Term_instMonadLogTermElabM___spec__1( lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1(lean_object*, lean_object*, uint8_t, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1034____closed__3; lean_object* l_Lean_stringToMessageData(lean_object*); +lean_object* l_Lean_Elab_Term_elabDecimalLit_match__1(lean_object*); +lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_mkFreshTypeMVarFor(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Std_PersistentArray_forM___at_Lean_Elab_Term_instMetaEvalTermElabM___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_MessageData_isNest(lean_object*); lean_object* l_Lean_Elab_Term_resolveName___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -78,8 +81,8 @@ lean_object* l_Std_RBNode_insert___at_Lean_NameSet_insert___spec__1(lean_object* lean_object* l_List_foldl___at_Lean_Elab_addMacroStack___spec__1(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_getLetRecsToLift___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_instMonadMacroAdapterTermElabM___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Elab_Term_elabNumLit___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_withIncRecDepth___rarg___lambda__2___closed__2; +lean_object* l_Lean_Meta_getDecLevel___at_Lean_Elab_Term_elabNumLit___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryLiftAndCoe___closed__9; extern lean_object* l_Lean_nullKind; lean_object* l_Lean_Elab_Term_instAddErrorMessageContextTermElabM(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -121,6 +124,7 @@ lean_object* l_Lean_Elab_Term_isValidAutoBoundImplicitName_match__1___rarg(lean_ lean_object* l_Lean_Format_pretty(lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_liftAttrM(lean_object*); lean_object* l_Lean_Elab_Term_throwErrorIfErrors___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_Term_elabDecimalLit(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_getDeclName_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__2; lean_object* l_Lean_Elab_logTrace___at_Lean_Elab_Term_traceAtCmdPos___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -134,10 +138,11 @@ lean_object* l_Lean_Elab_Term_resolveLocalName(lean_object*, lean_object*, lean_ lean_object* l___regBuiltin_Lean_Elab_Term_elabQuotedName___closed__1; lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryLiftAndCoe_match__2(lean_object*); lean_object* l___regBuiltin_Lean_Elab_Term_elabEnsureTypeOf___closed__1; -lean_object* l_Lean_Elab_Term_elabNumLit___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_elabNumLit___lambda__1(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_elabTypeStx___closed__3; lean_object* l_Lean_Meta_instantiateMVars___at_Lean_Elab_Term_MVarErrorInfo_logError___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_getMVarsAtDeclImp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_mkFreshTypeMVarFor___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_registerCustomErrorIfMVar_match__1___rarg(lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__8; lean_object* l_Lean_Elab_Term_mkTermElabAttributeUnsafe___closed__1; @@ -216,11 +221,10 @@ lean_object* l_Lean_Elab_Term_instMonadLogTermElabM___closed__4; extern lean_object* l_Lean_Meta_mkAppM___rarg___closed__2; lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux_match__1(lean_object*); extern lean_object* l_rawNatLit___closed__2; -lean_object* l_Lean_Meta_isExprDefEq___at_Lean_Elab_Term_elabNumLit___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_getDecLevel___at_Lean_Elab_Term_elabNumLit___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_local_ctx_find_from_user_name(lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_getMVarDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_assignExprMVar___at_Lean_Elab_Term_synthesizeInstMVarCore___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -extern lean_object* l_Lean_Meta_decLevel___rarg___lambda__1___closed__4; lean_object* l_Lean_Meta_mkLambdaFVarsImp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_expr_instantiate1(lean_object*, lean_object*); @@ -234,6 +238,7 @@ lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___lambda__ lean_object* l_Lean_Elab_Term_instMonadLogTermElabM___closed__1; lean_object* l___regBuiltin_Lean_Elab_Term_elabProp(lean_object*); lean_object* lean_string_append(lean_object*, lean_object*); +lean_object* l___regBuiltin_Lean_Elab_Term_elabDecimalLit(lean_object*); lean_object* l_Lean_Meta_withLocalDecl___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImplicitLambda___spec__1___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_mkAppM___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_ensureType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -272,7 +277,6 @@ lean_object* l_Lean_Elab_Term_elabSyntheticHole_match__2(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*); lean_object* l_List_foldlM___at_Lean_Elab_Term_logUnassignedUsingErrorInfos___spec__6___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* l_Lean_Meta_withMVarContext___at_Lean_Elab_Term_logUnassignedUsingErrorInfos___spec__5(lean_object*); -lean_object* l_Lean_Meta_mkFreshTypeMVar___at_Lean_Elab_Term_elabNumLit___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_resolveName___closed__6; lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryCoeSort___closed__1; lean_object* l_Lean_Elab_Term_elabStrLit_match__1___rarg(lean_object*, lean_object*, lean_object*); @@ -295,7 +299,6 @@ lean_object* l_Lean_Elab_Term_getMainModule___rarg(lean_object*, lean_object*); lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_instMetaEvalTermElabM___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_instMonadMacroAdapterTermElabM___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_USize_decLt(size_t, size_t); -lean_object* l_Lean_Meta_mkFreshTypeMVar___at_Lean_Elab_Term_elabNumLit___spec__1(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_FileMap_instInhabitedFileMap___closed__1; lean_object* l_Lean_Meta_instantiateMVarsImp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_instMonadMacroAdapterTermElabM___closed__5; @@ -307,7 +310,6 @@ lean_object* l_Std_PersistentArray_forMAux___at_Lean_Elab_Term_instMetaEvalTermE lean_object* l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__4; lean_object* l_Lean_Elab_Term_elabNumLit_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabTypeWithAutoBoundImplicit___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -extern lean_object* l_Lean_Meta_decLevel___rarg___lambda__1___closed__2; extern lean_object* l_myMacro____x40_Init_Notation___hyg_11163____closed__9; extern lean_object* l_Lean_levelZero; lean_object* l_Lean_Elab_Term_elabStrLit___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -403,9 +405,7 @@ lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_useImplicitLambda_x3f_ lean_object* l_Lean_Elab_Term_getMessageLog(lean_object*); lean_object* l_Std_AssocList_find_x3f___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFns___spec__6(lean_object*, lean_object*); extern lean_object* l_Lean_initFn____x40_Lean_Data_Options___hyg_476____closed__3; -lean_object* l_Lean_Elab_throwIllFormedSyntax___at_Lean_Elab_Term_elabNumLit___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_mkFreshLevelMVar___at___private_Lean_Meta_Basic_0__Lean_Meta_mkFreshExprMVarImpl___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Elab_Term_elabNumLit___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_st_ref_take(lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_instToStringLVal_match__1(lean_object*); lean_object* l_Lean_Elab_Term_MVarErrorInfo_logError___closed__2; @@ -422,6 +422,7 @@ lean_object* l_Lean_Elab_Term_instMonadLogTermElabM; lean_object* l_List_map___at_Lean_Elab_Term_isLetRecAuxMVar___spec__2(lean_object*); lean_object* lean_nat_sub(lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_mkTacticMVar___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_elabDecimalLit___closed__1; lean_object* l_Lean_Elab_Term_mkExplicitBinder___closed__7; lean_object* l_Lean_Elab_Term_mkConst___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_resolveName_match__1(lean_object*); @@ -520,6 +521,7 @@ lean_object* l_Lean_Meta_mkLambdaFVars___at___private_Lean_Elab_Term_0__Lean_Ela lean_object* l___regBuiltin_Lean_Elab_Term_elabByTactic___closed__1; extern lean_object* l_Lean_Expr_instInhabitedExpr___closed__1; lean_object* l_Lean_Elab_Term_instMonadLogTermElabM___closed__5; +lean_object* l_Lean_Elab_Term_elabDecimalLit___closed__3; size_t l_Lean_Name_hash(lean_object*); lean_object* l_Lean_withNestedTraces___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_registerSyntheticMVarWithCurrRef___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -534,6 +536,7 @@ lean_object* l_Lean_Meta_getMVarsAtDecl___at_Lean_Elab_Term_ensureNoUnassignedMV lean_object* l___regBuiltin_Lean_Elab_Term_elabBadCDot___closed__3; lean_object* l_Lean_Meta_withMVarContext___at_Lean_Elab_Term_logUnassignedUsingErrorInfos___spec__5___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_getAutoBoundImplicitLocalOption___boxed(lean_object*); +lean_object* l_Lean_Elab_Term_elabDecimalLit_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* lean_st_mk_ref(lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_mkTypeMismatchError_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Elab_Term_elabCharLit(lean_object*); @@ -552,6 +555,7 @@ extern lean_object* l_Lean_Parser_Tactic_letrec___closed__1; lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux_match__2(lean_object*); lean_object* l_Lean_Elab_addMacroStack___at_Lean_Elab_Term_instAddErrorMessageContextTermElabM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_logException___at___private_Lean_Elab_Term_0__Lean_Elab_Term_exceptionToSorry___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_mkFreshTypeMVarFor_match__1(lean_object*); lean_object* l_Lean_Elab_Term_mkTermElabAttributeUnsafe___closed__6; lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_dropTermParens_match__1___rarg(lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabSyntheticHole_match__2___rarg(lean_object*, lean_object*, lean_object*); @@ -586,6 +590,7 @@ lean_object* l_Lean_Elab_Term_getMainModule(lean_object*, lean_object*, lean_obj extern lean_object* l_Lean_Meta_throwTypeExcepted___rarg___closed__2; lean_object* l_Lean_Elab_Term_isMonadApp_match__1(lean_object*); lean_object* l_Lean_Elab_Term_mkTermElabAttribute(lean_object*); +lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_mkFreshTypeMVarFor_match__1___rarg(lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_numLitKind___closed__2; lean_object* l_Std_AssocList_find_x3f___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFns___spec__6___boxed(lean_object*, lean_object*); lean_object* l_Lean_printTraces___at_Lean_Core_instMetaEvalCoreM___spec__1(lean_object*, lean_object*, lean_object*); @@ -625,7 +630,6 @@ lean_object* l___private_Lean_Meta_InferType_0__Lean_Meta_getLevelImp(lean_objec lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryCoeSort___closed__3; lean_object* l_Lean_Elab_Term_elabSyntheticHole___closed__1; lean_object* l_Lean_Elab_Term_registerMVarErrorHoleInfo___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7541____closed__1; lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryCoe___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_addAutoBoundImplicits___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_withLCtx___at_Lean_Elab_Term_elabSyntheticHole___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -640,7 +644,6 @@ lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___lambda__1___boxed(lean_ob lean_object* l_Lean_Elab_Term_elabEnsureExpectedType(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_0__Lean_Elab_Term_isTypeApp_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Elab_Term_elabNumLit_match__2(lean_object*); lean_object* l_Lean_Elab_Term_levelMVarToParam_x27_match__1___rarg(lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabQuotedName_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabRawNatLit_match__1___rarg(lean_object*, lean_object*, lean_object*); @@ -716,11 +719,13 @@ lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_instMetaEvalTermElabM uint8_t l_List_elem___at_Lean_NameHashSet_insert___spec__2(lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_withoutPostponing___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_savingMCtx(lean_object*); +lean_object* l_Lean_Elab_throwIllFormedSyntax___at_Lean_Elab_Term_elabNumLit___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabHole(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_resolveName_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_isLetRecAuxMVar___closed__2; lean_object* l___regBuiltin_Lean_Elab_Term_elabCharLit___closed__1; extern lean_object* l_Lean_Syntax_mkApp___closed__1; +lean_object* l_Lean_Syntax_isDecimalLit_x3f(lean_object*); lean_object* l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__4; lean_object* l_Lean_Elab_Term_elabEnsureExpectedType_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFnsAux_match__2(lean_object*); @@ -729,7 +734,6 @@ lean_object* l_Std_PersistentArray_push___rarg(lean_object*, lean_object*); lean_object* l_Lean_Elab_isAutoBoundImplicitLocalException_x3f(lean_object*); lean_object* l_Lean_Elab_Term_mkTermElabAttributeUnsafe___closed__4; lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_mkSomeContext; -lean_object* l_Lean_Meta_decLevel___at_Lean_Elab_Term_elabNumLit___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_mkFreshBinderName(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_isLocalIdent_x3f_match__2(lean_object*); lean_object* l_Std_PersistentHashMap_findAux___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFns___spec__3(lean_object*, size_t, lean_object*); @@ -860,6 +864,8 @@ lean_object* l_Lean_Elab_Term_elabSort(lean_object*, lean_object*, lean_object*, uint8_t l_Lean_Elab_Term_levelMVarToParam___lambda__1(lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryLiftAndCoe_match__2___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabSyntheticHole___closed__2; +lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7628____closed__1; +lean_object* l_Lean_mkApp4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore(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___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore_match__2(lean_object*); lean_object* l_Lean_Elab_Term_mkTypeMismatchError___closed__2; @@ -870,6 +876,7 @@ lean_object* l_Lean_Elab_logAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_e lean_object* l_Lean_Elab_Term_getMessageLog___boxed(lean_object*); lean_object* l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__1; lean_object* l_Lean_Elab_Term_isLocalIdent_x3f_match__1(lean_object*); +lean_object* l_Lean_Elab_Term_elabDecimalLit___closed__4; lean_object* l_Std_PersistentArray_forIn___at_Lean_Elab_Term_addAutoBoundImplicits___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -913,7 +920,6 @@ extern lean_object* l_Lean_mkOptionalNode___closed__1; lean_object* l_Lean_Syntax_isNameLit_x3f(lean_object*); lean_object* l_Lean_Elab_Term_liftCoreM(lean_object*); lean_object* l_Lean_Elab_Term_getMainModule___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Meta_isExprDefEq___at_Lean_Elab_Term_elabNumLit___spec__3___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_0__Lean_Elab_Term_isMonad_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_isMonad_x3f___closed__1; lean_object* l_Lean_Elab_throwIllFormedSyntax___at_Lean_Elab_Term_elabStrLit___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -944,6 +950,7 @@ lean_object* l___private_Lean_MonadEnv_0__Lean_mkAuxNameAux(lean_object*, lean_o lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__1(lean_object*); lean_object* l_Lean_Meta_whnf___rarg___lambda__2(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*); +lean_object* l_Lean_Elab_throwIllFormedSyntax___at_Lean_Elab_Term_elabNumLit___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___lambda__4___closed__5; lean_object* l_Lean_Elab_Term_mkExplicitBinder___closed__4; lean_object* l_Lean_Elab_Term_withoutErrToSorry___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -953,7 +960,6 @@ lean_object* l_Lean_Elab_Term_TermElabM_toIO___rarg(lean_object*, lean_object*, lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_instMetaEvalTermElabM___spec__11(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Std_PersistentArray_forInAux___at_Lean_Elab_Term_addAutoBoundImplicits___spec__4___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_applyResult_match__1(lean_object*); -lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_decLevelImp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabByTactic___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_resolveName___closed__2; lean_object* l_Lean_Elab_Term_elabSyntheticHole(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -962,11 +968,9 @@ lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_mkTacticMVar(lean_obje lean_object* l_Lean_Meta_inferType___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_getLevelNames___boxed(lean_object*); lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux_match__3(lean_object*); -lean_object* l_Lean_Elab_Term_elabNumLit_match__2___rarg(lean_object*, lean_object*, lean_object*); lean_object* lean_string_length(lean_object*); lean_object* l_Lean_Elab_Term_setMessageLog___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_indentD(lean_object*); -lean_object* l_Lean_Meta_decLevel___at_Lean_Elab_Term_elabNumLit___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_getMVars___at_Lean_Elab_Term_logUnassignedUsingErrorInfos___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Elab_unsupportedSyntaxExceptionId; lean_object* l_Lean_Elab_Term_logUnassignedUsingErrorInfos_match__1___rarg(lean_object*, lean_object*); @@ -988,7 +992,7 @@ lean_object* l_IO_println___at_Lean_instEval___spec__1(lean_object*, lean_object lean_object* l_Lean_Elab_Term_logUnassignedUsingErrorInfos_match__2___rarg(lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_throwErrorIfErrors(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_NameSet_contains(lean_object*, lean_object*); -lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7541_(lean_object*); +lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7628_(lean_object*); lean_object* l_Lean_Elab_Term_elabByTactic_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_addAutoBoundImplicits(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_withAutoBoundImplicitLocal___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -1022,6 +1026,7 @@ lean_object* l_Lean_Elab_Term_getFVarLocalDecl_x21_match__1(lean_object*); lean_object* l_Lean_Elab_Term_elabTypeWithAutoBoundImplicit_loop_match__1(lean_object*); extern lean_object* l_Lean_Elab_mkMacroAttributeUnsafe___closed__2; lean_object* l_Lean_Elab_Term_resolveName___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_decimalLitKind___closed__2; lean_object* l_Lean_Elab_Term_MVarErrorInfo_logError___closed__11; lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withLocalContextImp___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_MetavarContext_getDecl(lean_object*, lean_object*); @@ -1047,6 +1052,7 @@ lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_instMetaEvalTermElabM lean_object* l_Lean_Elab_Term_isLetRecAuxMVar___closed__5; lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryCoe(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_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_instMetaEvalTermElabM___spec__12___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_Term_elabDecimalLit___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_instMetaEvalTermElabM___spec__10___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_tryPostponeIfHasMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1034____closed__4; @@ -1109,7 +1115,6 @@ lean_object* l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___lambda__1___boxed(l lean_object* l_Lean_getAttributeImpl(lean_object*, lean_object*); lean_object* l_Lean_Meta_mkAppOptM___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Meta_throwLetTypeMismatchMessage___rarg___closed__8; -lean_object* l_Lean_Elab_throwIllFormedSyntax___at_Lean_Elab_Term_elabNumLit___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_saveAllState___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_isExprDefEq___at_Lean_Elab_Term_synthesizeInstMVarCore___spec__3___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_MVarErrorInfo_logError___closed__8; @@ -1131,6 +1136,7 @@ lean_object* l_Lean_Elab_Term_liftMetaM___rarg(lean_object*, lean_object*, lean_ lean_object* l_Lean_Meta_mkFreshTypeMVar___at___private_Lean_Elab_Term_0__Lean_Elab_Term_exceptionToSorry___spec__5(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_tryCoeThunk_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_getMainModule___rarg___boxed(lean_object*, lean_object*); +lean_object* l_Lean_Elab_Term_elabDecimalLit___closed__1; lean_object* l_Lean_Elab_Term_elabRawNatLit___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_isMonadApp_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryLiftAndCoe___closed__7; @@ -33059,6 +33065,143 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); return x_5; } } +lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_mkFreshTypeMVarFor_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +if (lean_obj_tag(x_1) == 0) +{ +lean_object* x_4; +lean_dec(x_2); +x_4 = lean_apply_1(x_3, x_1); +return x_4; +} +else +{ +lean_object* x_5; lean_object* x_6; +lean_dec(x_3); +x_5 = lean_ctor_get(x_1, 0); +lean_inc(x_5); +lean_dec(x_1); +x_6 = lean_apply_1(x_2, x_5); +return x_6; +} +} +} +lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_mkFreshTypeMVarFor_match__1(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Lean_Elab_Term_0__Lean_Elab_Term_mkFreshTypeMVarFor_match__1___rarg), 3, 0); +return x_2; +} +} +lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_mkFreshTypeMVarFor(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: +{ +uint8_t x_9; lean_object* x_10; lean_object* x_11; +x_9 = 1; +x_10 = lean_box(0); +lean_inc(x_4); +x_11 = l_Lean_Meta_mkFreshTypeMVar___at___private_Lean_Elab_Term_0__Lean_Elab_Term_exceptionToSorry___spec__5(x_9, x_10, x_2, x_3, x_4, x_5, x_6, x_7, x_8); +if (lean_obj_tag(x_1) == 0) +{ +uint8_t x_12; +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +x_12 = !lean_is_exclusive(x_11); +if (x_12 == 0) +{ +return x_11; +} +else +{ +lean_object* x_13; lean_object* x_14; lean_object* x_15; +x_13 = lean_ctor_get(x_11, 0); +x_14 = lean_ctor_get(x_11, 1); +lean_inc(x_14); +lean_inc(x_13); +lean_dec(x_11); +x_15 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_15, 0, x_13); +lean_ctor_set(x_15, 1, x_14); +return x_15; +} +} +else +{ +lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; +x_16 = lean_ctor_get(x_11, 0); +lean_inc(x_16); +x_17 = lean_ctor_get(x_11, 1); +lean_inc(x_17); +lean_dec(x_11); +x_18 = lean_ctor_get(x_1, 0); +lean_inc(x_18); +lean_dec(x_1); +lean_inc(x_16); +x_19 = l_Lean_Meta_isExprDefEqImp(x_18, x_16, x_4, x_5, x_6, x_7, x_17); +if (lean_obj_tag(x_19) == 0) +{ +uint8_t x_20; +x_20 = !lean_is_exclusive(x_19); +if (x_20 == 0) +{ +lean_object* x_21; +x_21 = lean_ctor_get(x_19, 0); +lean_dec(x_21); +lean_ctor_set(x_19, 0, x_16); +return x_19; +} +else +{ +lean_object* x_22; lean_object* x_23; +x_22 = lean_ctor_get(x_19, 1); +lean_inc(x_22); +lean_dec(x_19); +x_23 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_23, 0, x_16); +lean_ctor_set(x_23, 1, x_22); +return x_23; +} +} +else +{ +uint8_t x_24; +lean_dec(x_16); +x_24 = !lean_is_exclusive(x_19); +if (x_24 == 0) +{ +return x_19; +} +else +{ +lean_object* x_25; lean_object* x_26; lean_object* x_27; +x_25 = lean_ctor_get(x_19, 0); +x_26 = lean_ctor_get(x_19, 1); +lean_inc(x_26); +lean_inc(x_25); +lean_dec(x_19); +x_27 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_27, 0, x_25); +lean_ctor_set(x_27, 1, x_26); +return x_27; +} +} +} +} +} +lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_mkFreshTypeMVarFor___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) { +_start: +{ +lean_object* x_9; +x_9 = l___private_Lean_Elab_Term_0__Lean_Elab_Term_mkFreshTypeMVarFor(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8); +lean_dec(x_3); +lean_dec(x_2); +return x_9; +} +} lean_object* l_Lean_Elab_Term_elabNumLit_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { @@ -33090,149 +33233,59 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabNumLit_match__1___rarg), 3 return x_2; } } -lean_object* l_Lean_Elab_Term_elabNumLit_match__2___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { -_start: -{ -if (lean_obj_tag(x_1) == 0) -{ -lean_object* x_4; -lean_dec(x_2); -x_4 = lean_apply_1(x_3, x_1); -return x_4; -} -else -{ -lean_object* x_5; lean_object* x_6; -lean_dec(x_3); -x_5 = lean_ctor_get(x_1, 0); -lean_inc(x_5); -lean_dec(x_1); -x_6 = lean_apply_1(x_2, x_5); -return x_6; -} -} -} -lean_object* l_Lean_Elab_Term_elabNumLit_match__2(lean_object* x_1) { -_start: -{ -lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabNumLit_match__2___rarg), 3, 0); -return x_2; -} -} -lean_object* l_Lean_Meta_mkFreshTypeMVar___at_Lean_Elab_Term_elabNumLit___spec__1(uint8_t 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; lean_object* x_13; lean_object* x_14; lean_object* x_15; -x_10 = l_Lean_Meta_mkFreshLevelMVar___at___private_Lean_Meta_Basic_0__Lean_Meta_mkFreshExprMVarImpl___spec__1___rarg(x_6, x_7, x_8, x_9); -x_11 = lean_ctor_get(x_10, 0); -lean_inc(x_11); -x_12 = lean_ctor_get(x_10, 1); -lean_inc(x_12); -lean_dec(x_10); -x_13 = l_Lean_mkSort(x_11); -x_14 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_14, 0, x_13); -x_15 = l___private_Lean_Meta_Basic_0__Lean_Meta_mkFreshExprMVarImpl(x_14, x_1, x_2, x_5, x_6, x_7, x_8, x_12); -return x_15; -} -} -lean_object* l_Lean_Meta_decLevel___at_Lean_Elab_Term_elabNumLit___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) { +lean_object* l_Lean_Meta_getDecLevel___at_Lean_Elab_Term_elabNumLit___spec__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) { _start: { lean_object* x_9; -lean_inc(x_1); -x_9 = l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_decLevelImp(x_1, x_4, x_5, x_6, x_7, x_8); +lean_inc(x_7); +lean_inc(x_6); +lean_inc(x_5); +lean_inc(x_4); +x_9 = l___private_Lean_Meta_InferType_0__Lean_Meta_getLevelImp(x_1, x_4, x_5, x_6, x_7, x_8); if (lean_obj_tag(x_9) == 0) { -lean_object* x_10; +lean_object* x_10; lean_object* x_11; lean_object* x_12; x_10 = lean_ctor_get(x_9, 0); lean_inc(x_10); -if (lean_obj_tag(x_10) == 0) -{ -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; x_11 = lean_ctor_get(x_9, 1); lean_inc(x_11); lean_dec(x_9); -x_12 = lean_alloc_ctor(3, 1, 0); -lean_ctor_set(x_12, 0, x_1); -x_13 = l_Lean_Meta_decLevel___rarg___lambda__1___closed__2; -x_14 = lean_alloc_ctor(10, 2, 0); -lean_ctor_set(x_14, 0, x_13); -lean_ctor_set(x_14, 1, x_12); -x_15 = l_Lean_Meta_decLevel___rarg___lambda__1___closed__4; -x_16 = lean_alloc_ctor(10, 2, 0); +x_12 = l_Lean_Meta_decLevel___at_Lean_Meta_getDecLevel___spec__1(x_10, x_4, x_5, x_6, x_7, x_11); +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +return x_12; +} +else +{ +uint8_t x_13; +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +x_13 = !lean_is_exclusive(x_9); +if (x_13 == 0) +{ +return x_9; +} +else +{ +lean_object* x_14; lean_object* x_15; lean_object* x_16; +x_14 = lean_ctor_get(x_9, 0); +x_15 = lean_ctor_get(x_9, 1); +lean_inc(x_15); +lean_inc(x_14); +lean_dec(x_9); +x_16 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_16, 0, x_14); lean_ctor_set(x_16, 1, x_15); -x_17 = l_Lean_throwError___at_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1019____spec__1___rarg(x_16, x_4, x_5, x_6, x_7, x_11); -return x_17; -} -else -{ -uint8_t x_18; -lean_dec(x_1); -x_18 = !lean_is_exclusive(x_9); -if (x_18 == 0) -{ -lean_object* x_19; lean_object* x_20; -x_19 = lean_ctor_get(x_9, 0); -lean_dec(x_19); -x_20 = lean_ctor_get(x_10, 0); -lean_inc(x_20); -lean_dec(x_10); -lean_ctor_set(x_9, 0, x_20); -return x_9; -} -else -{ -lean_object* x_21; lean_object* x_22; lean_object* x_23; -x_21 = lean_ctor_get(x_9, 1); -lean_inc(x_21); -lean_dec(x_9); -x_22 = lean_ctor_get(x_10, 0); -lean_inc(x_22); -lean_dec(x_10); -x_23 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_23, 0, x_22); -lean_ctor_set(x_23, 1, x_21); -return x_23; -} -} -} -else -{ -uint8_t x_24; -lean_dec(x_1); -x_24 = !lean_is_exclusive(x_9); -if (x_24 == 0) -{ -return x_9; -} -else -{ -lean_object* x_25; lean_object* x_26; lean_object* x_27; -x_25 = lean_ctor_get(x_9, 0); -x_26 = lean_ctor_get(x_9, 1); -lean_inc(x_26); -lean_inc(x_25); -lean_dec(x_9); -x_27 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_27, 0, x_25); -lean_ctor_set(x_27, 1, x_26); -return x_27; +return x_16; } } } } -lean_object* l_Lean_Meta_isExprDefEq___at_Lean_Elab_Term_elabNumLit___spec__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) { -_start: -{ -lean_object* x_10; -x_10 = l_Lean_Meta_isExprDefEqImp(x_1, x_2, x_5, x_6, x_7, x_8, x_9); -return x_10; -} -} -lean_object* l_Lean_Elab_throwIllFormedSyntax___at_Lean_Elab_Term_elabNumLit___spec__4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) { +lean_object* l_Lean_Elab_throwIllFormedSyntax___at_Lean_Elab_Term_elabNumLit___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) { _start: { lean_object* x_8; lean_object* x_9; @@ -33241,216 +33294,110 @@ x_9 = l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1___rarg( return x_9; } } -lean_object* l_Lean_Elab_Term_elabNumLit___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, lean_object* x_10) { +lean_object* l_Lean_Elab_Term_elabNumLit___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: { -lean_object* x_11; -lean_inc(x_9); +lean_object* x_10; lean_inc(x_8); lean_inc(x_7); lean_inc(x_6); -lean_inc(x_1); -x_11 = l___private_Lean_Meta_InferType_0__Lean_Meta_getLevelImp(x_1, x_6, x_7, x_8, x_9, x_10); -if (lean_obj_tag(x_11) == 0) +lean_inc(x_5); +x_10 = l___private_Lean_Elab_Term_0__Lean_Elab_Term_mkFreshTypeMVarFor(x_1, x_3, x_4, x_5, x_6, x_7, x_8, x_9); +if (lean_obj_tag(x_10) == 0) { -lean_object* x_12; lean_object* x_13; lean_object* x_14; -x_12 = lean_ctor_get(x_11, 0); +lean_object* x_11; lean_object* x_12; lean_object* x_13; +x_11 = lean_ctor_get(x_10, 0); +lean_inc(x_11); +x_12 = lean_ctor_get(x_10, 1); lean_inc(x_12); -x_13 = lean_ctor_get(x_11, 1); -lean_inc(x_13); -lean_dec(x_11); -x_14 = l_Lean_Meta_decLevel___at_Lean_Elab_Term_elabNumLit___spec__2(x_12, x_4, x_5, x_6, x_7, x_8, x_9, x_13); -if (lean_obj_tag(x_14) == 0) -{ -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; -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 = lean_box(0); -x_18 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_18, 0, x_15); -lean_ctor_set(x_18, 1, x_17); -x_19 = l_Lean_Meta_evalNat_visit___closed__2; -lean_inc(x_18); -x_20 = l_Lean_mkConst(x_19, x_18); -x_21 = l_Lean_mkNatLit(x_2); -lean_inc(x_21); -lean_inc(x_1); -x_22 = l_Lean_mkAppB(x_20, x_1, x_21); -x_23 = l_Lean_Elab_Term_mkInstMVar(x_22, x_4, x_5, x_6, x_7, x_8, x_9, x_16); -if (lean_obj_tag(x_23) == 0) -{ -uint8_t x_24; -x_24 = !lean_is_exclusive(x_23); -if (x_24 == 0) -{ -lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; -x_25 = lean_ctor_get(x_23, 0); -x_26 = l_Lean_Meta_evalNat_visit___closed__3; -x_27 = l_Lean_mkConst(x_26, x_18); -x_28 = l_Lean_mkApp3(x_27, x_1, x_21, x_25); -lean_ctor_set(x_23, 0, x_28); -return x_23; -} -else -{ -lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; -x_29 = lean_ctor_get(x_23, 0); -x_30 = lean_ctor_get(x_23, 1); -lean_inc(x_30); -lean_inc(x_29); -lean_dec(x_23); -x_31 = l_Lean_Meta_evalNat_visit___closed__3; -x_32 = l_Lean_mkConst(x_31, x_18); -x_33 = l_Lean_mkApp3(x_32, x_1, x_21, x_29); -x_34 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_34, 0, x_33); -lean_ctor_set(x_34, 1, x_30); -return x_34; -} -} -else -{ -uint8_t x_35; -lean_dec(x_21); -lean_dec(x_18); -lean_dec(x_1); -x_35 = !lean_is_exclusive(x_23); -if (x_35 == 0) -{ -return x_23; -} -else -{ -lean_object* x_36; lean_object* x_37; lean_object* x_38; -x_36 = lean_ctor_get(x_23, 0); -x_37 = lean_ctor_get(x_23, 1); -lean_inc(x_37); -lean_inc(x_36); -lean_dec(x_23); -x_38 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_38, 0, x_36); -lean_ctor_set(x_38, 1, x_37); -return x_38; -} -} -} -else -{ -uint8_t x_39; -lean_dec(x_9); -lean_dec(x_8); -lean_dec(x_7); -lean_dec(x_6); -lean_dec(x_5); -lean_dec(x_4); -lean_dec(x_2); -lean_dec(x_1); -x_39 = !lean_is_exclusive(x_14); -if (x_39 == 0) -{ -return x_14; -} -else -{ -lean_object* x_40; lean_object* x_41; lean_object* x_42; -x_40 = lean_ctor_get(x_14, 0); -x_41 = lean_ctor_get(x_14, 1); -lean_inc(x_41); -lean_inc(x_40); -lean_dec(x_14); -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_9); -lean_dec(x_8); -lean_dec(x_7); -lean_dec(x_6); -lean_dec(x_5); -lean_dec(x_4); -lean_dec(x_2); -lean_dec(x_1); -x_43 = !lean_is_exclusive(x_11); -if (x_43 == 0) -{ -return x_11; -} -else -{ -lean_object* x_44; lean_object* x_45; lean_object* x_46; -x_44 = lean_ctor_get(x_11, 0); -x_45 = lean_ctor_get(x_11, 1); -lean_inc(x_45); -lean_inc(x_44); -lean_dec(x_11); -x_46 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_46, 0, x_44); -lean_ctor_set(x_46, 1, x_45); -return x_46; -} -} -} -} -lean_object* l_Lean_Elab_Term_elabNumLit___lambda__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, lean_object* x_9) { -_start: -{ -uint8_t x_10; lean_object* x_11; lean_object* x_12; -x_10 = 1; -x_11 = lean_box(0); -lean_inc(x_5); -x_12 = l_Lean_Meta_mkFreshTypeMVar___at_Lean_Elab_Term_elabNumLit___spec__1(x_10, x_11, x_3, x_4, x_5, x_6, x_7, x_8, x_9); -if (lean_obj_tag(x_1) == 0) -{ -lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; -x_13 = lean_ctor_get(x_12, 0); -lean_inc(x_13); -x_14 = lean_ctor_get(x_12, 1); -lean_inc(x_14); -lean_dec(x_12); -x_15 = lean_box(0); -x_16 = l_Lean_Elab_Term_elabNumLit___lambda__1(x_13, x_2, x_15, x_3, x_4, x_5, x_6, x_7, x_8, x_14); -return x_16; -} -else -{ -lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; -x_17 = lean_ctor_get(x_12, 0); -lean_inc(x_17); -x_18 = lean_ctor_get(x_12, 1); -lean_inc(x_18); -lean_dec(x_12); -x_19 = lean_ctor_get(x_1, 0); -lean_inc(x_19); -lean_dec(x_1); +lean_dec(x_10); lean_inc(x_8); lean_inc(x_7); lean_inc(x_6); lean_inc(x_5); -lean_inc(x_17); -x_20 = l_Lean_Meta_isExprDefEqImp(x_19, x_17, x_5, x_6, x_7, x_8, x_18); -if (lean_obj_tag(x_20) == 0) +lean_inc(x_11); +x_13 = l_Lean_Meta_getDecLevel___at_Lean_Elab_Term_elabNumLit___spec__1(x_11, x_3, x_4, x_5, x_6, x_7, x_8, x_12); +if (lean_obj_tag(x_13) == 0) { -lean_object* x_21; lean_object* x_22; lean_object* x_23; -x_21 = lean_ctor_get(x_20, 1); -lean_inc(x_21); -lean_dec(x_20); -x_22 = lean_box(0); -x_23 = l_Lean_Elab_Term_elabNumLit___lambda__1(x_17, x_2, x_22, x_3, x_4, x_5, x_6, x_7, x_8, x_21); -return x_23; +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; +x_14 = lean_ctor_get(x_13, 0); +lean_inc(x_14); +x_15 = lean_ctor_get(x_13, 1); +lean_inc(x_15); +lean_dec(x_13); +x_16 = lean_box(0); +x_17 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_17, 0, x_14); +lean_ctor_set(x_17, 1, x_16); +x_18 = l_Lean_Meta_evalNat_visit___closed__2; +lean_inc(x_17); +x_19 = l_Lean_mkConst(x_18, x_17); +x_20 = l_Lean_mkNatLit(x_2); +lean_inc(x_20); +lean_inc(x_11); +x_21 = l_Lean_mkAppB(x_19, x_11, x_20); +x_22 = l_Lean_Elab_Term_mkInstMVar(x_21, x_3, x_4, x_5, x_6, x_7, x_8, x_15); +if (lean_obj_tag(x_22) == 0) +{ +uint8_t x_23; +x_23 = !lean_is_exclusive(x_22); +if (x_23 == 0) +{ +lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; +x_24 = lean_ctor_get(x_22, 0); +x_25 = l_Lean_Meta_evalNat_visit___closed__3; +x_26 = l_Lean_mkConst(x_25, x_17); +x_27 = l_Lean_mkApp3(x_26, x_11, x_20, x_24); +lean_ctor_set(x_22, 0, x_27); +return x_22; } else { -uint8_t x_24; +lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; +x_28 = lean_ctor_get(x_22, 0); +x_29 = lean_ctor_get(x_22, 1); +lean_inc(x_29); +lean_inc(x_28); +lean_dec(x_22); +x_30 = l_Lean_Meta_evalNat_visit___closed__3; +x_31 = l_Lean_mkConst(x_30, x_17); +x_32 = l_Lean_mkApp3(x_31, x_11, x_20, x_28); +x_33 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_33, 0, x_32); +lean_ctor_set(x_33, 1, x_29); +return x_33; +} +} +else +{ +uint8_t x_34; +lean_dec(x_20); lean_dec(x_17); +lean_dec(x_11); +x_34 = !lean_is_exclusive(x_22); +if (x_34 == 0) +{ +return x_22; +} +else +{ +lean_object* x_35; lean_object* x_36; lean_object* x_37; +x_35 = lean_ctor_get(x_22, 0); +x_36 = lean_ctor_get(x_22, 1); +lean_inc(x_36); +lean_inc(x_35); +lean_dec(x_22); +x_37 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_37, 0, x_35); +lean_ctor_set(x_37, 1, x_36); +return x_37; +} +} +} +else +{ +uint8_t x_38; +lean_dec(x_11); lean_dec(x_8); lean_dec(x_7); lean_dec(x_6); @@ -33458,26 +33405,55 @@ lean_dec(x_5); lean_dec(x_4); lean_dec(x_3); lean_dec(x_2); -x_24 = !lean_is_exclusive(x_20); -if (x_24 == 0) +x_38 = !lean_is_exclusive(x_13); +if (x_38 == 0) { -return x_20; +return x_13; } else { -lean_object* x_25; lean_object* x_26; lean_object* x_27; -x_25 = lean_ctor_get(x_20, 0); -x_26 = lean_ctor_get(x_20, 1); -lean_inc(x_26); -lean_inc(x_25); -lean_dec(x_20); -x_27 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_27, 0, x_25); -lean_ctor_set(x_27, 1, x_26); -return x_27; +lean_object* x_39; lean_object* x_40; lean_object* x_41; +x_39 = lean_ctor_get(x_13, 0); +x_40 = lean_ctor_get(x_13, 1); +lean_inc(x_40); +lean_inc(x_39); +lean_dec(x_13); +x_41 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_41, 0, x_39); +lean_ctor_set(x_41, 1, x_40); +return x_41; } } } +else +{ +uint8_t x_42; +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_42 = !lean_is_exclusive(x_10); +if (x_42 == 0) +{ +return x_10; +} +else +{ +lean_object* x_43; lean_object* x_44; lean_object* x_45; +x_43 = lean_ctor_get(x_10, 0); +x_44 = lean_ctor_get(x_10, 1); +lean_inc(x_44); +lean_inc(x_43); +lean_dec(x_10); +x_45 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_45, 0, x_43); +lean_ctor_set(x_45, 1, x_44); +return x_45; +} +} } } lean_object* l_Lean_Elab_Term_elabNumLit(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) { @@ -33490,7 +33466,7 @@ if (lean_obj_tag(x_11) == 0) { lean_object* x_12; uint8_t x_13; lean_dec(x_2); -x_12 = l_Lean_Elab_throwIllFormedSyntax___at_Lean_Elab_Term_elabNumLit___spec__4(x_3, x_4, x_5, x_6, x_7, x_8, x_9); +x_12 = l_Lean_Elab_throwIllFormedSyntax___at_Lean_Elab_Term_elabNumLit___spec__2(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); @@ -33521,55 +33497,26 @@ lean_object* x_17; lean_object* x_18; x_17 = lean_ctor_get(x_11, 0); lean_inc(x_17); lean_dec(x_11); -x_18 = l_Lean_Elab_Term_elabNumLit___lambda__2(x_2, x_17, x_3, x_4, x_5, x_6, x_7, x_8, x_9); +x_18 = l_Lean_Elab_Term_elabNumLit___lambda__1(x_2, x_17, x_3, x_4, x_5, x_6, x_7, x_8, x_9); return x_18; } } } -lean_object* l_Lean_Meta_mkFreshTypeMVar___at_Lean_Elab_Term_elabNumLit___spec__1___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: -{ -uint8_t x_10; lean_object* x_11; -x_10 = lean_unbox(x_1); -lean_dec(x_1); -x_11 = l_Lean_Meta_mkFreshTypeMVar___at_Lean_Elab_Term_elabNumLit___spec__1(x_10, x_2, 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_4); -lean_dec(x_3); -return x_11; -} -} -lean_object* l_Lean_Meta_decLevel___at_Lean_Elab_Term_elabNumLit___spec__2___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* l_Lean_Meta_getDecLevel___at_Lean_Elab_Term_elabNumLit___spec__1___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) { _start: { lean_object* x_9; -x_9 = l_Lean_Meta_decLevel___at_Lean_Elab_Term_elabNumLit___spec__2(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8); -lean_dec(x_7); -lean_dec(x_6); -lean_dec(x_5); -lean_dec(x_4); +x_9 = l_Lean_Meta_getDecLevel___at_Lean_Elab_Term_elabNumLit___spec__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8); lean_dec(x_3); lean_dec(x_2); return x_9; } } -lean_object* l_Lean_Meta_isExprDefEq___at_Lean_Elab_Term_elabNumLit___spec__3___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_Meta_isExprDefEq___at_Lean_Elab_Term_elabNumLit___spec__3(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9); -lean_dec(x_4); -lean_dec(x_3); -return x_10; -} -} -lean_object* l_Lean_Elab_throwIllFormedSyntax___at_Lean_Elab_Term_elabNumLit___spec__4___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* l_Lean_Elab_throwIllFormedSyntax___at_Lean_Elab_Term_elabNumLit___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) { _start: { lean_object* x_8; -x_8 = l_Lean_Elab_throwIllFormedSyntax___at_Lean_Elab_Term_elabNumLit___spec__4(x_1, x_2, x_3, x_4, x_5, x_6, x_7); +x_8 = l_Lean_Elab_throwIllFormedSyntax___at_Lean_Elab_Term_elabNumLit___spec__2(x_1, x_2, x_3, x_4, x_5, x_6, x_7); lean_dec(x_6); lean_dec(x_5); lean_dec(x_4); @@ -33578,15 +33525,6 @@ lean_dec(x_2); return x_8; } } -lean_object* l_Lean_Elab_Term_elabNumLit___lambda__1___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, lean_object* x_10) { -_start: -{ -lean_object* x_11; -x_11 = l_Lean_Elab_Term_elabNumLit___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10); -lean_dec(x_3); -return x_11; -} -} lean_object* l_Lean_Elab_Term_elabNumLit___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: { @@ -33710,6 +33648,298 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); return x_5; } } +lean_object* l_Lean_Elab_Term_elabDecimalLit_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +if (lean_obj_tag(x_1) == 0) +{ +lean_object* x_4; lean_object* x_5; +lean_dec(x_3); +x_4 = lean_box(0); +x_5 = lean_apply_1(x_2, x_4); +return x_5; +} +else +{ +lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; +lean_dec(x_2); +x_6 = lean_ctor_get(x_1, 0); +lean_inc(x_6); +lean_dec(x_1); +x_7 = lean_ctor_get(x_6, 0); +lean_inc(x_7); +x_8 = lean_ctor_get(x_6, 1); +lean_inc(x_8); +lean_dec(x_6); +x_9 = lean_apply_2(x_3, x_7, x_8); +return x_9; +} +} +} +lean_object* l_Lean_Elab_Term_elabDecimalLit_match__1(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabDecimalLit_match__1___rarg), 3, 0); +return x_2; +} +} +static lean_object* _init_l_Lean_Elab_Term_elabDecimalLit___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("OfDecimal"); +return x_1; +} +} +static lean_object* _init_l_Lean_Elab_Term_elabDecimalLit___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_Lean_Elab_Term_elabDecimalLit___closed__1; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +static lean_object* _init_l_Lean_Elab_Term_elabDecimalLit___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("ofDecimal"); +return x_1; +} +} +static lean_object* _init_l_Lean_Elab_Term_elabDecimalLit___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Elab_Term_elabDecimalLit___closed__2; +x_2 = l_Lean_Elab_Term_elabDecimalLit___closed__3; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* l_Lean_Elab_Term_elabDecimalLit(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_Syntax_isDecimalLit_x3f(x_1); +if (lean_obj_tag(x_10) == 0) +{ +lean_object* x_11; +lean_dec(x_2); +x_11 = 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_11; +} +else +{ +lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; +x_12 = lean_ctor_get(x_10, 0); +lean_inc(x_12); +lean_dec(x_10); +x_13 = lean_ctor_get(x_12, 0); +lean_inc(x_13); +x_14 = lean_ctor_get(x_12, 1); +lean_inc(x_14); +lean_dec(x_12); +lean_inc(x_8); +lean_inc(x_7); +lean_inc(x_6); +lean_inc(x_5); +x_15 = l___private_Lean_Elab_Term_0__Lean_Elab_Term_mkFreshTypeMVarFor(x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9); +if (lean_obj_tag(x_15) == 0) +{ +lean_object* x_16; lean_object* x_17; lean_object* x_18; +x_16 = lean_ctor_get(x_15, 0); +lean_inc(x_16); +x_17 = lean_ctor_get(x_15, 1); +lean_inc(x_17); +lean_dec(x_15); +lean_inc(x_8); +lean_inc(x_7); +lean_inc(x_6); +lean_inc(x_5); +lean_inc(x_16); +x_18 = l_Lean_Meta_getDecLevel___at___private_Lean_Elab_Term_0__Lean_Elab_Term_tryLiftAndCoe___spec__1(x_16, x_3, x_4, x_5, x_6, x_7, x_8, x_17); +if (lean_obj_tag(x_18) == 0) +{ +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; +x_19 = lean_ctor_get(x_18, 0); +lean_inc(x_19); +x_20 = lean_ctor_get(x_18, 1); +lean_inc(x_20); +lean_dec(x_18); +x_21 = lean_box(0); +x_22 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_22, 0, x_19); +lean_ctor_set(x_22, 1, x_21); +x_23 = l_Lean_Elab_Term_elabDecimalLit___closed__2; +lean_inc(x_22); +x_24 = l_Lean_mkConst(x_23, x_22); +lean_inc(x_16); +x_25 = l_Lean_mkApp(x_24, x_16); +x_26 = l_Lean_Elab_Term_mkInstMVar(x_25, x_3, x_4, x_5, x_6, x_7, x_8, x_20); +if (lean_obj_tag(x_26) == 0) +{ +uint8_t x_27; +x_27 = !lean_is_exclusive(x_26); +if (x_27 == 0) +{ +lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; +x_28 = lean_ctor_get(x_26, 0); +x_29 = l_Lean_Elab_Term_elabDecimalLit___closed__4; +x_30 = l_Lean_mkConst(x_29, x_22); +x_31 = l_Lean_mkNatLit(x_13); +x_32 = l_Lean_mkNatLit(x_14); +x_33 = l_Lean_mkApp4(x_30, x_16, x_28, x_31, x_32); +lean_ctor_set(x_26, 0, x_33); +return x_26; +} +else +{ +lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; +x_34 = lean_ctor_get(x_26, 0); +x_35 = lean_ctor_get(x_26, 1); +lean_inc(x_35); +lean_inc(x_34); +lean_dec(x_26); +x_36 = l_Lean_Elab_Term_elabDecimalLit___closed__4; +x_37 = l_Lean_mkConst(x_36, x_22); +x_38 = l_Lean_mkNatLit(x_13); +x_39 = l_Lean_mkNatLit(x_14); +x_40 = l_Lean_mkApp4(x_37, x_16, x_34, x_38, x_39); +x_41 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_41, 0, x_40); +lean_ctor_set(x_41, 1, x_35); +return x_41; +} +} +else +{ +uint8_t x_42; +lean_dec(x_22); +lean_dec(x_16); +lean_dec(x_14); +lean_dec(x_13); +x_42 = !lean_is_exclusive(x_26); +if (x_42 == 0) +{ +return x_26; +} +else +{ +lean_object* x_43; lean_object* x_44; lean_object* x_45; +x_43 = lean_ctor_get(x_26, 0); +x_44 = lean_ctor_get(x_26, 1); +lean_inc(x_44); +lean_inc(x_43); +lean_dec(x_26); +x_45 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_45, 0, x_43); +lean_ctor_set(x_45, 1, x_44); +return x_45; +} +} +} +else +{ +uint8_t x_46; +lean_dec(x_16); +lean_dec(x_14); +lean_dec(x_13); +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_46 = !lean_is_exclusive(x_18); +if (x_46 == 0) +{ +return x_18; +} +else +{ +lean_object* x_47; lean_object* x_48; lean_object* x_49; +x_47 = lean_ctor_get(x_18, 0); +x_48 = lean_ctor_get(x_18, 1); +lean_inc(x_48); +lean_inc(x_47); +lean_dec(x_18); +x_49 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_49, 0, x_47); +lean_ctor_set(x_49, 1, x_48); +return x_49; +} +} +} +else +{ +uint8_t x_50; +lean_dec(x_14); +lean_dec(x_13); +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_50 = !lean_is_exclusive(x_15); +if (x_50 == 0) +{ +return x_15; +} +else +{ +lean_object* x_51; lean_object* x_52; lean_object* x_53; +x_51 = lean_ctor_get(x_15, 0); +x_52 = lean_ctor_get(x_15, 1); +lean_inc(x_52); +lean_inc(x_51); +lean_dec(x_15); +x_53 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_53, 0, x_51); +lean_ctor_set(x_53, 1, x_52); +return x_53; +} +} +} +} +} +lean_object* l_Lean_Elab_Term_elabDecimalLit___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_elabDecimalLit(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; +} +} +static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabDecimalLit___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabDecimalLit___boxed), 9, 0); +return x_1; +} +} +lean_object* l___regBuiltin_Lean_Elab_Term_elabDecimalLit(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_Lean_decimalLitKind___closed__2; +x_4 = l___regBuiltin_Lean_Elab_Term_elabDecimalLit___closed__1; +x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); +return x_5; +} +} lean_object* l_Lean_Elab_Term_elabCharLit_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { @@ -37453,7 +37683,7 @@ x_8 = l_Lean_Elab_Term_instMetaEvalTermElabM___rarg(x_1, x_2, x_3, x_4, x_7, x_6 return x_8; } } -static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7541____closed__1() { +static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7628____closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; @@ -37463,7 +37693,7 @@ x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7541_(lean_object* x_1) { +lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7628_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; @@ -37475,7 +37705,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6; x_4 = lean_ctor_get(x_3, 1); lean_inc(x_4); lean_dec(x_3); -x_5 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7541____closed__1; +x_5 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7628____closed__1; x_6 = l_Lean_registerTraceClass(x_5, x_4); if (lean_obj_tag(x_6) == 0) { @@ -38041,6 +38271,19 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabRawNatLit___closed__1); res = l___regBuiltin_Lean_Elab_Term_elabRawNatLit(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); +l_Lean_Elab_Term_elabDecimalLit___closed__1 = _init_l_Lean_Elab_Term_elabDecimalLit___closed__1(); +lean_mark_persistent(l_Lean_Elab_Term_elabDecimalLit___closed__1); +l_Lean_Elab_Term_elabDecimalLit___closed__2 = _init_l_Lean_Elab_Term_elabDecimalLit___closed__2(); +lean_mark_persistent(l_Lean_Elab_Term_elabDecimalLit___closed__2); +l_Lean_Elab_Term_elabDecimalLit___closed__3 = _init_l_Lean_Elab_Term_elabDecimalLit___closed__3(); +lean_mark_persistent(l_Lean_Elab_Term_elabDecimalLit___closed__3); +l_Lean_Elab_Term_elabDecimalLit___closed__4 = _init_l_Lean_Elab_Term_elabDecimalLit___closed__4(); +lean_mark_persistent(l_Lean_Elab_Term_elabDecimalLit___closed__4); +l___regBuiltin_Lean_Elab_Term_elabDecimalLit___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_elabDecimalLit___closed__1(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabDecimalLit___closed__1); +res = l___regBuiltin_Lean_Elab_Term_elabDecimalLit(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); l___regBuiltin_Lean_Elab_Term_elabCharLit___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_elabCharLit___closed__1(); lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabCharLit___closed__1); res = l___regBuiltin_Lean_Elab_Term_elabCharLit(lean_io_mk_world()); @@ -38094,9 +38337,9 @@ l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__2 = _init_l_Lean_Elab_Te lean_mark_persistent(l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__2); l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__3 = _init_l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__3(); lean_mark_persistent(l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__3); -l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7541____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7541____closed__1(); -lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7541____closed__1); -res = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7541_(lean_io_mk_world()); +l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7628____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7628____closed__1(); +lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7628____closed__1); +res = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7628_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); return lean_io_result_mk_ok(lean_box(0)); diff --git a/stage0/stdlib/Lean/Parser.c b/stage0/stdlib/Lean/Parser.c index 0e37a658cf..e49197223e 100644 --- a/stage0/stdlib/Lean/Parser.c +++ b/stage0/stdlib/Lean/Parser.c @@ -15,14 +15,18 @@ extern "C" { #endif lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_strLit_parenthesizer(lean_object*); extern lean_object* l_Lean_Parser_Level_num_formatter___closed__1; +extern lean_object* l_Lean_Parser_Term_decimal_formatter___closed__1; lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_ident_parenthesizer___closed__1; lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_charLit_parenthesizer___closed__1; lean_object* l___regBuiltin_Lean_PrettyPrinter_Formatter_ident_formatter___closed__1; extern lean_object* l_Lean_identKind___closed__2; +lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_decimalLit_parenthesizer___closed__1; +lean_object* l_Lean_Parser_Term_decimal_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_charLitKind___closed__2; lean_object* l_Lean_PrettyPrinter_Parenthesizer_strLit_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_PrettyPrinter_Parenthesizer_mkAntiquot_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_PrettyPrinter_Formatter_charLit_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l___regBuiltin_Lean_PrettyPrinter_Formatter_decimalLit_formatter(lean_object*); lean_object* l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_PrettyPrinter_Parenthesizer_numLit_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_str_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -36,6 +40,7 @@ lean_object* l_Lean_PrettyPrinter_Formatter_ident_formatter(lean_object*, lean_o lean_object* l___regBuiltin_Lean_PrettyPrinter_Formatter_charLit_formatter(lean_object*); lean_object* l___regBuiltin_Lean_PrettyPrinter_Formatter_ident_formatter(lean_object*); lean_object* l___regBuiltin_Lean_PrettyPrinter_Formatter_numLit_formatter(lean_object*); +lean_object* l_Lean_PrettyPrinter_Formatter_decimalLit_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_charLit_parenthesizer(lean_object*); lean_object* l___regBuiltin_Lean_PrettyPrinter_Formatter_strLit_formatter(lean_object*); extern lean_object* l_Lean_strLitKind___closed__2; @@ -44,6 +49,7 @@ extern lean_object* l_Lean_numLitKind___closed__2; extern lean_object* l_Lean_PrettyPrinter_formatterAttribute; lean_object* l_Lean_Parser_Term_char_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_PrettyPrinter_Parenthesizer_charLit_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_PrettyPrinter_Parenthesizer_decimalLit_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_mkAntiquot_formatter(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_mk_antiquot_formatter(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Level_ident_formatter___closed__1; @@ -54,8 +60,11 @@ lean_object* l_Lean_Parser_Term_ident_parenthesizer(lean_object*, lean_object*, lean_object* l_Lean_PrettyPrinter_Formatter_numLit_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_PrettyPrinter_Formatter_strLit_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_PrettyPrinter_Formatter_mkAntiquot_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_decimalLit_parenthesizer(lean_object*); +extern lean_object* l_Lean_decimalLitKind___closed__2; lean_object* l_Lean_Parser_Term_num_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_PrettyPrinter_Formatter_numLit_formatter___closed__1; +lean_object* l___regBuiltin_Lean_PrettyPrinter_Formatter_decimalLit_formatter___closed__1; lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_strLit_parenthesizer___closed__1; extern lean_object* l_Lean_Parser_Term_str_formatter___closed__1; lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_ident_parenthesizer(lean_object*); @@ -133,6 +142,33 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); return x_5; } } +lean_object* l_Lean_PrettyPrinter_Parenthesizer_decimalLit_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; +x_6 = l_Lean_Parser_Term_decimal_parenthesizer(x_1, x_2, x_3, x_4, x_5); +return x_6; +} +} +static lean_object* _init_l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_decimalLit_parenthesizer___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_decimalLit_parenthesizer), 5, 0); +return x_1; +} +} +lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_decimalLit_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_decimalLitKind___closed__2; +x_4 = l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_decimalLit_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_PrettyPrinter_Parenthesizer_charLit_parenthesizer(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { _start: { @@ -263,6 +299,35 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); return x_5; } } +lean_object* l_Lean_PrettyPrinter_Formatter_decimalLit_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_leadingNode_formatter___closed__1; +x_7 = l_Lean_Parser_Term_decimal_formatter___closed__1; +x_8 = l_Lean_PrettyPrinter_Formatter_andthen_formatter(x_6, x_7, x_1, x_2, x_3, x_4, x_5); +return x_8; +} +} +static lean_object* _init_l___regBuiltin_Lean_PrettyPrinter_Formatter_decimalLit_formatter___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_decimalLit_formatter), 5, 0); +return x_1; +} +} +lean_object* l___regBuiltin_Lean_PrettyPrinter_Formatter_decimalLit_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_decimalLitKind___closed__2; +x_4 = l___regBuiltin_Lean_PrettyPrinter_Formatter_decimalLit_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_PrettyPrinter_Formatter_charLit_formatter(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { _start: { @@ -372,6 +437,11 @@ lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_numLit_pare res = l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_numLit_parenthesizer(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); +l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_decimalLit_parenthesizer___closed__1 = _init_l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_decimalLit_parenthesizer___closed__1(); +lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_decimalLit_parenthesizer___closed__1); +res = l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_decimalLit_parenthesizer(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_charLit_parenthesizer___closed__1 = _init_l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_charLit_parenthesizer___closed__1(); lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_charLit_parenthesizer___closed__1); res = l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_charLit_parenthesizer(lean_io_mk_world()); @@ -392,6 +462,11 @@ lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Formatter_numLit_formatte res = l___regBuiltin_Lean_PrettyPrinter_Formatter_numLit_formatter(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); +l___regBuiltin_Lean_PrettyPrinter_Formatter_decimalLit_formatter___closed__1 = _init_l___regBuiltin_Lean_PrettyPrinter_Formatter_decimalLit_formatter___closed__1(); +lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Formatter_decimalLit_formatter___closed__1); +res = l___regBuiltin_Lean_PrettyPrinter_Formatter_decimalLit_formatter(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); l___regBuiltin_Lean_PrettyPrinter_Formatter_charLit_formatter___closed__1 = _init_l___regBuiltin_Lean_PrettyPrinter_Formatter_charLit_formatter___closed__1(); lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Formatter_charLit_formatter___closed__1); res = l___regBuiltin_Lean_PrettyPrinter_Formatter_charLit_formatter(lean_io_mk_world()); diff --git a/stage0/stdlib/Lean/Parser/Basic.c b/stage0/stdlib/Lean/Parser/Basic.c index c6f2fe5784..0d1c4194d7 100644 --- a/stage0/stdlib/Lean/Parser/Basic.c +++ b/stage0/stdlib/Lean/Parser/Basic.c @@ -515,7 +515,6 @@ lean_object* l_Lean_Parser_TokenMap_instInhabitedTokenMap(lean_object*); uint32_t lean_string_utf8_get(lean_object*, lean_object*); lean_object* l_Lean_Parser_ParserState_mergeErrors_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_mkAntiquot___closed__13; -lean_object* l_IO_mkRef___at_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5941____spec__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_errorAtSavedPosFn___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_orelseFnCore___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_symbolFn(lean_object*, lean_object*, lean_object*); @@ -544,10 +543,10 @@ extern lean_object* l_Lean_instInhabitedSyntax; lean_object* l_Lean_Parser_categoryParserOfStackFn_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_checkInsideQuot; lean_object* l_Lean_Parser_nameLitNoAntiquot___closed__3; +lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5942____closed__1; lean_object* l_Lean_Parser_leadingParserAux_match__1___rarg(lean_object*, lean_object*); -lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5941____closed__1; lean_object* l_Lean_Parser_longestMatchMkResult(lean_object*, lean_object*); -lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5960____closed__1; +lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5961____closed__1; size_t l_USize_mul(size_t, size_t); lean_object* l_Lean_Parser_toggleInsideQuot(lean_object*); lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Syntax_forArgsM___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -681,8 +680,8 @@ lean_object* l_Std_RBNode_insert___at_Lean_Parser_TokenMap_insert___spec__5___ra lean_object* l_Lean_Parser_ParserState_mkUnexpectedErrorAt(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_mkAntiquot___closed__24; lean_object* l_Std_RBNode_find___at_Lean_Parser_TokenMap_insert___spec__1(lean_object*); -lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5960____lambda__1(lean_object*); lean_object* l_Lean_Parser_mergeOrElseErrors(lean_object*, lean_object*, lean_object*, uint8_t); +lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5961____lambda__1(lean_object*); lean_object* l_Std_RBNode_find___at_Lean_Parser_indexed___spec__1(lean_object*); lean_object* l_Lean_Parser_withPosition___lambda__1(lean_object*, lean_object*, lean_object*); uint8_t lean_nat_dec_le(lean_object*, lean_object*); @@ -691,7 +690,7 @@ lean_object* l_Lean_Parser_numLitNoAntiquot___closed__3; lean_object* l_Lean_Parser_categoryParser(lean_object*, lean_object*); lean_object* l_Lean_Parser_Parser_info___default___elambda__2___boxed(lean_object*); uint8_t l_Std_RBNode_isRed___rarg(lean_object*); -lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5941____lambda__1(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5942____lambda__1(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_ParserState_mkError_match__1(lean_object*); lean_object* l_Lean_Parser_antiquotNestedExpr___closed__6; lean_object* l_Lean_Parser_mkAntiquot___closed__22; @@ -735,6 +734,7 @@ lean_object* l_Lean_Parser_categoryParser___elambda__1(lean_object*, lean_object lean_object* l_Lean_Parser_pushNone___elambda__1(lean_object*); lean_object* l_Lean_Parser_tryAnti_match__2___rarg(lean_object*, lean_object*); lean_object* l_Lean_Parser_FirstTokens_toStr___closed__2; +lean_object* l_IO_mkRef___at_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5942____spec__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_rawIdentNoAntiquot; lean_object* l_Lean_Parser_ParserState_replaceLongest(lean_object*, lean_object*); lean_object* l_Lean_Parser_ident___elambda__1___closed__2; @@ -751,6 +751,7 @@ lean_object* l_Std_RBNode_insert___at_Lean_Parser_TokenMap_insert___spec__5(lean lean_object* l_Lean_Parser_checkNoWsBefore___elambda__1(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_PrattParsingTables_trailingParsers___default; lean_object* l_Lean_Parser_noFirstTokenInfo___elambda__2(lean_object*, lean_object*); +lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5942____lambda__1___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_withoutPosition(lean_object*); lean_object* l_Array_qsort_sort___at_Lean_Parser_Error_toString___spec__1(lean_object*, lean_object*, lean_object*); lean_object* l_Std_RBNode_ins___at_Lean_Parser_TokenMap_insert___spec__6___rarg(lean_object*, lean_object*, lean_object*); @@ -793,7 +794,6 @@ lean_object* l_Std_RBNode_find___at_Lean_Parser_indexed___spec__1___rarg(lean_ob lean_object* l_Lean_Parser_checkOutsideQuotFn___boxed(lean_object*, lean_object*); lean_object* lean_array_pop(lean_object*); lean_object* l_Lean_Parser_TokenMap_insert___rarg(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5941____lambda__1___boxed(lean_object*, lean_object*, lean_object*); extern size_t l_Std_PersistentHashMap_insertAux___rarg___closed__2; lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_nameLitAux_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_strAux_parse___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -812,8 +812,8 @@ lean_object* l_Lean_Parser_indexed_match__1___rarg(lean_object*, lean_object*, l lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_tokenFnAux_match__1(lean_object*); lean_object* l_Lean_Parser_mkAntiquot___closed__6; lean_object* l_Lean_Parser_rawIdent___closed__1; -lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5960_(lean_object*); -lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5941_(lean_object*); +lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5961_(lean_object*); +lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5942_(lean_object*); lean_object* l_Lean_Parser_fieldIdx___closed__7; lean_object* l_Lean_Parser_mkAntiquot(lean_object*, lean_object*, uint8_t); lean_object* l_Lean_Parser_optionaInfo___elambda__1(lean_object*, lean_object*); @@ -8730,20 +8730,20 @@ x_15 = lean_string_utf8_get(x_7, x_14); x_16 = l_Char_isDigit(x_15); if (x_16 == 0) { -lean_object* x_17; lean_object* x_18; -lean_dec(x_14); -x_17 = l_Lean_decimalLitKind; -x_18 = l_Lean_Parser_mkNodeToken(x_17, x_1, x_2, x_5); -return x_18; +lean_object* x_17; lean_object* x_18; lean_object* x_19; +x_17 = l_Lean_Parser_ParserState_setPos(x_5, x_14); +x_18 = l_Lean_decimalLitKind; +x_19 = l_Lean_Parser_mkNodeToken(x_18, x_1, x_2, x_17); +return x_19; } else { -lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; -x_19 = l_Lean_Parser_ParserState_setPos(x_5, x_14); -x_20 = l_Lean_Parser_takeWhileFn(x_4, x_2, x_19); -x_21 = l_Lean_decimalLitKind; -x_22 = l_Lean_Parser_mkNodeToken(x_21, x_1, x_2, x_20); -return x_22; +lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; +x_20 = l_Lean_Parser_ParserState_setPos(x_5, x_14); +x_21 = l_Lean_Parser_takeWhileFn(x_4, x_2, x_20); +x_22 = l_Lean_decimalLitKind; +x_23 = l_Lean_Parser_mkNodeToken(x_22, x_1, x_2, x_21); +return x_23; } } } @@ -25948,7 +25948,7 @@ lean_dec(x_1); return x_6; } } -lean_object* l_IO_mkRef___at_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5941____spec__1(lean_object* x_1, lean_object* x_2) { +lean_object* l_IO_mkRef___at_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5942____spec__1(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; uint8_t x_4; @@ -25973,7 +25973,7 @@ return x_7; } } } -lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5941____lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5942____lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { lean_object* x_4; @@ -25981,34 +25981,34 @@ x_4 = l_Lean_Parser_whitespace(x_2, x_3); return x_4; } } -static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5941____closed__1() { +static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5942____closed__1() { _start: { lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5941____lambda__1___boxed), 3, 0); +x_1 = lean_alloc_closure((void*)(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5942____lambda__1___boxed), 3, 0); return x_1; } } -lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5941_(lean_object* x_1) { +lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5942_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; -x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5941____closed__1; -x_3 = l_IO_mkRef___at_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5941____spec__1(x_2, x_1); +x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5942____closed__1; +x_3 = l_IO_mkRef___at_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5942____spec__1(x_2, x_1); return x_3; } } -lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5941____lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5942____lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { lean_object* x_4; -x_4 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5941____lambda__1(x_1, x_2, x_3); +x_4 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5942____lambda__1(x_1, x_2, x_3); lean_dec(x_2); lean_dec(x_1); return x_4; } } -lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5960____lambda__1(lean_object* x_1) { +lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5961____lambda__1(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; uint8_t x_4; @@ -26034,19 +26034,19 @@ return x_7; } } } -static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5960____closed__1() { +static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5961____closed__1() { _start: { lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5960____lambda__1), 1, 0); +x_1 = lean_alloc_closure((void*)(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5961____lambda__1), 1, 0); return x_1; } } -lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5960_(lean_object* x_1) { +lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5961_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; -x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5960____closed__1; +x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5961____closed__1; x_3 = l_Lean_EnvExtensionInterfaceUnsafe_registerExt___rarg(x_2, x_1); return x_3; } @@ -29705,16 +29705,16 @@ l_Lean_Parser_instInhabitedParserCategory___closed__1 = _init_l_Lean_Parser_inst lean_mark_persistent(l_Lean_Parser_instInhabitedParserCategory___closed__1); l_Lean_Parser_instInhabitedParserCategory = _init_l_Lean_Parser_instInhabitedParserCategory(); lean_mark_persistent(l_Lean_Parser_instInhabitedParserCategory); -l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5941____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5941____closed__1(); -lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5941____closed__1); -res = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5941_(lean_io_mk_world()); +l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5942____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5942____closed__1(); +lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5942____closed__1); +res = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5942_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; l_Lean_Parser_categoryParserFnRef = lean_io_result_get_value(res); lean_mark_persistent(l_Lean_Parser_categoryParserFnRef); lean_dec_ref(res); -l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5960____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5960____closed__1(); -lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5960____closed__1); -res = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5960_(lean_io_mk_world()); +l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5961____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5961____closed__1(); +lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5961____closed__1); +res = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_5961_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; l_Lean_Parser_categoryParserFnExtension = lean_io_result_get_value(res); lean_mark_persistent(l_Lean_Parser_categoryParserFnExtension); diff --git a/stage0/stdlib/Lean/PrettyPrinter/Delaborator/Builtins.c b/stage0/stdlib/Lean/PrettyPrinter/Delaborator/Builtins.c index 8bd623356e..854cef5d90 100644 --- a/stage0/stdlib/Lean/PrettyPrinter/Delaborator/Builtins.c +++ b/stage0/stdlib/Lean/PrettyPrinter/Delaborator/Builtins.c @@ -20,6 +20,7 @@ lean_object* l_Lean_PrettyPrinter_Delaborator_AppMatchState_moreArgs___default; lean_object* l_Lean_PrettyPrinter_Delaborator_delabProjectionApp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppImplicit___closed__4; extern lean_object* l_Lean_Name_toString___closed__1; +extern lean_object* l_Lean_decimalLitKind; lean_object* l_Array_mapIdxM_map___at_Lean_PrettyPrinter_Delaborator_delabStructureInstance___spec__1___closed__1; lean_object* l_Lean_PrettyPrinter_Delaborator_delabTuple___closed__1; extern lean_object* l_Lean_Meta_Match_Pattern_toExpr_visit___closed__2; @@ -177,6 +178,7 @@ extern lean_object* l_Lean_PrettyPrinter_Delaborator_withAppFn___rarg___closed__ lean_object* l_Lean_PrettyPrinter_Delaborator_delabDo___lambda__1___closed__1; uint8_t l_Lean_Name_isPrefixOf(lean_object*, lean_object*); lean_object* l_Lean_Expr_getOptParamDefault_x3f(lean_object*); +lean_object* lean_string_utf8_extract(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_PrettyPrinter_Delaborator_delabMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_PrettyPrinter_Delaborator_delabNil___closed__1; lean_object* l_Lean_PrettyPrinter_Delaborator_delabMVar___closed__4; @@ -315,6 +317,7 @@ lean_object* l_Lean_PrettyPrinter_Delaborator_delabConst___lambda__2(lean_object lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppMatch___lambda__3___closed__5; lean_object* lean_array_get(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_PrettyPrinter_Delaborator_delabMData___closed__5; +lean_object* l_Lean_PrettyPrinter_Delaborator_delabOfDecimal___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_PrettyPrinter_Delaborator_delabCoe___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_PrettyPrinter_Delaborator_delabBVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_PrettyPrinter_Delaborator_delabConst___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -324,6 +327,7 @@ lean_object* l_Lean_PrettyPrinter_Delaborator_delabListToArray___lambda__1(lean_ lean_object* l_Lean_PrettyPrinter_Delaborator_delabSort___closed__3; lean_object* l_Lean_PrettyPrinter_Delaborator_delabTuple___lambda__1___closed__1; lean_object* l___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_shouldGroupWithNext(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__1; lean_object* l_Lean_PrettyPrinter_Delaborator_delabMVar_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabAppMatch___closed__1; lean_object* l___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_skippingBinders___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -353,6 +357,7 @@ lean_object* l_Lean_PrettyPrinter_Delaborator_delabTuple___lambda__1___boxed(lea lean_object* l_Lean_PrettyPrinter_Delaborator_delabMVar___closed__5; lean_object* l_Lean_Meta_inferType___at___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_delabPatterns___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_PrettyPrinter_Delaborator_delabFVar___closed__1; +extern lean_object* l_Lean_Elab_Term_elabDecimalLit___closed__3; size_t l_Lean_Name_hash(lean_object*); extern lean_object* l_Lean_PrettyPrinter_Delaborator_delabAttribute; lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppMatch___lambda__3___closed__15; @@ -367,6 +372,7 @@ extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_333____clos lean_object* l_Lean_PrettyPrinter_Delaborator_delabBVar_match__1(lean_object*); lean_object* l___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_unresolveUsingNamespace(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_myMacro____x40_Init_Notation___hyg_8644____closed__4; +lean_object* l_Lean_PrettyPrinter_Delaborator_delabOfDecimal_match__1(lean_object*); extern lean_object* l_Lean_instInhabitedSourceInfo___closed__1; lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfNat___closed__2; lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppMatch___closed__5; @@ -379,6 +385,7 @@ lean_object* l_Lean_PrettyPrinter_Delaborator_delabForall(lean_object*, lean_obj lean_object* l_Lean_PrettyPrinter_Delaborator_delabOfNat___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_List_headD___rarg(lean_object*, lean_object*); extern lean_object* l_Lean_Elab_Term_mkExplicitBinder___closed__5; +lean_object* l_Lean_PrettyPrinter_Delaborator_delabOfDecimal(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_myMacro____x40_Init_Notation___hyg_13596____closed__8; lean_object* l_Array_mapIdxM_map___at___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_delabPatterns___spec__3___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppExplicit_match__2(lean_object*); @@ -390,6 +397,7 @@ extern lean_object* l_myMacro____x40_Init_Notation___hyg_13219____closed__8; lean_object* lean_array_to_list(lean_object*, lean_object*); lean_object* l_Lean_PrettyPrinter_Delaborator_delabLam___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_Name_isAtomic(lean_object*); +lean_object* l_Lean_PrettyPrinter_Delaborator_delabOfDecimal_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_PrettyPrinter_Delaborator_delabStructureInstance___lambda__3___closed__6; extern lean_object* l_Lean_PrettyPrinter_Delaborator_getExprKind___closed__4; extern lean_object* l_Lean_protectedExt; @@ -422,6 +430,7 @@ size_t lean_usize_modn(size_t, lean_object*); lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNil___closed__2; lean_object* l_Lean_PrettyPrinter_Delaborator_delabProjectionApp___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_mkSimpleThunk___closed__1; +lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__3; lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppWithUnexpander___closed__3; lean_object* l_Lean_PrettyPrinter_Delaborator_delabConst_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabMData(lean_object*); @@ -481,6 +490,7 @@ lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppMatch___lambda__3___closed lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabFVar(lean_object*); lean_object* l_Lean_PrettyPrinter_Delaborator_withBindingBodyUnusedName___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppWithUnexpander_match__2___rarg(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_PrettyPrinter_Delaborator_delabOfDecimal___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabListToArray___closed__1; lean_object* l_Lean_PrettyPrinter_Delaborator_getParamKinds___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Meta_Match_Pattern_toExpr_visit___closed__3; @@ -628,9 +638,11 @@ lean_object* l_Lean_PrettyPrinter_Delaborator_delabSort_match__1(lean_object*); lean_object* l_Lean_Meta_setMCtx___at___private_Lean_Meta_Basic_0__Lean_Meta_liftMkBindingM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_myMacro____x40_Init_Notation___hyg_9577____closed__6; lean_object* l_Lean_PrettyPrinter_Delaborator_delabDoElems___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__2; extern lean_object* l_Lean_PrettyPrinter_Delaborator_getExprKind___closed__5; lean_object* l_Lean_PrettyPrinter_Delaborator_delabForall_match__1(lean_object*); lean_object* l_Lean_getPPExplicit___boxed(lean_object*); +lean_object* l_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__1; lean_object* l_Array_mapMUnsafe_map___at_Lean_PrettyPrinter_Delaborator_delabDo___spec__1___closed__2; lean_object* l_Array_zipWithAux___at_Lean_PrettyPrinter_Delaborator_delabAppMatch___spec__4___closed__1; lean_object* l_Lean_PrettyPrinter_Delaborator_delabConst___lambda__1___closed__5; @@ -680,6 +692,7 @@ lean_object* l_Array_mapIdxM_map___at___private_Lean_PrettyPrinter_Delaborator_B lean_object* l_Lean_Meta_inferType___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Array_instReprArray___rarg___closed__1; lean_object* l_Lean_PrettyPrinter_Delaborator_delabOfNat___closed__3; +lean_object* lean_string_length(lean_object*); lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppWithUnexpander___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabAppWithUnexpander(lean_object*); lean_object* l_List_forIn_loop___at_Lean_PrettyPrinter_Delaborator_delabMData___spec__3___lambda__1(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -696,6 +709,7 @@ lean_object* l_Lean_PrettyPrinter_Delaborator_delabSort___closed__11; lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabBVar___closed__1; extern lean_object* l_Lean_mkOptionalNode___closed__2; lean_object* l_Std_HashMapImp_find_x3f___at_Lean_PrettyPrinter_Delaborator_delabAppWithUnexpander___spec__5___boxed(lean_object*, lean_object*); +lean_object* l_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__2; lean_object* l_Lean_PrettyPrinter_Delaborator_delabDo___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Std_RBNode_insert___at_Lean_PrettyPrinter_Delaborator_delabMData___spec__1(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_PrettyPrinter_Delaborator_delabDoElems___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -776,6 +790,7 @@ lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCoeFun___closed_ extern lean_object* l_addParenHeuristic___closed__1; lean_object* l___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_shouldGroupWithNext_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_unresolveUsingNamespace___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +extern lean_object* l_Lean_Elab_Term_elabDecimalLit___closed__1; lean_object* l_Std_AssocList_find_x3f___at_Lean_PrettyPrinter_Delaborator_delabAppWithUnexpander___spec__6___boxed(lean_object*, lean_object*); extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_578____closed__8; lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppImplicit_match__3___rarg(lean_object*, lean_object*); @@ -783,6 +798,7 @@ lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabProjectionApp(le uint8_t l_Lean_Expr_isLet(lean_object*); extern lean_object* l_myMacro____x40_Init_Notation___hyg_14258____closed__2; uint8_t l_Lean_isStructure(lean_object*, lean_object*); +lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfDecimal(lean_object*); lean_object* l_Lean_PrettyPrinter_Delaborator_delabNamedPattern(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNil(lean_object*); lean_object* l_Lean_Syntax_mkLit(lean_object*, lean_object*, lean_object*); @@ -16316,6 +16332,332 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); return x_5; } } +lean_object* l_Lean_PrettyPrinter_Delaborator_delabOfDecimal_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +if (lean_obj_tag(x_1) == 5) +{ +lean_object* x_4; +x_4 = lean_ctor_get(x_1, 0); +lean_inc(x_4); +if (lean_obj_tag(x_4) == 5) +{ +lean_object* x_5; +x_5 = lean_ctor_get(x_4, 1); +lean_inc(x_5); +if (lean_obj_tag(x_5) == 9) +{ +lean_object* x_6; +x_6 = lean_ctor_get(x_5, 0); +lean_inc(x_6); +if (lean_obj_tag(x_6) == 0) +{ +lean_object* x_7; +x_7 = lean_ctor_get(x_1, 1); +lean_inc(x_7); +if (lean_obj_tag(x_7) == 9) +{ +lean_object* x_8; +x_8 = lean_ctor_get(x_7, 0); +lean_inc(x_8); +if (lean_obj_tag(x_8) == 0) +{ +uint64_t x_9; lean_object* x_10; uint64_t x_11; uint64_t x_12; lean_object* x_13; uint64_t 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_dec(x_3); +x_9 = lean_ctor_get_uint64(x_1, sizeof(void*)*2); +lean_dec(x_1); +x_10 = lean_ctor_get(x_4, 0); +lean_inc(x_10); +x_11 = lean_ctor_get_uint64(x_4, sizeof(void*)*2); +lean_dec(x_4); +x_12 = lean_ctor_get_uint64(x_5, sizeof(void*)*1); +lean_dec(x_5); +x_13 = lean_ctor_get(x_6, 0); +lean_inc(x_13); +lean_dec(x_6); +x_14 = lean_ctor_get_uint64(x_7, sizeof(void*)*1); +lean_dec(x_7); +x_15 = lean_ctor_get(x_8, 0); +lean_inc(x_15); +lean_dec(x_8); +x_16 = lean_box_uint64(x_12); +x_17 = lean_box_uint64(x_11); +x_18 = lean_box_uint64(x_14); +x_19 = lean_box_uint64(x_9); +x_20 = lean_apply_7(x_2, x_10, x_13, x_16, x_17, x_15, x_18, x_19); +return x_20; +} +else +{ +lean_object* x_21; +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_2); +x_21 = lean_apply_1(x_3, x_1); +return x_21; +} +} +else +{ +lean_object* x_22; +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_2); +x_22 = lean_apply_1(x_3, x_1); +return x_22; +} +} +else +{ +lean_object* x_23; +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_2); +x_23 = lean_apply_1(x_3, x_1); +return x_23; +} +} +else +{ +lean_object* x_24; +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_2); +x_24 = lean_apply_1(x_3, x_1); +return x_24; +} +} +else +{ +lean_object* x_25; +lean_dec(x_4); +lean_dec(x_2); +x_25 = lean_apply_1(x_3, x_1); +return x_25; +} +} +else +{ +lean_object* x_26; +lean_dec(x_2); +x_26 = lean_apply_1(x_3, x_1); +return x_26; +} +} +} +lean_object* l_Lean_PrettyPrinter_Delaborator_delabOfDecimal_match__1(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Delaborator_delabOfDecimal_match__1___rarg), 3, 0); +return x_2; +} +} +lean_object* l_Lean_PrettyPrinter_Delaborator_delabOfDecimal___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) { +_start: +{ +if (lean_obj_tag(x_1) == 5) +{ +lean_object* x_8; +x_8 = lean_ctor_get(x_1, 0); +lean_inc(x_8); +if (lean_obj_tag(x_8) == 5) +{ +lean_object* x_9; +x_9 = lean_ctor_get(x_8, 1); +lean_inc(x_9); +lean_dec(x_8); +if (lean_obj_tag(x_9) == 9) +{ +lean_object* x_10; +x_10 = lean_ctor_get(x_9, 0); +lean_inc(x_10); +lean_dec(x_9); +if (lean_obj_tag(x_10) == 0) +{ +lean_object* x_11; +x_11 = lean_ctor_get(x_1, 1); +lean_inc(x_11); +lean_dec(x_1); +if (lean_obj_tag(x_11) == 9) +{ +lean_object* x_12; +x_12 = lean_ctor_get(x_11, 0); +lean_inc(x_12); +lean_dec(x_11); +if (lean_obj_tag(x_12) == 0) +{ +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; 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; +x_13 = lean_ctor_get(x_10, 0); +lean_inc(x_13); +lean_dec(x_10); +x_14 = lean_ctor_get(x_12, 0); +lean_inc(x_14); +lean_dec(x_12); +x_15 = l_Nat_repr(x_13); +x_16 = lean_string_length(x_15); +x_17 = lean_nat_sub(x_16, x_14); +lean_dec(x_14); +x_18 = lean_unsigned_to_nat(0u); +x_19 = lean_string_utf8_extract(x_15, x_18, x_17); +x_20 = lean_string_utf8_extract(x_15, x_17, x_16); +lean_dec(x_16); +lean_dec(x_17); +lean_dec(x_15); +x_21 = l_Lean_Name_toString___closed__1; +x_22 = lean_string_append(x_19, x_21); +x_23 = lean_string_append(x_22, x_20); +lean_dec(x_20); +x_24 = l_Lean_decimalLitKind; +x_25 = l_Lean_instInhabitedSourceInfo___closed__1; +x_26 = l_Lean_Syntax_mkLit(x_24, x_23, x_25); +x_27 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_27, 0, x_26); +lean_ctor_set(x_27, 1, x_7); +return x_27; +} +else +{ +lean_object* x_28; +lean_dec(x_12); +lean_dec(x_10); +x_28 = l_Lean_PrettyPrinter_Delaborator_failure___rarg(x_7); +return x_28; +} +} +else +{ +lean_object* x_29; +lean_dec(x_11); +lean_dec(x_10); +x_29 = l_Lean_PrettyPrinter_Delaborator_failure___rarg(x_7); +return x_29; +} +} +else +{ +lean_object* x_30; +lean_dec(x_10); +lean_dec(x_1); +x_30 = l_Lean_PrettyPrinter_Delaborator_failure___rarg(x_7); +return x_30; +} +} +else +{ +lean_object* x_31; +lean_dec(x_9); +lean_dec(x_1); +x_31 = l_Lean_PrettyPrinter_Delaborator_failure___rarg(x_7); +return x_31; +} +} +else +{ +lean_object* x_32; +lean_dec(x_8); +lean_dec(x_1); +x_32 = l_Lean_PrettyPrinter_Delaborator_failure___rarg(x_7); +return x_32; +} +} +else +{ +lean_object* x_33; +lean_dec(x_1); +x_33 = l_Lean_PrettyPrinter_Delaborator_failure___rarg(x_7); +return x_33; +} +} +} +static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Delaborator_delabOfDecimal___lambda__1___boxed), 7, 0); +return x_1; +} +} +static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___closed__1; +x_2 = l_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__1; +x_3 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_PrettyPrinter_Delaborator_delabAppExplicit___spec__2___rarg), 8, 2); +lean_closure_set(x_3, 0, x_1); +lean_closure_set(x_3, 1, x_2); +return x_3; +} +} +lean_object* l_Lean_PrettyPrinter_Delaborator_delabOfDecimal(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +lean_object* x_7; lean_object* x_8; lean_object* x_9; +x_7 = l_Lean_PrettyPrinter_Delaborator_delabOfNat___closed__3; +x_8 = l_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__2; +x_9 = l_Lean_PrettyPrinter_Delaborator_whenPPOption(x_7, x_8, x_1, x_2, x_3, x_4, x_5, x_6); +return x_9; +} +} +lean_object* l_Lean_PrettyPrinter_Delaborator_delabOfDecimal___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) { +_start: +{ +lean_object* x_8; +x_8 = l_Lean_PrettyPrinter_Delaborator_delabOfDecimal___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +return x_8; +} +} +static lean_object* _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__1() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_PrettyPrinter_Delaborator_getExprKind___closed__5; +x_2 = l_Lean_Elab_Term_elabDecimalLit___closed__1; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +static lean_object* _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__1; +x_2 = l_Lean_Elab_Term_elabDecimalLit___closed__3; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +static lean_object* _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Delaborator_delabOfDecimal), 6, 0); +return x_1; +} +} +lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfDecimal(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_Delaborator_delabAttribute; +x_3 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__2; +x_4 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__3; +x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); +return x_5; +} +} lean_object* l_Lean_PrettyPrinter_Delaborator_delabProj_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { @@ -16366,7 +16708,7 @@ _start: lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_1 = l_Lean_PrettyPrinter_Delaborator_delabFVar___closed__1; x_2 = l_Lean_PrettyPrinter_Delaborator_delabProj___closed__1; -x_3 = lean_unsigned_to_nat(378u); +x_3 = lean_unsigned_to_nat(387u); x_4 = lean_unsigned_to_nat(38u); x_5 = l_Lean_Syntax_strLitToAtom___closed__3; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -21038,7 +21380,7 @@ _start: lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_1 = l_Lean_PrettyPrinter_Delaborator_delabFVar___closed__1; x_2 = l_Lean_PrettyPrinter_Delaborator_delabDoElems___closed__1; -x_3 = lean_unsigned_to_nat(519u); +x_3 = lean_unsigned_to_nat(528u); x_4 = lean_unsigned_to_nat(40u); x_5 = l_Lean_Syntax_strLitToAtom___closed__3; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -22032,6 +22374,19 @@ lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfNat___ res = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfNat(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); +l_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__1 = _init_l_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__1(); +lean_mark_persistent(l_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__1); +l_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__2 = _init_l_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__2(); +lean_mark_persistent(l_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__2); +l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__1 = _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__1(); +lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__1); +l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__2 = _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__2(); +lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__2); +l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__3 = _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__3(); +lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfDecimal___closed__3); +res = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfDecimal(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); l_Lean_PrettyPrinter_Delaborator_delabProj___closed__1 = _init_l_Lean_PrettyPrinter_Delaborator_delabProj___closed__1(); lean_mark_persistent(l_Lean_PrettyPrinter_Delaborator_delabProj___closed__1); l_Lean_PrettyPrinter_Delaborator_delabProj___closed__2 = _init_l_Lean_PrettyPrinter_Delaborator_delabProj___closed__2();