chore: update stage0
This commit is contained in:
Leonardo de Moura
parent
85c9ab072c
commit
e8b58abffc
9 changed files with 1178 additions and 462 deletions
24
stage0/src/Lean/Elab/Term.lean
generated
24
stage0/src/Lean/Elab/Term.lean
generated
|
|
@ -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)
|
||||
|
|
|
|||
2
stage0/src/Lean/Parser.lean
generated
2
stage0/src/Lean/Parser.lean
generated
|
|
@ -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
|
||||
|
||||
|
|
|
|||
2
stage0/src/Lean/Parser/Basic.lean
generated
2
stage0/src/Lean/Parser/Basic.lean
generated
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
44
stage0/stdlib/Lean/Elab/Binders.c
generated
44
stage0/stdlib/Lean/Elab/Binders.c
generated
|
|
@ -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:
|
||||
{
|
||||
|
|
|
|||
1047
stage0/stdlib/Lean/Elab/Term.c
generated
1047
stage0/stdlib/Lean/Elab/Term.c
generated
File diff suppressed because it is too large
Load diff
75
stage0/stdlib/Lean/Parser.c
generated
75
stage0/stdlib/Lean/Parser.c
generated
|
|
@ -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());
|
||||
|
|
|
|||
78
stage0/stdlib/Lean/Parser/Basic.c
generated
78
stage0/stdlib/Lean/Parser/Basic.c
generated
|
|
@ -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);
|
||||
|
|
|
|||
359
stage0/stdlib/Lean/PrettyPrinter/Delaborator/Builtins.c
generated
359
stage0/stdlib/Lean/PrettyPrinter/Delaborator/Builtins.c
generated
|
|
@ -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();
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue