From f2bbe222d78ae9eb092462824d59587e08d08da9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 6 Aug 2021 14:08:01 -0700 Subject: [PATCH] chore: update stage0 --- stage0/src/Lean/Elab/BuiltinCommand.lean | 8 + stage0/src/Lean/Meta/ReduceEval.lean | 3 +- stage0/src/Lean/Parser/Basic.lean | 20 +- stage0/src/Lean/ParserCompiler.lean | 9 +- .../Lean/PrettyPrinter/Delaborator/Basic.lean | 17 +- .../PrettyPrinter/Delaborator/SubExpr.lean | 4 +- .../Delaborator/TopDownAnalyze.lean | 17 +- stage0/src/Lean/PrettyPrinter/Formatter.lean | 11 +- .../src/Lean/PrettyPrinter/Parenthesizer.lean | 12 +- stage0/stdlib/Lean/Elab/BuiltinCommand.c | 732 +++++++++++++----- stage0/stdlib/Lean/Elab/Syntax.c | 4 +- stage0/stdlib/Lean/Parser/Basic.c | 169 ++-- stage0/stdlib/Lean/ParserCompiler.c | 2 +- .../Lean/PrettyPrinter/Delaborator/Basic.c | 2 +- .../Delaborator/TopDownAnalyze.c | 4 +- stage0/stdlib/Lean/PrettyPrinter/Formatter.c | 2 +- 16 files changed, 691 insertions(+), 325 deletions(-) diff --git a/stage0/src/Lean/Elab/BuiltinCommand.lean b/stage0/src/Lean/Elab/BuiltinCommand.lean index 27dd560bc2..cf6c08e208 100644 --- a/stage0/src/Lean/Elab/BuiltinCommand.lean +++ b/stage0/src/Lean/Elab/BuiltinCommand.lean @@ -3,11 +3,19 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +import Lean.DocString import Lean.Elab.Command import Lean.Elab.Open namespace Lean.Elab.Command +@[builtinCommandElab moduleDoc] def elabModuleDoc : CommandElab := fun stx => + match stx[1] with + | Syntax.atom _ val => + let doc := val.extract 0 (val.bsize - 2) + modifyEnv fun env => addMainModuleDoc env doc + | _ => throwErrorAt stx "unexpected module doc string{indentD stx[1]}" + private def addScope (isNewNamespace : Bool) (header : String) (newNamespace : Name) : CommandElabM Unit := do modify fun s => { s with env := s.env.registerNamespace newNamespace, diff --git a/stage0/src/Lean/Meta/ReduceEval.lean b/stage0/src/Lean/Meta/ReduceEval.lean index 6c867be776..ab28b50c0f 100644 --- a/stage0/src/Lean/Meta/ReduceEval.lean +++ b/stage0/src/Lean/Meta/ReduceEval.lean @@ -3,11 +3,10 @@ Copyright (c) 2020 Sebastian Ullrich. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Sebastian Ullrich -/ +import Lean.Meta.Offset /-! Evaluation by reduction -/ -import Lean.Meta.Offset - namespace Lean.Meta class ReduceEval (α : Type) where diff --git a/stage0/src/Lean/Parser/Basic.lean b/stage0/src/Lean/Parser/Basic.lean index 6f9faef7c6..a9740fa7d4 100644 --- a/stage0/src/Lean/Parser/Basic.lean +++ b/stage0/src/Lean/Parser/Basic.lean @@ -3,6 +3,15 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Sebastian Ullrich -/ +import Lean.Data.Trie +import Lean.Data.Position +import Lean.Syntax +import Lean.ToExpr +import Lean.Environment +import Lean.Attributes +import Lean.Message +import Lean.Compiler.InitAttr +import Lean.ResolveName /-! # Basic Lean parser infrastructure @@ -54,15 +63,6 @@ running multiple parsers should check if an error message is set in the parser s Error recovery is left to the designer of the specific language; for example, Lean's top-level `parseCommand` loop skips tokens until the next command keyword on error. -/ -import Lean.Data.Trie -import Lean.Data.Position -import Lean.Syntax -import Lean.ToExpr -import Lean.Environment -import Lean.Attributes -import Lean.Message -import Lean.Compiler.InitAttr -import Lean.ResolveName namespace Lean @@ -772,7 +772,7 @@ partial def whitespace : ParserFn := fun c s => if curr == '-' then let i := input.next i let curr := input.get i - if curr == '-' then s -- "/--" doc comment is an actual token + if curr == '-' || curr == '!' then s -- "/--" and "/-!" doc comment are actual tokens else andthenFn (finishCommentBlock 1) whitespace c (s.next input i) else s else s diff --git a/stage0/src/Lean/ParserCompiler.lean b/stage0/src/Lean/ParserCompiler.lean index 5b42588338..53b09cf806 100644 --- a/stage0/src/Lean/ParserCompiler.lean +++ b/stage0/src/Lean/ParserCompiler.lean @@ -3,17 +3,16 @@ Copyright (c) 2020 Sebastian Ullrich. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Sebastian Ullrich -/ - -/-! -Gadgets for compiling parser declarations into other programs, such as pretty printers. --/ - import Lean.Util.ReplaceExpr import Lean.Meta.Basic import Lean.Meta.WHNF import Lean.ParserCompiler.Attribute import Lean.Parser.Extension +/-! +Gadgets for compiling parser declarations into other programs, such as pretty printers. +-/ + namespace Lean namespace ParserCompiler diff --git a/stage0/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/stage0/src/Lean/PrettyPrinter/Delaborator/Basic.lean index d23957605f..fdb32397fc 100644 --- a/stage0/src/Lean/PrettyPrinter/Delaborator/Basic.lean +++ b/stage0/src/Lean/PrettyPrinter/Delaborator/Basic.lean @@ -3,6 +3,14 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Sebastian Ullrich -/ +import Lean.KeyedDeclsAttribute +import Lean.ProjFns +import Lean.Syntax +import Lean.Meta.Match +import Lean.Elab.Term +import Lean.PrettyPrinter.Delaborator.Options +import Lean.PrettyPrinter.Delaborator.SubExpr +import Lean.PrettyPrinter.Delaborator.TopDownAnalyze /-! The delaborator is the first stage of the pretty printer, and the inverse of the @@ -25,15 +33,6 @@ back to the subterm. The delaborator is extensible via the `[delab]` attribute. -/ -import Lean.KeyedDeclsAttribute -import Lean.ProjFns -import Lean.Syntax -import Lean.Meta.Match -import Lean.Elab.Term -import Lean.PrettyPrinter.Delaborator.Options -import Lean.PrettyPrinter.Delaborator.SubExpr -import Lean.PrettyPrinter.Delaborator.TopDownAnalyze - namespace Lean.PrettyPrinter.Delaborator open Lean.Meta SubExpr diff --git a/stage0/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean b/stage0/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean index 2c969c8f12..cdf37f52ca 100644 --- a/stage0/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean +++ b/stage0/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean @@ -3,6 +3,8 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Daniel Selsam -/ +import Lean.Meta.Basic +import Std.Data.RBMap /-! This file defines utilities for `MetaM` computations to traverse subexpressions @@ -13,8 +15,6 @@ map a path of `childIdxs` to a natural number by computing the value of the 4-ar representation `1 :: childIdxs`, since n-ary representations without leading zeros are unique. Note that `pos` is initialized to `1` (case `childIdxs == []`). -/ -import Lean.Meta.Basic -import Std.Data.RBMap namespace Lean.PrettyPrinter.Delaborator diff --git a/stage0/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/stage0/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean index 1498a66eb9..d555eb1854 100644 --- a/stage0/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean +++ b/stage0/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean @@ -3,6 +3,14 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Daniel Selsam -/ +import Lean.Meta +import Lean.Util.FindMVar +import Lean.Util.FindLevelMVar +import Lean.Util.CollectLevelParams +import Lean.Util.ReplaceLevel +import Lean.PrettyPrinter.Delaborator.Options +import Lean.PrettyPrinter.Delaborator.SubExpr +import Std.Data.RBMap /-! The top-down analyzer is an optional preprocessor to the delaborator that aims @@ -13,15 +21,6 @@ can still not be re-elaborated correctly, and it may also add many annotations that are not strictly necessary. -/ -import Lean.Meta -import Lean.Util.FindMVar -import Lean.Util.FindLevelMVar -import Lean.Util.CollectLevelParams -import Lean.Util.ReplaceLevel -import Lean.PrettyPrinter.Delaborator.Options -import Lean.PrettyPrinter.Delaborator.SubExpr -import Std.Data.RBMap - namespace Lean open Lean.Meta diff --git a/stage0/src/Lean/PrettyPrinter/Formatter.lean b/stage0/src/Lean/PrettyPrinter/Formatter.lean index ad0ae82ce6..bc424cc20b 100644 --- a/stage0/src/Lean/PrettyPrinter/Formatter.lean +++ b/stage0/src/Lean/PrettyPrinter/Formatter.lean @@ -3,6 +3,11 @@ Copyright (c) 2020 Sebastian Ullrich. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Sebastian Ullrich -/ +import Lean.CoreM +import Lean.Parser.Extension +import Lean.KeyedDeclsAttribute +import Lean.ParserCompiler.Attribute +import Lean.PrettyPrinter.Basic /-! The formatter turns a `Syntax` tree into a `Format` object, inserting both mandatory whitespace (to separate adjacent @@ -13,12 +18,6 @@ parser-specific handlers registered via attributes. The traversal is right-to-le already know the text following it and can decide whether or not whitespace between the two is necessary. -/ -import Lean.CoreM -import Lean.Parser.Extension -import Lean.KeyedDeclsAttribute -import Lean.ParserCompiler.Attribute -import Lean.PrettyPrinter.Basic - namespace Lean namespace PrettyPrinter namespace Formatter diff --git a/stage0/src/Lean/PrettyPrinter/Parenthesizer.lean b/stage0/src/Lean/PrettyPrinter/Parenthesizer.lean index 84228d1ab0..77a2346945 100644 --- a/stage0/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/stage0/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -3,6 +3,12 @@ Copyright (c) 2020 Sebastian Ullrich. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Sebastian Ullrich -/ +import Lean.CoreM +import Lean.KeyedDeclsAttribute +import Lean.Parser.Extension +import Lean.ParserCompiler.Attribute +import Lean.PrettyPrinter.Basic + /-! The parenthesizer inserts parentheses into a `Syntax` object where syntactically necessary, usually as an intermediary @@ -71,12 +77,6 @@ node). -/ -import Lean.CoreM -import Lean.KeyedDeclsAttribute -import Lean.Parser.Extension -import Lean.ParserCompiler.Attribute -import Lean.PrettyPrinter.Basic - namespace Lean namespace PrettyPrinter namespace Parenthesizer diff --git a/stage0/stdlib/Lean/Elab/BuiltinCommand.c b/stage0/stdlib/Lean/Elab/BuiltinCommand.c index 2278352a25..4ad2c6d384 100644 --- a/stage0/stdlib/Lean/Elab/BuiltinCommand.c +++ b/stage0/stdlib/Lean/Elab/BuiltinCommand.c @@ -1,6 +1,6 @@ // Lean compiler output // Module: Lean.Elab.BuiltinCommand -// Imports: Init Lean.Elab.Command Lean.Elab.Open +// Imports: Init Lean.DocString Lean.Elab.Command Lean.Elab.Open #include #if defined(__clang__) #pragma clang diagnostic ignored "-Wunused-parameter" @@ -17,6 +17,7 @@ lean_object* l_Lean_Elab_elabSetOption_setOption___at_Lean_Elab_Command_elabSetO lean_object* l_Lean_throwError___at_Lean_Elab_Command_elabSetOption___spec__2(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Command_elabVariable(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_resolveNamespace___at_Lean_Elab_Command_elabExport___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__8; lean_object* l_Lean_Elab_Command_elabEnd_match__1(lean_object*); lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_myMacro____x40_Init_Notation___hyg_72____spec__1(lean_object*, lean_object*); lean_object* l_Lean_KVMap_setBool(lean_object*, lean_object*, uint8_t); @@ -28,8 +29,8 @@ static lean_object* l_Lean_Elab_Command_elabCheckFailure___closed__2; size_t l_USize_add(size_t, size_t); static lean_object* l_Lean_Elab_Command_elabCheck___lambda__1___closed__1; static lean_object* l___regBuiltin_Lean_Elab_Command_elabSetOption___closed__4; +static lean_object* l_Lean_Elab_Command_elabModuleDoc___closed__4; lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabVariable___spec__3(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__4; lean_object* lean_erase_macro_scopes(lean_object*); lean_object* l_Lean_stringToMessageData(lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Command_elbChoice___closed__3; @@ -39,6 +40,7 @@ lean_object* l_List_head_x21___at_Lean_Elab_Command_instMonadOptionsCommandElabM lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabOpen___spec__13___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_throwError___at_Lean_Elab_Command_elabExport___spec__10___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_popScopes___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__4; extern lean_object* l_Lean_nullKind; lean_object* l_Lean_Elab_Command_withNamespace(lean_object*); lean_object* l_Lean_Elab_Command_liftTermElabM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -63,6 +65,7 @@ lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_BuiltinCommand_0_ lean_object* l_Array_anyMUnsafe_any___at___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_matchBinderNames___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_throwError___at_Lean_Elab_Command_elabExport___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Command_elabSetOption___closed__1; +static lean_object* l_Lean_Elab_Command_elabModuleDoc___closed__2; lean_object* l_Lean_Elab_Command_elabEval___rarg(lean_object*); lean_object* l_Lean_Elab_Command_failIfSucceeds_match__1___rarg(lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Command_elabEnd___lambda__1___closed__4; @@ -85,8 +88,8 @@ static lean_object* l___regBuiltin_Lean_Elab_Command_elabExport___closed__4; lean_object* l_Std_PersistentArray_mapM___at_Lean_MessageLog_errorsToWarnings___spec__1(lean_object*); static lean_object* l_Lean_Elab_Command_elabSection___closed__1; lean_object* l_Lean_throwUnknownConstant___at_Lean_Elab_Command_elabExport___spec__8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Elab_Command_elabNamespace___closed__7; static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_replaceBinderAnnotation___spec__2___lambda__2___closed__2; +static lean_object* l_Lean_Elab_Command_elabModuleDoc___closed__3; static lean_object* l_Lean_Elab_Command_elabEvalUnsafe___closed__7; lean_object* l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_replaceBinderAnnotation_match__1(lean_object*); lean_object* l_Lean_Elab_Command_hasNoErrorMessages___rarg___boxed(lean_object*, lean_object*); @@ -134,18 +137,23 @@ lean_object* lean_string_append(lean_object*, lean_object*); static lean_object* l_Lean_Elab_Command_elabEvalUnsafe___lambda__2___closed__1; uint8_t l_Array_isEqvAux___at___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_matchBinderNames___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Command_elabSynth___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Command_elabModuleDoc___closed__1; static lean_object* l___regBuiltin_Lean_Elab_Command_elabSynth___closed__5; lean_object* l_Lean_Elab_Command_elabEvalUnsafe___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Elab_Command_expandInCmd(lean_object*); +lean_object* lean_string_utf8_extract(lean_object*, lean_object*, lean_object*); lean_object* lean_add_alias(lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_typelessBinder_x3f___closed__6; lean_object* l_Lean_Elab_Command_failIfSucceeds(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_replaceBinderAnnotation___spec__2___lambda__2___closed__4; +static lean_object* l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__6; static lean_object* l___regBuiltin_Lean_Elab_Command_elabOpen___closed__5; static lean_object* l_Lean_resolveNamespace___at_Lean_Elab_Command_elabExport___spec__1___closed__2; lean_object* l_Lean_Elab_log___at_Lean_Elab_Command_runLinters___spec__3(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_OpenDecl_elabOpenDecl___at_Lean_Elab_Command_elabOpen___spec__1___closed__6; lean_object* l_Lean_Elab_Command_elabEvalUnsafe___lambda__8(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*); +static lean_object* l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__2; +lean_object* lean_string_utf8_byte_size(lean_object*); lean_object* l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_elabChoiceAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_checkAnonymousScope___boxed(lean_object*); lean_object* l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_popScopes___boxed(lean_object*, lean_object*, lean_object*, lean_object*); @@ -156,6 +164,7 @@ static lean_object* l_Lean_Elab_Command_failIfSucceeds___lambda__1___closed__2; uint8_t l_USize_decLt(size_t, size_t); lean_object* l_Lean_Elab_Command_elabOpen(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Command_elabOpen___closed__3; +lean_object* l_Lean_Elab_Command_elabModuleDoc___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Open_0__Lean_Elab_OpenDecl_elabOpenRenaming___at_Lean_Elab_Command_elabOpen___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Command_elabEval___rarg___closed__1; static lean_object* l_Lean_Elab_Command_elabSynth___closed__2; @@ -211,14 +220,15 @@ static lean_object* l___regBuiltin_Lean_Elab_Command_elabVariable___closed__2; lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_replaceBinderAnnotation___spec__2___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_nat_sub(lean_object*, lean_object*); lean_object* l_Lean_Elab_Command_elabEvalUnsafe(lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__6; lean_object* l_Lean_Option_get___at_Lean_initFn____x40_Lean_Util_PPExt___hyg_225____spec__1(lean_object*, lean_object*); static lean_object* l_Lean_Elab_Command_elabCheck___closed__2; uint8_t l_Array_anyMUnsafe_any___at___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_matchBinderNames___spec__4(lean_object*, lean_object*, size_t, size_t); lean_object* l_Lean_resolveGlobalConstCore___at_Lean_Elab_Command_elabExport___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Syntax_isStrLit_x3f(lean_object*); lean_object* l_Lean_Elab_Command_elabEvalUnsafe___lambda__1___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_Command_elabModuleDoc(lean_object*); static lean_object* l_Lean_Elab_elabSetOption_setOption___at_Lean_Elab_Command_elabSetOption___spec__3___closed__1; +static lean_object* l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__1; static lean_object* l_Lean_Elab_pushInfoLeaf___at_Lean_Elab_Command_elabEnd___spec__3___closed__2; static lean_object* l___regBuiltin_Lean_Elab_Command_elabOpen___closed__1; lean_object* l_Lean_KernelException_toMessageData(lean_object*, lean_object*); @@ -249,6 +259,7 @@ static lean_object* l___regBuiltin_Lean_Elab_Command_elabOpen___closed__4; static lean_object* l___regBuiltin_Lean_Elab_Command_elabOpen___closed__2; lean_object* l___regBuiltin_Lean_Elab_Command_elabSetOption(lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Command_elabInitQuot___closed__3; +static lean_object* l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__9; lean_object* l_Lean_Elab_Command_elabEvalUnsafe_match__1(lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Command_expandInCmd___closed__2; static lean_object* l___regBuiltin_Lean_Elab_Command_elabCheck___closed__2; @@ -264,7 +275,9 @@ lean_object* l_Lean_Elab_Command_getBracketedBinderIds(lean_object*); lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabUniverse___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_pushInfoLeaf___at_Lean_Elab_Command_elabEnd___spec__3___closed__1; uint8_t l_Array_contains___at_Lean_findField_x3f___spec__1(lean_object*, lean_object*); +static lean_object* l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__3; lean_object* l_Lean_evalConst___at_Lean_Elab_Term_evalExpr___spec__11___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__11; lean_object* l_Lean_Elab_Term_synthesizeSyntheticMVars_loop(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__2; lean_object* l_Lean_Elab_Command_elabEvalUnsafe___lambda__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -307,14 +320,13 @@ static lean_object* l___regBuiltin_Lean_Elab_Command_elabSynth___closed__1; static lean_object* l_Lean_Elab_Command_elabSynth___closed__1; lean_object* l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_replaceBinderAnnotation_match__3(lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Command_elabEnd___closed__2; +static lean_object* l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__10; static lean_object* l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_typelessBinder_x3f___closed__3; lean_object* l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_replaceBinderAnnotation___lambda__1(lean_object*, lean_object*); lean_object* l_Lean_Elab_Command_elabSetOption___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_replaceBinderAnnotation___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Elab_Command_elabCheck___lambda__1___closed__3; lean_object* l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_replaceBinderAnnotation(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_elabSetOption___at_Lean_Elab_Command_elabSetOption___spec__1___closed__1; -static lean_object* l_Lean_Elab_Command_elabNamespace___closed__4; static lean_object* l_Lean_Elab_Command_elabEnd___closed__2; lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_replaceBinderAnnotation___spec__2___lambda__3___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Command_elabCommand(lean_object*, lean_object*, lean_object*, lean_object*); @@ -351,6 +363,7 @@ lean_object* l_Lean_Elab_Command_hasNoErrorMessages___rarg(lean_object*, lean_ob static lean_object* l_Lean_Elab_elabSetOption___at_Lean_Elab_Command_elabSetOption___spec__1___closed__2; static lean_object* l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_matchBinderNames___closed__2; static lean_object* l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_typelessBinder_x3f___closed__2; +lean_object* l_Lean_PersistentEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Command_elabEval___closed__2; lean_object* l___regBuiltin_Lean_Elab_Command_elabEnd(lean_object*); static lean_object* l_Lean_Elab_Command_elabReduce___lambda__1___closed__1; @@ -378,19 +391,21 @@ static lean_object* l___regBuiltin_Lean_Elab_Command_elabCheck___closed__1; lean_object* l_Lean_Elab_Command_elabEvalUnsafe_match__4(lean_object*); lean_object* l_Lean_Meta_synthInstance(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_addScopes___closed__1; -static lean_object* l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__5; static lean_object* l___regBuiltin_Lean_Elab_Command_elabCheckFailure___closed__3; lean_object* l_Std_PersistentArray_push___rarg(lean_object*, lean_object*); uint8_t l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_checkEndHeader(lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Command_elabSection___closed__2; +extern lean_object* l___private_Lean_DocString_0__Lean_moduleDocExt; static lean_object* l_Lean_Elab_Command_elabExport___closed__2; lean_object* l_Lean_Syntax_getSepArgs(lean_object*); static lean_object* l_Lean_Elab_Command_elabReduce___lambda__1___closed__2; lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabOpen___spec__12(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_popScopes___spec__2(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__13; extern lean_object* l_Lean_Elab_macroAttribute; lean_object* l_Lean_throwError___at_Lean_Elab_Command_elabExport___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_replaceBinderAnnotation___spec__2(lean_object*, uint8_t, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__12; lean_object* l_Lean_Elab_logException___at_Lean_Elab_Command_runLinters___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__3; lean_object* l_Lean_Elab_Command_elabEvalUnsafe___lambda__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -423,6 +438,7 @@ static lean_object* l_Lean_Elab_Command_elabEnd___closed__1; lean_object* l_Lean_resolveGlobalName___at_Lean_Elab_Command_elabExport___spec__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Environment_registerNamespace(lean_object*, lean_object*); static lean_object* l_Lean_resolveGlobalConstNoOverloadCore___at_Lean_Elab_Command_elabExport___spec__5___closed__2; +lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Command_elabModuleDoc___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabExport___spec__12___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Std_Range_forIn_loop___at___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_popScopes___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Command_elabVariable___closed__2; @@ -455,7 +471,6 @@ lean_object* l_Lean_Elab_Command_expandInCmd___boxed(lean_object*, lean_object*, lean_object* l___regBuiltin_Lean_Elab_Command_elabNamespace(lean_object*); lean_object* l_Lean_Elab_Command_elabEvalUnsafe___lambda__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* l_Lean_Elab_Command_elabVariable___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Elab_Command_elabNamespace___closed__8; lean_object* l___private_Lean_Elab_Open_0__Lean_Elab_OpenDecl_elabOpenHiding___at_Lean_Elab_Command_elabOpen___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Command_expandInCmd___closed__1; static lean_object* l_Lean_Elab_Command_elabVariable___lambda__2___closed__1; @@ -468,6 +483,7 @@ static lean_object* l___regBuiltin_Lean_Elab_Command_elabInitQuot___closed__1; static lean_object* l_Lean_Elab_Command_elabCheckFailure___closed__3; lean_object* l_Lean_Meta_instantiateMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Command_elabEvalUnsafe___lambda__4___closed__1; +static lean_object* l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__5; lean_object* l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_replaceBinderAnnotation_match__4(lean_object*); lean_object* l_Lean_throwError___at___private_Lean_Elab_Command_0__Lean_Elab_Command_elabCommandUsing___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*); @@ -480,10 +496,13 @@ lean_object* l_Lean_Elab_Command_elabVariable___lambda__1___boxed(lean_object*, lean_object* l_Lean_Elab_Term_withoutAutoBoundImplicit___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_DataValue_sameCtor(lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabBinders___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__14; lean_object* l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_elabChoiceAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Command_getBracketedBinderIds___spec__1(size_t, size_t, lean_object*); lean_object* l_Lean_Elab_Command_getScopes___rarg(lean_object*, lean_object*); +lean_object* l_Lean_Elab_Command_elabModuleDoc(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_replaceBinderAnnotation___spec__2___lambda__2___closed__3; +lean_object* l_Lean_indentD(lean_object*); extern lean_object* l_Lean_Elab_unsupportedSyntaxExceptionId; lean_object* l___private_Lean_Elab_Open_0__Lean_Elab_OpenDecl_addOpenDecl___at_Lean_Elab_Command_elabOpen___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabVariable___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -497,16 +516,15 @@ lean_object* l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_checkEndH lean_object* l_Lean_Elab_Command_elabSynth___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Command_elabEvalUnsafe___closed__5; static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_replaceBinderAnnotation___spec__2___lambda__2___closed__10; -static lean_object* l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_checkAnonymousScope_match__1___rarg___closed__1; static lean_object* l_Lean_Elab_OpenDecl_elabOpenDecl___at_Lean_Elab_Command_elabOpen___spec__1___closed__5; lean_object* l_Lean_Elab_Command_elabVariable___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Command_elabEvalUnsafe___closed__3; -static lean_object* l_Lean_Elab_Command_elabNamespace___closed__6; static lean_object* l_Lean_Elab_Command_elabEvalUnsafe___closed__6; lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_addScope___spec__2(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Command_expandInCmd___closed__3; uint8_t l_Std_PersistentArray_anyM___at_Lean_MessageLog_hasErrors___spec__1(lean_object*); lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_replaceBinderAnnotation___spec__2___lambda__3(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_Command_elabModuleDoc_match__1(lean_object*); static lean_object* l_Lean_Elab_Command_elabEnd___lambda__1___closed__2; lean_object* l_Lean_throwError___at_Lean_Elab_Command_elabSetOption___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*); @@ -518,6 +536,7 @@ static lean_object* l___regBuiltin_Lean_Elab_Command_elabUniverse___closed__1; lean_object* l_Lean_Elab_OpenDecl_elabOpenDecl___at_Lean_Elab_Command_elabOpen___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Command_elabCheck_match__1(lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Command_elabUniverse___closed__2; +lean_object* l_Lean_Elab_Command_elabModuleDoc_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Command_getScope___rarg(lean_object*, lean_object*); lean_object* l_Lean_Elab_elabSetOption_setOption___at_Lean_Elab_Command_elabSetOption___spec__3___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Command_elabEnd___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -531,14 +550,12 @@ lean_object* l_Lean_Elab_Command_elabVariable___lambda__2(lean_object*, lean_obj lean_object* l___regBuiltin_Lean_Elab_Command_elabUniverse(lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Command_elabVariable___closed__3; lean_object* l_Lean_Elab_Command_hasNoErrorMessages___boxed(lean_object*); -static lean_object* l_Lean_Elab_Command_elabNamespace___closed__5; lean_object* l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_addScope___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_replaceBinderAnnotation___spec__2___lambda__2___closed__6; lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_replaceBinderAnnotation___spec__2___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Open_0__Lean_Elab_OpenDecl_elabOpenOnly___at_Lean_Elab_Command_elabOpen___spec__8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Command_elabInitQuot_match__1(lean_object*); lean_object* l_Lean_Elab_Term_withAutoBoundImplicit___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Elab_Command_elabNamespace___closed__3; static lean_object* l_Lean_Elab_Command_elabSynth___closed__3; static lean_object* l___regBuiltin_Lean_Elab_Command_elabExport___closed__5; lean_object* l_Lean_mkConst(lean_object*, lean_object*); @@ -556,6 +573,7 @@ lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_BuiltinCommand_0_ lean_object* l_Lean_ScopedEnvExtension_activateScoped___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabOpen___spec__7(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Command_elabEnd___lambda__1___closed__3; +static lean_object* l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__7; lean_object* l_Lean_throwError___at___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_matchBinderNames___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_throwError___at___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_matchBinderNames___spec__2(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Command_elabReduce___closed__2; @@ -577,8 +595,420 @@ static lean_object* l___regBuiltin_Lean_Elab_Command_elabExport___closed__3; lean_object* l_Lean_Elab_getBetterRef(lean_object*, lean_object*); uint8_t lean_string_dec_eq(lean_object*, lean_object*); uint8_t lean_nat_dec_lt(lean_object*, lean_object*); +lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Command_elabModuleDoc___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_add_decl(lean_object*, lean_object*); lean_object* l_Lean_Elab_addCompletionInfo___at_Lean_Elab_Command_elabEnd___spec__2(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_Command_elabModuleDoc_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +if (lean_obj_tag(x_1) == 2) +{ +lean_object* x_4; lean_object* x_5; lean_object* x_6; +lean_dec(x_3); +x_4 = lean_ctor_get(x_1, 0); +lean_inc(x_4); +x_5 = lean_ctor_get(x_1, 1); +lean_inc(x_5); +lean_dec(x_1); +x_6 = lean_apply_2(x_2, x_4, x_5); +return x_6; +} +else +{ +lean_object* x_7; +lean_dec(x_2); +x_7 = lean_apply_1(x_3, x_1); +return x_7; +} +} +} +lean_object* l_Lean_Elab_Command_elabModuleDoc_match__1(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Command_elabModuleDoc_match__1___rarg), 3, 0); +return x_2; +} +} +lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Command_elabModuleDoc___spec__1(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; lean_object* x_9; uint8_t x_10; +x_6 = l_Lean_Elab_Command_getRef(x_3, x_4, x_5); +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 = l_Lean_replaceRef(x_1, x_7); +lean_dec(x_7); +x_10 = !lean_is_exclusive(x_3); +if (x_10 == 0) +{ +lean_object* x_11; lean_object* x_12; +x_11 = lean_ctor_get(x_3, 6); +lean_dec(x_11); +lean_ctor_set(x_3, 6, x_9); +x_12 = l_Lean_throwError___at___private_Lean_Elab_Command_0__Lean_Elab_Command_elabCommandUsing___spec__1(x_2, x_3, x_4, x_8); +return x_12; +} +else +{ +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; +x_13 = lean_ctor_get(x_3, 0); +x_14 = lean_ctor_get(x_3, 1); +x_15 = lean_ctor_get(x_3, 2); +x_16 = lean_ctor_get(x_3, 3); +x_17 = lean_ctor_get(x_3, 4); +x_18 = lean_ctor_get(x_3, 5); +lean_inc(x_18); +lean_inc(x_17); +lean_inc(x_16); +lean_inc(x_15); +lean_inc(x_14); +lean_inc(x_13); +lean_dec(x_3); +x_19 = lean_alloc_ctor(0, 7, 0); +lean_ctor_set(x_19, 0, x_13); +lean_ctor_set(x_19, 1, x_14); +lean_ctor_set(x_19, 2, x_15); +lean_ctor_set(x_19, 3, x_16); +lean_ctor_set(x_19, 4, x_17); +lean_ctor_set(x_19, 5, x_18); +lean_ctor_set(x_19, 6, x_9); +x_20 = l_Lean_throwError___at___private_Lean_Elab_Command_0__Lean_Elab_Command_elabCommandUsing___spec__1(x_2, x_19, x_4, x_8); +return x_20; +} +} +} +static lean_object* _init_l_Lean_Elab_Command_elabModuleDoc___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("unexpected module doc string"); +return x_1; +} +} +static lean_object* _init_l_Lean_Elab_Command_elabModuleDoc___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Elab_Command_elabModuleDoc___closed__1; +x_2 = l_Lean_stringToMessageData(x_1); +return x_2; +} +} +static lean_object* _init_l_Lean_Elab_Command_elabModuleDoc___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string(""); +return x_1; +} +} +static lean_object* _init_l_Lean_Elab_Command_elabModuleDoc___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Elab_Command_elabModuleDoc___closed__3; +x_2 = l_Lean_stringToMessageData(x_1); +return x_2; +} +} +lean_object* l_Lean_Elab_Command_elabModuleDoc(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +lean_object* x_5; lean_object* x_6; +x_5 = lean_unsigned_to_nat(1u); +x_6 = l_Lean_Syntax_getArg(x_1, x_5); +if (lean_obj_tag(x_6) == 2) +{ +lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; uint8_t x_16; +lean_dec(x_2); +x_7 = lean_ctor_get(x_6, 1); +lean_inc(x_7); +lean_dec(x_6); +x_8 = lean_string_utf8_byte_size(x_7); +x_9 = lean_unsigned_to_nat(2u); +x_10 = lean_nat_sub(x_8, x_9); +lean_dec(x_8); +x_11 = lean_unsigned_to_nat(0u); +x_12 = lean_string_utf8_extract(x_7, x_11, x_10); +lean_dec(x_10); +lean_dec(x_7); +x_13 = lean_st_ref_take(x_3, x_4); +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_is_exclusive(x_14); +if (x_16 == 0) +{ +lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; uint8_t x_21; +x_17 = lean_ctor_get(x_14, 0); +x_18 = l___private_Lean_DocString_0__Lean_moduleDocExt; +x_19 = l_Lean_PersistentEnvExtension_addEntry___rarg(x_18, x_17, x_12); +lean_ctor_set(x_14, 0, x_19); +x_20 = lean_st_ref_set(x_3, x_14, x_15); +lean_dec(x_3); +x_21 = !lean_is_exclusive(x_20); +if (x_21 == 0) +{ +lean_object* x_22; lean_object* x_23; +x_22 = lean_ctor_get(x_20, 0); +lean_dec(x_22); +x_23 = lean_box(0); +lean_ctor_set(x_20, 0, x_23); +return x_20; +} +else +{ +lean_object* x_24; lean_object* x_25; lean_object* x_26; +x_24 = lean_ctor_get(x_20, 1); +lean_inc(x_24); +lean_dec(x_20); +x_25 = lean_box(0); +x_26 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_26, 0, x_25); +lean_ctor_set(x_26, 1, x_24); +return x_26; +} +} +else +{ +lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; 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; lean_object* x_42; lean_object* x_43; +x_27 = lean_ctor_get(x_14, 0); +x_28 = lean_ctor_get(x_14, 1); +x_29 = lean_ctor_get(x_14, 2); +x_30 = lean_ctor_get(x_14, 3); +x_31 = lean_ctor_get(x_14, 4); +x_32 = lean_ctor_get(x_14, 5); +x_33 = lean_ctor_get(x_14, 6); +x_34 = lean_ctor_get(x_14, 7); +x_35 = lean_ctor_get(x_14, 8); +lean_inc(x_35); +lean_inc(x_34); +lean_inc(x_33); +lean_inc(x_32); +lean_inc(x_31); +lean_inc(x_30); +lean_inc(x_29); +lean_inc(x_28); +lean_inc(x_27); +lean_dec(x_14); +x_36 = l___private_Lean_DocString_0__Lean_moduleDocExt; +x_37 = l_Lean_PersistentEnvExtension_addEntry___rarg(x_36, x_27, x_12); +x_38 = lean_alloc_ctor(0, 9, 0); +lean_ctor_set(x_38, 0, x_37); +lean_ctor_set(x_38, 1, x_28); +lean_ctor_set(x_38, 2, x_29); +lean_ctor_set(x_38, 3, x_30); +lean_ctor_set(x_38, 4, x_31); +lean_ctor_set(x_38, 5, x_32); +lean_ctor_set(x_38, 6, x_33); +lean_ctor_set(x_38, 7, x_34); +lean_ctor_set(x_38, 8, x_35); +x_39 = lean_st_ref_set(x_3, x_38, x_15); +lean_dec(x_3); +x_40 = lean_ctor_get(x_39, 1); +lean_inc(x_40); +if (lean_is_exclusive(x_39)) { + lean_ctor_release(x_39, 0); + lean_ctor_release(x_39, 1); + x_41 = x_39; +} else { + lean_dec_ref(x_39); + x_41 = lean_box(0); +} +x_42 = lean_box(0); +if (lean_is_scalar(x_41)) { + x_43 = lean_alloc_ctor(0, 2, 0); +} else { + x_43 = x_41; +} +lean_ctor_set(x_43, 0, x_42); +lean_ctor_set(x_43, 1, x_40); +return x_43; +} +} +else +{ +lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; +x_44 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_44, 0, x_6); +x_45 = l_Lean_indentD(x_44); +x_46 = l_Lean_Elab_Command_elabModuleDoc___closed__2; +x_47 = lean_alloc_ctor(10, 2, 0); +lean_ctor_set(x_47, 0, x_46); +lean_ctor_set(x_47, 1, x_45); +x_48 = l_Lean_Elab_Command_elabModuleDoc___closed__4; +x_49 = lean_alloc_ctor(10, 2, 0); +lean_ctor_set(x_49, 0, x_47); +lean_ctor_set(x_49, 1, x_48); +x_50 = l_Lean_throwErrorAt___at_Lean_Elab_Command_elabModuleDoc___spec__1(x_1, x_49, x_2, x_3, x_4); +lean_dec(x_3); +return x_50; +} +} +} +lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Command_elabModuleDoc___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { +_start: +{ +lean_object* x_6; +x_6 = l_Lean_throwErrorAt___at_Lean_Elab_Command_elabModuleDoc___spec__1(x_1, x_2, x_3, x_4, x_5); +lean_dec(x_4); +lean_dec(x_1); +return x_6; +} +} +lean_object* l_Lean_Elab_Command_elabModuleDoc___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +lean_object* x_5; +x_5 = l_Lean_Elab_Command_elabModuleDoc(x_1, x_2, x_3, x_4); +lean_dec(x_1); +return x_5; +} +} +static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("Lean"); +return x_1; +} +} +static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__1; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("Parser"); +return x_1; +} +} +static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__2; +x_2 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__3; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__5() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("Command"); +return x_1; +} +} +static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__6() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__4; +x_2 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__5; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__7() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("moduleDoc"); +return x_1; +} +} +static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__8() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__6; +x_2 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__7; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__9() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("Elab"); +return x_1; +} +} +static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__10() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__2; +x_2 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__9; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__11() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__10; +x_2 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__5; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__12() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("elabModuleDoc"); +return x_1; +} +} +static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__13() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__11; +x_2 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__12; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__14() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Command_elabModuleDoc___boxed), 4, 0); +return x_1; +} +} +lean_object* l___regBuiltin_Lean_Elab_Command_elabModuleDoc(lean_object* x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; +x_2 = l_Lean_Elab_Command_commandElabAttribute; +x_3 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__8; +x_4 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__13; +x_5 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__14; +x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1); +return x_6; +} +} lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_addScope___spec__2(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) { _start: { @@ -1816,14 +2246,6 @@ lean_dec(x_2); return x_5; } } -static lean_object* _init_l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_checkAnonymousScope_match__1___rarg___closed__1() { -_start: -{ -lean_object* x_1; -x_1 = lean_mk_string(""); -return x_1; -} -} lean_object* l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_checkAnonymousScope_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { @@ -1856,7 +2278,7 @@ lean_inc(x_12); x_13 = lean_ctor_get(x_5, 6); lean_inc(x_13); lean_dec(x_5); -x_14 = l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_checkAnonymousScope_match__1___rarg___closed__1; +x_14 = l_Lean_Elab_Command_elabModuleDoc___closed__3; x_15 = lean_string_dec_eq(x_7, x_14); lean_dec(x_7); if (x_15 == 0) @@ -1906,7 +2328,7 @@ else lean_object* x_3; lean_object* x_4; lean_object* x_5; uint8_t x_6; x_3 = lean_ctor_get(x_1, 0); x_4 = lean_ctor_get(x_3, 0); -x_5 = l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_checkAnonymousScope_match__1___rarg___closed__1; +x_5 = l_Lean_Elab_Command_elabModuleDoc___closed__3; x_6 = lean_string_dec_eq(x_4, x_5); return x_6; } @@ -2094,7 +2516,7 @@ static lean_object* _init_l_Lean_Elab_Command_elabNamespace___closed__1() { _start: { lean_object* x_1; -x_1 = lean_mk_string("Lean"); +x_1 = lean_mk_string("namespace"); return x_1; } } @@ -2102,71 +2524,17 @@ static lean_object* _init_l_Lean_Elab_Command_elabNamespace___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__6; x_2 = l_Lean_Elab_Command_elabNamespace___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Elab_Command_elabNamespace___closed__3() { -_start: -{ -lean_object* x_1; -x_1 = lean_mk_string("Parser"); -return x_1; -} -} -static lean_object* _init_l_Lean_Elab_Command_elabNamespace___closed__4() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Command_elabNamespace___closed__2; -x_2 = l_Lean_Elab_Command_elabNamespace___closed__3; -x_3 = lean_name_mk_string(x_1, x_2); -return x_3; -} -} -static lean_object* _init_l_Lean_Elab_Command_elabNamespace___closed__5() { -_start: -{ -lean_object* x_1; -x_1 = lean_mk_string("Command"); -return x_1; -} -} -static lean_object* _init_l_Lean_Elab_Command_elabNamespace___closed__6() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Command_elabNamespace___closed__4; -x_2 = l_Lean_Elab_Command_elabNamespace___closed__5; -x_3 = lean_name_mk_string(x_1, x_2); -return x_3; -} -} -static lean_object* _init_l_Lean_Elab_Command_elabNamespace___closed__7() { -_start: -{ -lean_object* x_1; -x_1 = lean_mk_string("namespace"); -return x_1; -} -} -static lean_object* _init_l_Lean_Elab_Command_elabNamespace___closed__8() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Command_elabNamespace___closed__6; -x_2 = l_Lean_Elab_Command_elabNamespace___closed__7; -x_3 = lean_name_mk_string(x_1, x_2); -return x_3; -} -} lean_object* l_Lean_Elab_Command_elabNamespace(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { lean_object* x_5; uint8_t x_6; -x_5 = l_Lean_Elab_Command_elabNamespace___closed__8; +x_5 = l_Lean_Elab_Command_elabNamespace___closed__2; lean_inc(x_1); x_6 = l_Lean_Syntax_isOfKind(x_1, x_5); if (x_6 == 0) @@ -2214,7 +2582,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabNamespace___close _start: { lean_object* x_1; -x_1 = lean_mk_string("Elab"); +x_1 = lean_mk_string("elabNamespace"); return x_1; } } @@ -2222,7 +2590,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabNamespace___close _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Command_elabNamespace___closed__2; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__11; x_2 = l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -2231,34 +2599,6 @@ return x_3; static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__3() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__2; -x_2 = l_Lean_Elab_Command_elabNamespace___closed__5; -x_3 = lean_name_mk_string(x_1, x_2); -return x_3; -} -} -static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__4() { -_start: -{ -lean_object* x_1; -x_1 = lean_mk_string("elabNamespace"); -return x_1; -} -} -static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__5() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__3; -x_2 = l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__4; -x_3 = lean_name_mk_string(x_1, x_2); -return x_3; -} -} -static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__6() { -_start: -{ lean_object* x_1; x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Command_elabNamespace___boxed), 4, 0); return x_1; @@ -2269,9 +2609,9 @@ _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_2 = l_Lean_Elab_Command_commandElabAttribute; -x_3 = l_Lean_Elab_Command_elabNamespace___closed__8; -x_4 = l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__5; -x_5 = l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__6; +x_3 = l_Lean_Elab_Command_elabNamespace___closed__2; +x_4 = l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__2; +x_5 = l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__3; x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1); return x_6; } @@ -2288,7 +2628,7 @@ static lean_object* _init_l_Lean_Elab_Command_elabSection___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Command_elabNamespace___closed__6; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__6; x_2 = l_Lean_Elab_Command_elabSection___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -2361,7 +2701,7 @@ x_18 = lean_ctor_get(x_16, 2); lean_inc(x_18); lean_dec(x_16); x_19 = 0; -x_20 = l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_checkAnonymousScope_match__1___rarg___closed__1; +x_20 = l_Lean_Elab_Command_elabModuleDoc___closed__3; x_21 = l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_addScope(x_19, x_20, x_18, x_2, x_3, x_17); return x_21; } @@ -2417,7 +2757,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabSection___closed_ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__3; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__11; x_2 = l___regBuiltin_Lean_Elab_Command_elabSection___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -3257,7 +3597,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabEnd___closed__2() _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Command_elabNamespace___closed__6; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__6; x_2 = l___regBuiltin_Lean_Elab_Command_elabEnd___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -3275,7 +3615,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabEnd___closed__4() _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__3; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__11; x_2 = l___regBuiltin_Lean_Elab_Command_elabEnd___closed__3; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -3495,7 +3835,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elbChoice___closed__4 _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__3; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__11; x_2 = l___regBuiltin_Lean_Elab_Command_elbChoice___closed__3; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -3666,7 +4006,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabUniverse___closed _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Command_elabNamespace___closed__6; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__6; x_2 = l___regBuiltin_Lean_Elab_Command_elabUniverse___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -3684,7 +4024,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabUniverse___closed _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__3; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__11; x_2 = l___regBuiltin_Lean_Elab_Command_elabUniverse___closed__3; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -3832,7 +4172,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabInitQuot___closed _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Command_elabNamespace___closed__6; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__6; x_2 = l___regBuiltin_Lean_Elab_Command_elabInitQuot___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -3850,7 +4190,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabInitQuot___closed _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__3; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__11; x_2 = l___regBuiltin_Lean_Elab_Command_elabInitQuot___closed__3; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -4358,7 +4698,7 @@ x_16 = l_List_map___at_Lean_resolveGlobalConstNoOverloadCore___spec__1(x_9, x_7) x_17 = l_List_toString___at_Lean_resolveGlobalConstNoOverloadCore___spec__2(x_16); x_18 = lean_string_append(x_15, x_17); lean_dec(x_17); -x_19 = l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_checkAnonymousScope_match__1___rarg___closed__1; +x_19 = l_Lean_Elab_Command_elabModuleDoc___closed__3; x_20 = lean_string_append(x_18, x_19); x_21 = lean_alloc_ctor(2, 1, 0); lean_ctor_set(x_21, 0, x_20); @@ -4429,7 +4769,7 @@ x_39 = l_List_map___at_Lean_resolveGlobalConstNoOverloadCore___spec__1(x_32, x_7 x_40 = l_List_toString___at_Lean_resolveGlobalConstNoOverloadCore___spec__2(x_39); x_41 = lean_string_append(x_38, x_40); lean_dec(x_40); -x_42 = l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_checkAnonymousScope_match__1___rarg___closed__1; +x_42 = l_Lean_Elab_Command_elabModuleDoc___closed__3; x_43 = lean_string_append(x_41, x_42); x_44 = lean_alloc_ctor(2, 1, 0); lean_ctor_set(x_44, 0, x_43); @@ -5236,7 +5576,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabExport___closed__ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Command_elabNamespace___closed__6; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__6; x_2 = l___regBuiltin_Lean_Elab_Command_elabExport___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -5254,7 +5594,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabExport___closed__ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__3; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__11; x_2 = l___regBuiltin_Lean_Elab_Command_elabExport___closed__3; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -6355,7 +6695,7 @@ static lean_object* _init_l_Lean_Elab_OpenDecl_elabOpenDecl___at_Lean_Elab_Comma _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Command_elabNamespace___closed__6; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__6; x_2 = l_Lean_Elab_OpenDecl_elabOpenDecl___at_Lean_Elab_Command_elabOpen___spec__1___closed__2; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -6373,7 +6713,7 @@ static lean_object* _init_l_Lean_Elab_OpenDecl_elabOpenDecl___at_Lean_Elab_Comma _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Command_elabNamespace___closed__6; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__6; x_2 = l_Lean_Elab_OpenDecl_elabOpenDecl___at_Lean_Elab_Command_elabOpen___spec__1___closed__4; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -6391,7 +6731,7 @@ static lean_object* _init_l_Lean_Elab_OpenDecl_elabOpenDecl___at_Lean_Elab_Comma _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Command_elabNamespace___closed__6; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__6; x_2 = l_Lean_Elab_OpenDecl_elabOpenDecl___at_Lean_Elab_Command_elabOpen___spec__1___closed__6; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -7098,7 +7438,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabOpen___closed__2( _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Command_elabNamespace___closed__6; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__6; x_2 = l___regBuiltin_Lean_Elab_Command_elabOpen___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -7116,7 +7456,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabOpen___closed__4( _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__3; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__11; x_2 = l___regBuiltin_Lean_Elab_Command_elabOpen___closed__3; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -7154,7 +7494,7 @@ static lean_object* _init_l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Comm _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Command_elabNamespace___closed__4; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__4; x_2 = l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_typelessBinder_x3f___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -9574,7 +9914,7 @@ static lean_object* _init_l_Lean_Elab_Command_elabVariable___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Command_elabNamespace___closed__6; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__6; x_2 = l_Lean_Elab_Command_elabVariable___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -9783,7 +10123,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabVariable___closed _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__3; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__11; x_2 = l___regBuiltin_Lean_Elab_Command_elabVariable___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -9833,25 +10173,16 @@ return x_2; static lean_object* _init_l_Lean_Elab_Command_elabCheck___lambda__1___closed__1() { _start: { -lean_object* x_1; lean_object* x_2; -x_1 = l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_checkAnonymousScope_match__1___rarg___closed__1; -x_2 = l_Lean_stringToMessageData(x_1); -return x_2; -} -} -static lean_object* _init_l_Lean_Elab_Command_elabCheck___lambda__1___closed__2() { -_start: -{ lean_object* x_1; x_1 = lean_mk_string(" : "); return x_1; } } -static lean_object* _init_l_Lean_Elab_Command_elabCheck___lambda__1___closed__3() { +static lean_object* _init_l_Lean_Elab_Command_elabCheck___lambda__1___closed__2() { _start: { lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Elab_Command_elabCheck___lambda__1___closed__2; +x_1 = l_Lean_Elab_Command_elabCheck___lambda__1___closed__1; x_2 = l_Lean_stringToMessageData(x_1); return x_2; } @@ -9936,11 +10267,11 @@ lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean lean_free_object(x_27); x_32 = lean_alloc_ctor(2, 1, 0); lean_ctor_set(x_32, 0, x_26); -x_33 = l_Lean_Elab_Command_elabCheck___lambda__1___closed__1; +x_33 = l_Lean_Elab_Command_elabModuleDoc___closed__4; x_34 = lean_alloc_ctor(10, 2, 0); lean_ctor_set(x_34, 0, x_33); lean_ctor_set(x_34, 1, x_32); -x_35 = l_Lean_Elab_Command_elabCheck___lambda__1___closed__3; +x_35 = l_Lean_Elab_Command_elabCheck___lambda__1___closed__2; x_36 = lean_alloc_ctor(10, 2, 0); lean_ctor_set(x_36, 0, x_34); lean_ctor_set(x_36, 1, x_35); @@ -9990,11 +10321,11 @@ if (x_44 == 0) lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; uint8_t x_53; lean_object* x_54; x_45 = lean_alloc_ctor(2, 1, 0); lean_ctor_set(x_45, 0, x_26); -x_46 = l_Lean_Elab_Command_elabCheck___lambda__1___closed__1; +x_46 = l_Lean_Elab_Command_elabModuleDoc___closed__4; x_47 = lean_alloc_ctor(10, 2, 0); lean_ctor_set(x_47, 0, x_46); lean_ctor_set(x_47, 1, x_45); -x_48 = l_Lean_Elab_Command_elabCheck___lambda__1___closed__3; +x_48 = l_Lean_Elab_Command_elabCheck___lambda__1___closed__2; x_49 = lean_alloc_ctor(10, 2, 0); lean_ctor_set(x_49, 0, x_47); lean_ctor_set(x_49, 1, x_48); @@ -10390,7 +10721,7 @@ static lean_object* _init_l_Lean_Elab_Command_elabCheck___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Command_elabNamespace___closed__6; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__6; x_2 = l_Lean_Elab_Command_elabCheck___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -10581,7 +10912,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabCheck___closed__2 _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__3; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__11; x_2 = l___regBuiltin_Lean_Elab_Command_elabCheck___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -11317,7 +11648,7 @@ static lean_object* _init_l_Lean_Elab_Command_elabReduce___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Command_elabNamespace___closed__6; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__6; x_2 = l_Lean_Elab_Command_elabReduce___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -11480,7 +11811,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabReduce___closed__ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__3; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__11; x_2 = l___regBuiltin_Lean_Elab_Command_elabReduce___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -12397,7 +12728,7 @@ static lean_object* _init_l_Lean_Elab_Command_elabCheckFailure___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Command_elabNamespace___closed__6; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__6; x_2 = l_Lean_Elab_Command_elabCheckFailure___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -12477,7 +12808,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabCheckFailure___cl _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__3; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__11; x_2 = l___regBuiltin_Lean_Elab_Command_elabCheckFailure___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -14314,7 +14645,7 @@ static lean_object* _init_l_Lean_Elab_Command_elabEvalUnsafe___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Command_elabNamespace___closed__6; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__6; x_2 = l_Lean_Elab_Command_elabEvalUnsafe___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -14360,7 +14691,7 @@ static lean_object* _init_l_Lean_Elab_Command_elabEvalUnsafe___closed__7() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Command_elabNamespace___closed__2; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__2; x_2 = l_Lean_Elab_Command_elabEvalUnsafe___closed__6; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -14411,7 +14742,7 @@ lean_inc(x_20); lean_dec(x_18); x_21 = lean_ctor_get(x_19, 5); lean_inc(x_21); -x_22 = l_Lean_Elab_Command_elabNamespace___closed__2; +x_22 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__2; x_23 = l_Lean_Elab_Command_elabEvalUnsafe___closed__4; x_24 = lean_alloc_closure((void*)(l_Lean_Elab_Command_elabEvalUnsafe___lambda__3___boxed), 13, 5); lean_closure_set(x_24, 0, x_19); @@ -14439,7 +14770,7 @@ lean_inc(x_31); lean_dec(x_29); x_32 = lean_ctor_get(x_30, 5); lean_inc(x_32); -x_33 = l_Lean_Elab_Command_elabNamespace___closed__2; +x_33 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__2; x_34 = l_Lean_Elab_Command_elabEvalUnsafe___closed__4; x_35 = lean_alloc_closure((void*)(l_Lean_Elab_Command_elabEvalUnsafe___lambda__8___boxed), 13, 5); lean_closure_set(x_35, 0, x_30); @@ -14588,7 +14919,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabEval___closed__2( _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__3; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__11; x_2 = l___regBuiltin_Lean_Elab_Command_elabEval___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -15200,7 +15531,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabSynth___closed__2 _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Command_elabNamespace___closed__6; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__6; x_2 = l___regBuiltin_Lean_Elab_Command_elabSynth___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -15218,7 +15549,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabSynth___closed__4 _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__3; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__11; x_2 = l___regBuiltin_Lean_Elab_Command_elabSynth___closed__3; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -15574,7 +15905,7 @@ x_23 = l_Lean_Elab_elabSetOption___at_Lean_Elab_Command_elabSetOption___spec__1_ x_24 = lean_alloc_ctor(10, 2, 0); lean_ctor_set(x_24, 0, x_23); lean_ctor_set(x_24, 1, x_22); -x_25 = l_Lean_Elab_Command_elabCheck___lambda__1___closed__1; +x_25 = l_Lean_Elab_Command_elabModuleDoc___closed__4; x_26 = lean_alloc_ctor(10, 2, 0); lean_ctor_set(x_26, 0, x_24); lean_ctor_set(x_26, 1, x_25); @@ -15623,7 +15954,7 @@ x_39 = l_Lean_Elab_elabSetOption___at_Lean_Elab_Command_elabSetOption___spec__1_ x_40 = lean_alloc_ctor(10, 2, 0); lean_ctor_set(x_40, 0, x_39); lean_ctor_set(x_40, 1, x_38); -x_41 = l_Lean_Elab_Command_elabCheck___lambda__1___closed__1; +x_41 = l_Lean_Elab_Command_elabModuleDoc___closed__4; x_42 = lean_alloc_ctor(10, 2, 0); lean_ctor_set(x_42, 0, x_40); lean_ctor_set(x_42, 1, x_41); @@ -15856,7 +16187,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabSetOption___close _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Command_elabNamespace___closed__6; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__6; x_2 = l___regBuiltin_Lean_Elab_Command_elabSetOption___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -15874,7 +16205,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabSetOption___close _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__3; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__11; x_2 = l___regBuiltin_Lean_Elab_Command_elabSetOption___closed__3; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -16029,7 +16360,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Command_expandInCmd___closed_ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Command_elabNamespace___closed__6; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__6; x_2 = l___regBuiltin_Lean_Elab_Command_expandInCmd___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -16047,7 +16378,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Command_expandInCmd___closed_ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__3; +x_1 = l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__11; x_2 = l___regBuiltin_Lean_Elab_Command_expandInCmd___closed__3; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -16074,6 +16405,7 @@ return x_6; } } lean_object* initialize_Init(lean_object*); +lean_object* initialize_Lean_DocString(lean_object*); lean_object* initialize_Lean_Elab_Command(lean_object*); lean_object* initialize_Lean_Elab_Open(lean_object*); static bool _G_initialized = false; @@ -16084,48 +16416,70 @@ _G_initialized = true; res = initialize_Init(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); +res = initialize_Lean_DocString(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); res = initialize_Lean_Elab_Command(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); res = initialize_Lean_Elab_Open(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); +l_Lean_Elab_Command_elabModuleDoc___closed__1 = _init_l_Lean_Elab_Command_elabModuleDoc___closed__1(); +lean_mark_persistent(l_Lean_Elab_Command_elabModuleDoc___closed__1); +l_Lean_Elab_Command_elabModuleDoc___closed__2 = _init_l_Lean_Elab_Command_elabModuleDoc___closed__2(); +lean_mark_persistent(l_Lean_Elab_Command_elabModuleDoc___closed__2); +l_Lean_Elab_Command_elabModuleDoc___closed__3 = _init_l_Lean_Elab_Command_elabModuleDoc___closed__3(); +lean_mark_persistent(l_Lean_Elab_Command_elabModuleDoc___closed__3); +l_Lean_Elab_Command_elabModuleDoc___closed__4 = _init_l_Lean_Elab_Command_elabModuleDoc___closed__4(); +lean_mark_persistent(l_Lean_Elab_Command_elabModuleDoc___closed__4); +l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__1 = _init_l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__1(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__1); +l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__2 = _init_l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__2(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__2); +l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__3 = _init_l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__3(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__3); +l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__4 = _init_l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__4(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__4); +l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__5 = _init_l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__5(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__5); +l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__6 = _init_l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__6(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__6); +l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__7 = _init_l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__7(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__7); +l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__8 = _init_l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__8(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__8); +l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__9 = _init_l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__9(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__9); +l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__10 = _init_l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__10(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__10); +l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__11 = _init_l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__11(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__11); +l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__12 = _init_l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__12(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__12); +l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__13 = _init_l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__13(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__13); +l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__14 = _init_l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__14(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabModuleDoc___closed__14); +res = l___regBuiltin_Lean_Elab_Command_elabModuleDoc(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_addScopes___closed__1 = _init_l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_addScopes___closed__1(); lean_mark_persistent(l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_addScopes___closed__1); l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_addScopes___closed__2 = _init_l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_addScopes___closed__2(); lean_mark_persistent(l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_addScopes___closed__2); -l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_checkAnonymousScope_match__1___rarg___closed__1 = _init_l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_checkAnonymousScope_match__1___rarg___closed__1(); -lean_mark_persistent(l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_checkAnonymousScope_match__1___rarg___closed__1); l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Command_elabNamespace___spec__1___rarg___closed__1 = _init_l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Command_elabNamespace___spec__1___rarg___closed__1(); lean_mark_persistent(l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Command_elabNamespace___spec__1___rarg___closed__1); l_Lean_Elab_Command_elabNamespace___closed__1 = _init_l_Lean_Elab_Command_elabNamespace___closed__1(); lean_mark_persistent(l_Lean_Elab_Command_elabNamespace___closed__1); l_Lean_Elab_Command_elabNamespace___closed__2 = _init_l_Lean_Elab_Command_elabNamespace___closed__2(); lean_mark_persistent(l_Lean_Elab_Command_elabNamespace___closed__2); -l_Lean_Elab_Command_elabNamespace___closed__3 = _init_l_Lean_Elab_Command_elabNamespace___closed__3(); -lean_mark_persistent(l_Lean_Elab_Command_elabNamespace___closed__3); -l_Lean_Elab_Command_elabNamespace___closed__4 = _init_l_Lean_Elab_Command_elabNamespace___closed__4(); -lean_mark_persistent(l_Lean_Elab_Command_elabNamespace___closed__4); -l_Lean_Elab_Command_elabNamespace___closed__5 = _init_l_Lean_Elab_Command_elabNamespace___closed__5(); -lean_mark_persistent(l_Lean_Elab_Command_elabNamespace___closed__5); -l_Lean_Elab_Command_elabNamespace___closed__6 = _init_l_Lean_Elab_Command_elabNamespace___closed__6(); -lean_mark_persistent(l_Lean_Elab_Command_elabNamespace___closed__6); -l_Lean_Elab_Command_elabNamespace___closed__7 = _init_l_Lean_Elab_Command_elabNamespace___closed__7(); -lean_mark_persistent(l_Lean_Elab_Command_elabNamespace___closed__7); -l_Lean_Elab_Command_elabNamespace___closed__8 = _init_l_Lean_Elab_Command_elabNamespace___closed__8(); -lean_mark_persistent(l_Lean_Elab_Command_elabNamespace___closed__8); l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__1 = _init_l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__1(); lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__1); l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__2 = _init_l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__2(); lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__2); l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__3 = _init_l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__3(); lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__3); -l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__4 = _init_l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__4(); -lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__4); -l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__5 = _init_l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__5(); -lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__5); -l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__6 = _init_l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__6(); -lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabNamespace___closed__6); res = l___regBuiltin_Lean_Elab_Command_elabNamespace(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); @@ -16347,8 +16701,6 @@ l_Lean_Elab_Command_elabCheck___lambda__1___closed__1 = _init_l_Lean_Elab_Comman lean_mark_persistent(l_Lean_Elab_Command_elabCheck___lambda__1___closed__1); l_Lean_Elab_Command_elabCheck___lambda__1___closed__2 = _init_l_Lean_Elab_Command_elabCheck___lambda__1___closed__2(); lean_mark_persistent(l_Lean_Elab_Command_elabCheck___lambda__1___closed__2); -l_Lean_Elab_Command_elabCheck___lambda__1___closed__3 = _init_l_Lean_Elab_Command_elabCheck___lambda__1___closed__3(); -lean_mark_persistent(l_Lean_Elab_Command_elabCheck___lambda__1___closed__3); l_Lean_Elab_Command_elabCheck___closed__1 = _init_l_Lean_Elab_Command_elabCheck___closed__1(); lean_mark_persistent(l_Lean_Elab_Command_elabCheck___closed__1); l_Lean_Elab_Command_elabCheck___closed__2 = _init_l_Lean_Elab_Command_elabCheck___closed__2(); diff --git a/stage0/stdlib/Lean/Elab/Syntax.c b/stage0/stdlib/Lean/Elab/Syntax.c index d9683b961f..a2248c240d 100644 --- a/stage0/stdlib/Lean/Elab/Syntax.c +++ b/stage0/stdlib/Lean/Elab/Syntax.c @@ -508,7 +508,7 @@ static lean_object* l_Subarray_forInUnsafe_loop___at___private_Lean_Elab_Syntax_ lean_object* l_Lean_Syntax_getKind(lean_object*); uint8_t l_Lean_Parser_isValidSyntaxNodeKind(lean_object*, lean_object*); static lean_object* l_Lean_Elab_Term_toParserDescr_processNullaryOrCat___closed__4; -uint8_t l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7399_(uint8_t, uint8_t); +uint8_t l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7405_(uint8_t, uint8_t); static lean_object* l_Lean_Elab_Command_elabSyntax___closed__1; lean_object* l___private_Lean_Elab_Syntax_0__Lean_Elab_Term_withNestedParser___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_checkLeftRec(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -4765,7 +4765,7 @@ lean_inc(x_15); lean_dec(x_13); x_62 = lean_ctor_get_uint8(x_2, sizeof(void*)*1 + 2); x_63 = 0; -x_64 = l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7399_(x_62, x_63); +x_64 = l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7405_(x_62, x_63); if (x_64 == 0) { uint8_t x_65; diff --git a/stage0/stdlib/Lean/Parser/Basic.c b/stage0/stdlib/Lean/Parser/Basic.c index 06aadffe49..d0f36c7420 100644 --- a/stage0/stdlib/Lean/Parser/Basic.c +++ b/stage0/stdlib/Lean/Parser/Basic.c @@ -66,7 +66,6 @@ lean_object* l_Lean_Parser_indexed_match__2(lean_object*, lean_object*); lean_object* lean_nat_div(lean_object*, lean_object*); static lean_object* l_Lean_Parser_eoi___closed__2; static lean_object* l_Lean_Parser_eoi___closed__1; -lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7722____lambda__1(lean_object*); lean_object* l_Lean_Parser_parserOfStack___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_manyNoAntiquot(lean_object*); lean_object* l_Lean_Parser_decimalNumberFn___boxed(lean_object*, lean_object*, lean_object*); @@ -148,7 +147,6 @@ lean_object* l_Lean_Parser_pushNone; static lean_object* l_Lean_Parser_dbgTraceStateFn___closed__1; static lean_object* l_Lean_Parser_checkNoImmediateColon___closed__1; lean_object* l_Lean_EnvExtensionInterfaceUnsafe_registerExt___rarg(lean_object*, lean_object*); -static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7722____closed__1; lean_object* l_Lean_Parser_dbgTraceStateFn___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Parser_info___default___elambda__1___boxed(lean_object*); lean_object* l_Lean_Parser_longestMatchFn_match__1(lean_object*); @@ -164,6 +162,7 @@ lean_object* l_Lean_Parser_anyOfFn_match__1___rarg(lean_object*, lean_object*, l lean_object* l_Lean_Parser_strAux_parse(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_Parser_isLitKind(lean_object*); lean_object* l_instInhabitedDepArrow___rarg(lean_object*, lean_object*); +static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7728____closed__1; static lean_object* l_Lean_Parser_instBEqError___closed__1; static lean_object* l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__1; lean_object* lean_dbg_trace(lean_object*, lean_object*); @@ -180,6 +179,7 @@ uint8_t l_Char_isDigit(uint32_t); lean_object* l_Lean_Parser_instCoeStringParser___boxed(lean_object*); static lean_object* l_Lean_Parser_evalParserConstUnsafe___closed__4; lean_object* l_Array_qpartition_loop___at_Lean_Parser_Error_toString___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7728____lambda__1(lean_object*); lean_object* l_Lean_Parser_ParserState_mkNode(lean_object*, lean_object*, lean_object*); uint8_t l_Lean_Parser_binNumberFn___lambda__1(uint32_t); lean_object* l_Lean_Parser_FirstTokens_toStr_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -202,7 +202,6 @@ lean_object* l_Lean_isIdRest___boxed(lean_object*); static lean_object* l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__8; lean_object* l_Lean_Parser_pushNone___elambda__1___boxed(lean_object*); lean_object* l_Lean_Parser_notFollowedByFn(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7703____lambda__1___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_orelseFn(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Std_RBNode_find___at_Lean_Parser_indexed___spec__4(lean_object*); static lean_object* l_Lean_Parser_instInhabitedInputContext___closed__3; @@ -533,6 +532,7 @@ lean_object* l_Lean_Parser_many1Unbox___lambda__1(lean_object*); lean_object* l_Lean_Parser_instBEqLeadingIdentBehavior; lean_object* l_Lean_Parser_rawCh___boxed(lean_object*, lean_object*); lean_object* l_Lean_Parser_getNext___boxed(lean_object*, lean_object*); +lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7709____lambda__1(lean_object*, lean_object*, lean_object*); lean_object* lean_format_pretty(lean_object*, lean_object*); lean_object* l_Lean_Parser_tokenWithAntiquotFn___lambda__1(lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Parser_termParser___closed__2; @@ -540,6 +540,7 @@ extern lean_object* l_Lean_choiceKind; extern lean_object* l_Lean_charLitKind; lean_object* l_Std_PersistentHashMap_mkEmptyEntriesArray(lean_object*, lean_object*); lean_object* l_Lean_Parser_errorFn(lean_object*, lean_object*, lean_object*); +lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7405__match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_maxPrec; lean_object* l_Lean_Parser_withForbidden___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Syntax_foldArgsM___spec__1(lean_object*, lean_object*); @@ -557,7 +558,6 @@ lean_object* l_Lean_Parser_sepBy___elambda__1___boxed(lean_object*, lean_object* lean_object* l_Lean_Parser_pushNone___elambda__1___rarg(lean_object*); lean_object* l_Lean_Parser_scientificLitFn(lean_object*, lean_object*); lean_object* lean_array_to_list(lean_object*, lean_object*); -lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7703____lambda__1(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_PrattParsingTables_leadingParsers___default; static lean_object* l_Lean_Parser_fieldIdx___closed__5; lean_object* l_Lean_Parser_symbolInfo___elambda__2(lean_object*, lean_object*); @@ -596,6 +596,7 @@ static lean_object* l_Lean_Parser_charLitNoAntiquot___closed__1; static lean_object* l_Lean_Parser_mkAntiquotSplice___closed__5; static lean_object* l_List_toString___at_Lean_Parser_FirstTokens_toStr___spec__1___closed__3; lean_object* l_Lean_Parser_ParserContext_quotDepth___default; +static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7709____closed__1; lean_object* l_Lean_Parser_evalInsideQuot___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_checkTailNoWs___boxed(lean_object*); lean_object* l_Lean_Parser_takeUntilFn(lean_object*, lean_object*, lean_object*); @@ -633,10 +634,8 @@ static lean_object* l_Lean_Parser_quotedCharCoreFn___closed__1; lean_object* l_Lean_Parser_ParserState_restore___boxed(lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Parser_identFnAux_parse___lambda__2___closed__2; static lean_object* l_Lean_Parser_mkAntiquot___closed__21; -static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7703____closed__1; lean_object* l_Lean_Parser_ParserState_restore(lean_object*, lean_object*, lean_object*); lean_object* l_Std_PersistentHashMap_insert___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7399____boxed(lean_object*, lean_object*); lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_pickNonNone_match__1___rarg(lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Parser_antiquotNestedExpr___closed__3; lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_pickNonNone(lean_object*); @@ -654,10 +653,12 @@ size_t lean_usize_of_nat(lean_object*); static lean_object* l_Lean_Parser_checkInsideQuotFn___closed__1; uint8_t l_Lean_Syntax_isAntiquot(lean_object*); static lean_object* l_Lean_Parser_mkAntiquot___closed__7; +lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7405____boxed(lean_object*, lean_object*); static lean_object* l_Lean_Parser_pushNone___closed__1; lean_object* l_Lean_Parser_chFn(uint32_t, uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Parser_antiquotNestedExpr; lean_object* l_Lean_Parser_mkAtomicInfo___elambda__2___boxed(lean_object*); +lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7405__match__1___rarg(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Parser_mkAntiquotSplice___closed__8; static lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_Error_expectedToString___closed__2; lean_object* l_List_toString___at_Lean_Parser_dbgTraceStateFn___spec__1(lean_object*); @@ -809,7 +810,7 @@ static lean_object* l_Lean_Parser_Error_instToStringError___closed__1; lean_object* l_Lean_Parser_checkTailNoWs_match__1(lean_object*); lean_object* l_Lean_Parser_TokenMap_instEmptyCollectionTokenMap(lean_object*); lean_object* l_Lean_Parser_orelseInfo___elambda__1(lean_object*, lean_object*, lean_object*); -uint8_t l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7399_(uint8_t, uint8_t); +uint8_t l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7405_(uint8_t, uint8_t); lean_object* l_Lean_Parser_errorAtSavedPos(lean_object*, uint8_t); static lean_object* l_Lean_Parser_mkAntiquot___closed__14; static lean_object* l_Lean_Parser_FirstTokens_toStr___closed__1; @@ -889,7 +890,6 @@ lean_object* l_Lean_Parser_sepBy1NoAntiquot(lean_object*, lean_object*, uint8_t) lean_object* l_Lean_Parser_instInhabitedParserFn___rarg(lean_object*); static lean_object* l_Lean_Parser_tokenWithAntiquotFn___lambda__2___closed__9; lean_object* l_Lean_Parser_Parser_info___default___elambda__2(lean_object*); -lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7399__match__1___rarg(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_String_trim(lean_object*); lean_object* l_Lean_isIdEndEscape___boxed(lean_object*); static lean_object* l_Lean_Parser_parserOfStackFnUnsafe___closed__2; @@ -933,14 +933,13 @@ 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*); static lean_object* l_Lean_Parser_mkAntiquot___closed__6; static lean_object* l_Lean_Parser_parserOfStackFnUnsafe___closed__1; -lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7703_(lean_object*); -lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7722_(lean_object*); +lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7709_(lean_object*); +lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7728_(lean_object*); uint8_t l_Lean_Parser_instInhabitedLeadingIdentBehavior; static lean_object* l_Lean_Parser_fieldIdx___closed__7; lean_object* l_Lean_Parser_mkAntiquot(lean_object*, lean_object*, uint8_t); static lean_object* l_Lean_Parser_instBEqLeadingIdentBehavior___closed__1; lean_object* l_Lean_Parser_optionaInfo___elambda__1(lean_object*, lean_object*); -lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7399__match__1(lean_object*); lean_object* l_Lean_Parser_decimalNumberFn_parseOptExp(lean_object*, lean_object*); lean_object* l_Lean_Parser_leadingNode(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_instInhabitedParserInfo___lambda__2(lean_object*); @@ -1031,7 +1030,6 @@ lean_object* l_Lean_Parser_sepBy1___elambda__1(uint8_t, lean_object*, lean_objec lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_sepByFnAux_parse___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_TokenCacheEntry_stopPos___default; lean_object* l_Lean_Parser_setExpected___elambda__1(lean_object*); -lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7399__match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Parser_unicodeSymbolInfo___closed__1; lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_tokenFnAux(lean_object*, lean_object*); lean_object* l_Lean_Parser_hexNumberFn___lambda__1___boxed(lean_object*); @@ -1055,6 +1053,7 @@ lean_object* l_Lean_Parser_longestMatchFnAux_parse_match__2(lean_object*); lean_object* l_Lean_Parser_trailingLoop___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_leadingParserAux___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Parser_antiquotExpr___closed__3; +lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7709____lambda__1___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_charLitNoAntiquot; lean_object* l_Lean_Parser_FirstTokens_merge_match__1(lean_object*); lean_object* l_Lean_mkErrorStringWithPos(lean_object*, lean_object*, lean_object*, lean_object*); @@ -1071,6 +1070,7 @@ lean_object* l_Std_RBNode_ins___at_Lean_Parser_TokenMap_insert___spec__7___rarg( lean_object* l_Std_RBNode_insert___at_Lean_Parser_TokenMap_insert___spec__2(lean_object*); static lean_object* l_Lean_Parser_mkAtomicInfo___closed__2; lean_object* l_Lean_Parser_sepBy___boxed(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7405__match__1(lean_object*); static lean_object* l_Lean_Parser_identNoAntiquot___closed__2; lean_object* l_Lean_Parser_withoutForbidden(lean_object*); lean_object* l_Lean_Parser_indexed_match__2___rarg(lean_object*, lean_object*, lean_object*); @@ -8808,23 +8808,28 @@ x_19 = lean_string_utf8_get(x_4, x_18); x_20 = x_19 == x_11; if (x_20 == 0) { -lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; uint8_t x_26; -x_21 = l_Lean_Parser_ParserState_next(x_2, x_4, x_18); -lean_dec(x_18); -x_22 = lean_unsigned_to_nat(1u); -x_23 = l_Lean_Parser_finishCommentBlock(x_22, x_1, x_21); -x_24 = lean_ctor_get(x_23, 4); -lean_inc(x_24); -x_25 = lean_box(0); -x_26 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_674____at_Lean_Parser_ParserState_hasError___spec__1(x_24, x_25); -lean_dec(x_24); -if (x_26 == 0) +uint32_t x_21; uint8_t x_22; +x_21 = 33; +x_22 = x_19 == x_21; +if (x_22 == 0) { -return x_23; +lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; uint8_t x_28; +x_23 = l_Lean_Parser_ParserState_next(x_2, x_4, x_18); +lean_dec(x_18); +x_24 = lean_unsigned_to_nat(1u); +x_25 = l_Lean_Parser_finishCommentBlock(x_24, x_1, x_23); +x_26 = lean_ctor_get(x_25, 4); +lean_inc(x_26); +x_27 = lean_box(0); +x_28 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_674____at_Lean_Parser_ParserState_hasError___spec__1(x_26, x_27); +lean_dec(x_26); +if (x_28 == 0) +{ +return x_25; } else { -x_2 = x_23; +x_2 = x_25; goto _start; } } @@ -8834,39 +8839,45 @@ lean_dec(x_18); return x_2; } } +else +{ +lean_dec(x_18); +return x_2; +} +} } } else { -lean_object* x_28; uint32_t x_29; uint8_t x_30; -x_28 = lean_string_utf8_next(x_4, x_5); +lean_object* x_30; uint32_t x_31; uint8_t x_32; +x_30 = lean_string_utf8_next(x_4, x_5); lean_dec(x_5); -x_29 = lean_string_utf8_get(x_4, x_28); -x_30 = x_29 == x_11; -if (x_30 == 0) +x_31 = lean_string_utf8_get(x_4, x_30); +x_32 = x_31 == x_11; +if (x_32 == 0) { -lean_dec(x_28); +lean_dec(x_30); return x_2; } else { -lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; uint8_t x_36; -x_31 = l_Lean_Parser_ParserState_next(x_2, x_4, x_28); -lean_dec(x_28); -x_32 = l_Lean_Parser_whitespace___closed__1; -x_33 = l_Lean_Parser_takeUntilFn(x_32, x_1, x_31); -x_34 = lean_ctor_get(x_33, 4); -lean_inc(x_34); -x_35 = lean_box(0); -x_36 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_674____at_Lean_Parser_ParserState_hasError___spec__1(x_34, x_35); -lean_dec(x_34); -if (x_36 == 0) +lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; uint8_t x_38; +x_33 = l_Lean_Parser_ParserState_next(x_2, x_4, x_30); +lean_dec(x_30); +x_34 = l_Lean_Parser_whitespace___closed__1; +x_35 = l_Lean_Parser_takeUntilFn(x_34, x_1, x_33); +x_36 = lean_ctor_get(x_35, 4); +lean_inc(x_36); +x_37 = lean_box(0); +x_38 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_674____at_Lean_Parser_ParserState_hasError___spec__1(x_36, x_37); +lean_dec(x_36); +if (x_38 == 0) { -return x_33; +return x_35; } else { -x_2 = x_33; +x_2 = x_35; goto _start; } } @@ -8874,21 +8885,21 @@ goto _start; } else { -lean_object* x_38; -x_38 = l_Lean_Parser_ParserState_next(x_2, x_4, x_5); +lean_object* x_40; +x_40 = l_Lean_Parser_ParserState_next(x_2, x_4, x_5); lean_dec(x_5); -x_2 = x_38; +x_2 = x_40; goto _start; } } else { -lean_object* x_40; lean_object* x_41; lean_object* x_42; +lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_dec(x_5); -x_40 = lean_box(0); -x_41 = l_Lean_Parser_whitespace___closed__2; -x_42 = l_Lean_Parser_ParserState_mkUnexpectedError(x_2, x_41, x_40); -return x_42; +x_42 = lean_box(0); +x_43 = l_Lean_Parser_whitespace___closed__2; +x_44 = l_Lean_Parser_ParserState_mkUnexpectedError(x_2, x_43, x_42); +return x_44; } } else @@ -26644,7 +26655,7 @@ x_1 = 0; return x_1; } } -lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7399__match__1___rarg(uint8_t x_1, uint8_t x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7405__match__1___rarg(uint8_t x_1, uint8_t x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { _start: { switch (x_1) { @@ -26726,15 +26737,15 @@ return x_24; } } } -lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7399__match__1(lean_object* x_1) { +lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7405__match__1(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7399__match__1___rarg___boxed), 6, 0); +x_2 = lean_alloc_closure((void*)(l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7405__match__1___rarg___boxed), 6, 0); return x_2; } } -lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7399__match__1___rarg___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* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7405__match__1___rarg___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) { _start: { uint8_t x_7; uint8_t x_8; lean_object* x_9; @@ -26742,11 +26753,11 @@ x_7 = lean_unbox(x_1); lean_dec(x_1); x_8 = lean_unbox(x_2); lean_dec(x_2); -x_9 = l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7399__match__1___rarg(x_7, x_8, x_3, x_4, x_5, x_6); +x_9 = l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7405__match__1___rarg(x_7, x_8, x_3, x_4, x_5, x_6); return x_9; } } -uint8_t l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7399_(uint8_t x_1, uint8_t x_2) { +uint8_t l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7405_(uint8_t x_1, uint8_t x_2) { _start: { switch (x_1) { @@ -26807,7 +26818,7 @@ return x_11; } } } -lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7399____boxed(lean_object* x_1, lean_object* x_2) { +lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7405____boxed(lean_object* x_1, lean_object* x_2) { _start: { uint8_t x_3; uint8_t x_4; uint8_t x_5; lean_object* x_6; @@ -26815,7 +26826,7 @@ x_3 = lean_unbox(x_1); lean_dec(x_1); x_4 = lean_unbox(x_2); lean_dec(x_2); -x_5 = l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7399_(x_3, x_4); +x_5 = l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7405_(x_3, x_4); x_6 = lean_box(x_5); return x_6; } @@ -26824,7 +26835,7 @@ static lean_object* _init_l_Lean_Parser_instBEqLeadingIdentBehavior___closed__1( _start: { lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7399____boxed), 2, 0); +x_1 = lean_alloc_closure((void*)(l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_7405____boxed), 2, 0); return x_1; } } @@ -28062,7 +28073,7 @@ lean_dec(x_1); return x_6; } } -lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7703____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_7709____lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { lean_object* x_4; @@ -28070,34 +28081,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_7703____closed__1() { +static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7709____closed__1() { _start: { lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7703____lambda__1___boxed), 3, 0); +x_1 = lean_alloc_closure((void*)(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7709____lambda__1___boxed), 3, 0); return x_1; } } -lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7703_(lean_object* x_1) { +lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7709_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; -x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7703____closed__1; +x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7709____closed__1; x_3 = l_IO_mkRef___rarg(x_2, x_1); return x_3; } } -lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7703____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_7709____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_7703____lambda__1(x_1, x_2, x_3); +x_4 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7709____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_7722____lambda__1(lean_object* x_1) { +lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7728____lambda__1(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; uint8_t x_4; @@ -28123,19 +28134,19 @@ return x_7; } } } -static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7722____closed__1() { +static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7728____closed__1() { _start: { lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7722____lambda__1), 1, 0); +x_1 = lean_alloc_closure((void*)(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7728____lambda__1), 1, 0); return x_1; } } -lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7722_(lean_object* x_1) { +lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7728_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; -x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7722____closed__1; +x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7728____closed__1; x_3 = l_Lean_EnvExtensionInterfaceUnsafe_registerExt___rarg(x_2, x_1); return x_3; } @@ -33605,20 +33616,20 @@ 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_7703____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7703____closed__1(); -lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7703____closed__1); -res = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7703_(lean_io_mk_world()); +l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7709____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7709____closed__1(); +lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7709____closed__1); +res = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7709_(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_7722____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7722____closed__1(); -lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7722____closed__1); +l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7728____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7728____closed__1(); +lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7728____closed__1); l_Lean_Parser_categoryParserFnExtension___closed__1 = _init_l_Lean_Parser_categoryParserFnExtension___closed__1(); lean_mark_persistent(l_Lean_Parser_categoryParserFnExtension___closed__1); l_Lean_Parser_categoryParserFnExtension___closed__2 = _init_l_Lean_Parser_categoryParserFnExtension___closed__2(); lean_mark_persistent(l_Lean_Parser_categoryParserFnExtension___closed__2); -res = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7722_(lean_io_mk_world()); +res = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7728_(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/ParserCompiler.c b/stage0/stdlib/Lean/ParserCompiler.c index da32816e3b..f6183461cb 100644 --- a/stage0/stdlib/Lean/ParserCompiler.c +++ b/stage0/stdlib/Lean/ParserCompiler.c @@ -27011,7 +27011,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_ParserCompiler_compileCategoryParser___rarg___closed__22; x_2 = l_Lean_ParserCompiler_compileCategoryParser___rarg___closed__23; -x_3 = lean_unsigned_to_nat(110u); +x_3 = lean_unsigned_to_nat(109u); x_4 = lean_unsigned_to_nat(6u); x_5 = l_Lean_ParserCompiler_compileCategoryParser___rarg___closed__24; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); diff --git a/stage0/stdlib/Lean/PrettyPrinter/Delaborator/Basic.c b/stage0/stdlib/Lean/PrettyPrinter/Delaborator/Basic.c index d3963fcd03..6959801958 100644 --- a/stage0/stdlib/Lean/PrettyPrinter/Delaborator/Basic.c +++ b/stage0/stdlib/Lean/PrettyPrinter/Delaborator/Basic.c @@ -9894,7 +9894,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_delab___lambda__1___closed__2; x_2 = l_Lean_PrettyPrinter_delab___lambda__1___closed__3; -x_3 = lean_unsigned_to_nat(230u); +x_3 = lean_unsigned_to_nat(229u); x_4 = lean_unsigned_to_nat(14u); x_5 = l_Lean_PrettyPrinter_delab___lambda__1___closed__4; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); diff --git a/stage0/stdlib/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.c b/stage0/stdlib/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.c index f13f943fcf..6178b55f77 100644 --- a/stage0/stdlib/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.c +++ b/stage0/stdlib/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.c @@ -16694,7 +16694,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_TopDownAnalyze_analyze_analyzeConst___closed__5; x_2 = l_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_analyze_analyzeConst___closed__6; -x_3 = lean_unsigned_to_nat(417u); +x_3 = lean_unsigned_to_nat(416u); x_4 = lean_unsigned_to_nat(41u); x_5 = l_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_analyze_analyzeConst___closed__7; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -19158,7 +19158,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_TopDownAnalyze_analyze_analyzeConst___closed__5; x_2 = l_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_analyze_analyzeLet___closed__1; -x_3 = lean_unsigned_to_nat(435u); +x_3 = lean_unsigned_to_nat(434u); x_4 = lean_unsigned_to_nat(46u); x_5 = l_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_analyze_analyzeConst___closed__7; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); diff --git a/stage0/stdlib/Lean/PrettyPrinter/Formatter.c b/stage0/stdlib/Lean/PrettyPrinter/Formatter.c index e611d92d25..e9c5c1a9d7 100644 --- a/stage0/stdlib/Lean/PrettyPrinter/Formatter.c +++ b/stage0/stdlib/Lean/PrettyPrinter/Formatter.c @@ -7190,7 +7190,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_Formatter_symbolNoAntiquot_formatter___closed__8; x_2 = l_Lean_PrettyPrinter_Formatter_symbolNoAntiquot_formatter___closed__9; -x_3 = lean_unsigned_to_nat(325u); +x_3 = lean_unsigned_to_nat(324u); x_4 = lean_unsigned_to_nat(42u); x_5 = l_Lean_PrettyPrinter_Formatter_symbolNoAntiquot_formatter___closed__10; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);