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

chore: update stage0

Browse source
This commit is contained in:
Sebastian Ullrich 2022-04-15 14:31:48 +02:00 • committed by Leonardo de Moura
parent e1fbc04c3b
commit ca8fdcaa0c
14 changed files with 4291 additions and 1351 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
stage0/src/Init/Meta.lean generated
View file

@ -60,6 +60,9 @@ def toolchain :=
else
""
@[extern c inline "LEAN_IS_STAGE0"]
constant Internal.isStage0 (u : Unit) : Bool
/- Valid identifier names -/
def isGreek (c : Char) : Bool :=
0x391 ≤ c.val && c.val ≤ 0x3dd

5
stage0/src/Lean/Environment.lean generated
View file

@ -282,7 +282,10 @@ end EnvExtension
/- Environment extensions can only be registered during initialization.
Reasons:
1- Our implementation assumes the number of extensions does not change after an environment object is created.
2- We do not use any synchronization primitive to access `envExtensionsRef`. -/
2- We do not use any synchronization primitive to access `envExtensionsRef`.
Note that by default, extension state is *not* stored in .olean files and will not propagate across `import`s.
For that, you need to register a persistent environment extension. -/
def registerEnvExtension {σ : Type} (mkInitial : IO σ) : IO (EnvExtension σ) := EnvExtensionInterfaceImp.registerExt mkInitial
private def mkInitialExtensionStates : IO (Array EnvExtensionState) := EnvExtensionInterfaceImp.mkInitialExtStates

2
stage0/src/Lean/Parser/Extension.lean generated
View file

@ -404,7 +404,7 @@ def addSyntaxNodeKind (env : Environment) (k : SyntaxNodeKind) : Environment :=
def isValidSyntaxNodeKind (env : Environment) (k : SyntaxNodeKind) : Bool :=
let kinds := (parserExtension.getState env).kinds
kinds.contains k
kinds.contains k || (Internal.isStage0 () && env.contains k)
def getSyntaxNodeKinds (env : Environment) : List SyntaxNodeKind :=
let kinds := (parserExtension.getState env).kinds

53
stage0/src/Lean/Server/Rpc/RequestHandling.lean generated
View file

@ -13,6 +13,7 @@ namespace Lean.Server
private structure RpcProcedure where
wrapper : (sessionId : UInt64) → Json → RequestM (RequestTask Json)
deriving Inhabited
/- We store the builtin RPC handlers in a Ref and users' handlers in an extension. This ensures
that users don't need to import core Lean modules to make builtin handlers work, but also that
@ -20,11 +21,11 @@ they *can* easily create custom handlers and use them in the same file. -/
builtin_initialize builtinRpcProcedures : IO.Ref (Std.PHashMap Name RpcProcedure) ←
IO.mkRef {}
builtin_initialize userRpcProcedures : EnvExtension (Std.PHashMap Name RpcProcedure) ←
registerEnvExtension <| pure {}
builtin_initialize userRpcProcedures : MapDeclarationExtension Name ←
mkMapDeclarationExtension `userRpcProcedures
open RequestM in
private def handleRpcCall (p : Lsp.RpcCallParams) : RequestM (RequestTask Json) := do
private unsafe def handleRpcCallUnsafe (p : Lsp.RpcCallParams) : RequestM (RequestTask Json) := do
let doc ← readDoc
let text := doc.meta.text
let callPos := text.lspPosToUtf8Pos p.position
@ -35,11 +36,21 @@ private def handleRpcCall (p : Lsp.RpcCallParams) : RequestM (RequestTask Json)
fun snap => do
if let some proc := (← builtinRpcProcedures.get).find? p.method then
proc.wrapper p.sessionId p.params
else if let some proc := userRpcProcedures.getState snap.env |>.find? p.method then
proc.wrapper p.sessionId p.params
else if let some procName := userRpcProcedures.find? snap.env p.method then
let options := snap.cmdState.scopes.head!.opts
let proc : Except _ _ := Lean.Environment.evalConstCheck RpcProcedure snap.env options ``RpcProcedure procName
match proc with
| Except.ok x => x.wrapper p.sessionId p.params
| Except.error e => throwThe RequestError {
code := JsonRpc.ErrorCode.internalError
message := s!"Failed to evaluate RPC constant '{procName}': {e}" }
else
throwThe RequestError { code := JsonRpc.ErrorCode.methodNotFound
message := s!"No RPC method '{p.method}' bound" }
throwThe RequestError {
code := JsonRpc.ErrorCode.methodNotFound
message := s!"No RPC method '{p.method}' bound" }
@[implementedBy handleRpcCallUnsafe]
private constant handleRpcCall (p : Lsp.RpcCallParams) : RequestM (RequestTask Json)
builtin_initialize
registerLspRequestHandler "$/lean/rpc/call" Lsp.RpcCallParams Json handleRpcCall
@ -87,21 +98,27 @@ def registerBuiltinRpcProcedure (method : Name) paramType respType
let proc := wrapRpcProcedure method paramType respType handler
builtinRpcProcedures.modify fun ps => ps.insert method proc
def registerRpcProcedure (method : Name) paramType respType
{paramLspType} [RpcEncoding paramType paramLspType] [FromJson paramLspType]
{respLspType} [RpcEncoding respType respLspType] [ToJson respLspType]
(handler : paramType → RequestM (RequestTask respType)) : CoreM Unit := do
open Lean Elab Command Term Meta in
def registerRpcProcedure (method : Name) : CoreM Unit := do
let env ← getEnv
let errMsg := "Failed to register RPC call handler for '{method}'"
if (←builtinRpcProcedures.get).contains method then
throwError s!"{errMsg}: already registered (builtin)"
if userRpcProcedures.getState env |>.contains method then
if userRpcProcedures.contains env method then
throwError s!"{errMsg}: already registered"
let proc := wrapRpcProcedure method paramType respType handler
let env' := userRpcProcedures.modifyState env fun procs =>
procs.insert method proc
setEnv env'
let wrappedName := method ++ `_rpc_wrapped
let procT := mkConst ``RpcProcedure
let proc ← MetaM.run' <| TermElabM.run' <| do
let c ← Lean.Elab.Term.elabTerm (← `(wrapRpcProcedure $(quote method) _ _ $(mkIdent method))) procT
return ← instantiateMVars c
addAndCompile <| Declaration.defnDecl {
name := wrappedName
type := procT
value := proc
safety := DefinitionSafety.safe
levelParams := []
hints := ReducibilityHints.opaque
}
setEnv <| userRpcProcedures.insert (← getEnv) method wrappedName
end Lean.Server

5
stage0/src/Lean/Util/Path.lean generated
View file

@ -56,9 +56,6 @@ end SearchPath
builtin_initialize searchPathRef : IO.Ref SearchPath ← IO.mkRef {}
@[extern c inline "LEAN_IS_STAGE0"]
private constant isStage0 (u : Unit) : Bool
@[export lean_get_prefix]
def getBuildDir : IO FilePath := do
return (← IO.appDir).parent |>.get!
@ -67,7 +64,7 @@ def getBuildDir : IO FilePath := do
def getLibDir (leanSysroot : FilePath) : IO FilePath := do
let mut buildDir := leanSysroot
-- use stage1 stdlib with stage0 executable (which should never be distributed outside of the build directory)
if isStage0 () then
if Internal.isStage0 () then
buildDir := buildDir / ".." / "stage1"
return buildDir / "lib" / "lean"

1
stage0/src/library/constructions/projection.cpp generated
View file

@ -31,7 +31,6 @@ static bool is_prop(expr type) {
}
environment mk_projections(environment const & env, name const & n, buffer<name> const & proj_names, bool inst_implicit) {
lean_assert(proj_names.size() == infer_kinds.size());
local_ctx lctx;
name_generator ngen = mk_constructions_name_generator();
constant_info ind_info = env.get(n);

1375
stage0/stdlib/Init/Meta.c generated
View file

File diff suppressed because it is too large Load diff

4
stage0/stdlib/Lean/Data/KVMap.c generated
View file

@ -139,7 +139,7 @@ LEAN_EXPORT uint8_t l_Lean_KVMap_contains(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_KVMap_instValueBool___lambda__1___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Lean_KVMap_instValueNat___lambda__2___boxed(lean_object*);
static lean_object* l___private_Lean_Data_KVMap_0__Lean_reprKVMap____x40_Lean_Data_KVMap___hyg_861____closed__3;
lean_object* l___private_Init_Meta_0__Lean_Name_reprSyntax____x40_Init_Meta___hyg_1069_(lean_object*, lean_object*);
lean_object* l___private_Init_Meta_0__Lean_Name_reprSyntax____x40_Init_Meta___hyg_1077_(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_mkBoolDataValueEx___boxed(lean_object*);
static lean_object* l_Lean_KVMap_instValueDataValue___closed__1;
LEAN_EXPORT lean_object* l_Lean_KVMap_instValueString___lambda__2___boxed(lean_object*);
@ -1063,7 +1063,7 @@ lean_inc(x_81);
lean_dec(x_1);
x_82 = lean_unsigned_to_nat(1024u);
x_83 = lean_nat_dec_le(x_82, x_2);
x_84 = l___private_Init_Meta_0__Lean_Name_reprSyntax____x40_Init_Meta___hyg_1069_(x_81, x_82);
x_84 = l___private_Init_Meta_0__Lean_Name_reprSyntax____x40_Init_Meta___hyg_1077_(x_81, x_82);
x_85 = l___private_Lean_Data_KVMap_0__Lean_reprDataValue____x40_Lean_Data_KVMap___hyg_257____closed__34;
x_86 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_86, 0, x_85);

12
stage0/stdlib/Lean/Meta/Basic.c generated
View file

@ -252,7 +252,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_forallMetaBoundedTelescope(lean_object*, le
LEAN_EXPORT lean_object* l_Lean_Meta_instMonadEnvMetaM___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAuxAux_process___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_isClassExpensive_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8521_(uint8_t, uint8_t);
uint8_t l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8529_(uint8_t, uint8_t);
static lean_object* l_Lean_Meta_instAlternativeMetaM___closed__2;
LEAN_EXPORT lean_object* l_Lean_Meta_setInlineAttribute___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_withConfig___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1440,7 +1440,7 @@ x_5 = lean_ctor_get(x_1, 1);
x_6 = lean_ctor_get_uint8(x_2, sizeof(void*)*2);
x_7 = lean_ctor_get(x_2, 0);
x_8 = lean_ctor_get(x_2, 1);
x_9 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8521_(x_3, x_6);
x_9 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8529_(x_3, x_6);
if (x_9 == 0)
{
uint8_t x_10;
@ -6902,7 +6902,7 @@ x_8 = lean_ctor_get(x_6, 0);
x_9 = 0;
x_10 = lean_unbox(x_8);
lean_dec(x_8);
x_11 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8521_(x_10, x_9);
x_11 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8529_(x_10, x_9);
x_12 = lean_box(x_11);
lean_ctor_set(x_6, 0, x_12);
return x_6;
@ -6918,7 +6918,7 @@ lean_dec(x_6);
x_15 = 0;
x_16 = lean_unbox(x_13);
lean_dec(x_13);
x_17 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8521_(x_16, x_15);
x_17 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8529_(x_16, x_15);
x_18 = lean_box(x_17);
x_19 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_19, 0, x_18);
@ -6952,7 +6952,7 @@ x_8 = lean_ctor_get(x_6, 0);
x_9 = 2;
x_10 = lean_unbox(x_8);
lean_dec(x_8);
x_11 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8521_(x_10, x_9);
x_11 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8529_(x_10, x_9);
x_12 = lean_box(x_11);
lean_ctor_set(x_6, 0, x_12);
return x_6;
@ -6968,7 +6968,7 @@ lean_dec(x_6);
x_15 = 2;
x_16 = lean_unbox(x_13);
lean_dec(x_13);
x_17 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8521_(x_16, x_15);
x_17 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8529_(x_16, x_15);
x_18 = lean_box(x_17);
x_19 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_19, 0, x_18);

6
stage0/stdlib/Lean/Meta/GetConst.c generated
View file

@ -21,7 +21,7 @@ lean_object* lean_st_ref_get(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_getConstNoEx_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_isReducible___at___private_Lean_Meta_GetConst_0__Lean_Meta_canUnfoldDefault___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_getConst_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8521_(uint8_t, uint8_t);
uint8_t l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8529_(uint8_t, uint8_t);
lean_object* l_Lean_ConstantInfo_name(lean_object*);
LEAN_EXPORT lean_object* l_Lean_getReducibilityStatus___at___private_Lean_Meta_GetConst_0__Lean_Meta_canUnfoldDefault___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_GetConst_0__Lean_Meta_canUnfoldDefault(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -315,7 +315,7 @@ x_39 = lean_ctor_get(x_38, 0);
lean_inc(x_39);
lean_dec(x_38);
x_40 = 3;
x_41 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8521_(x_6, x_40);
x_41 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8529_(x_6, x_40);
if (x_41 == 0)
{
uint8_t x_42; lean_object* x_43;
@ -360,7 +360,7 @@ x_51 = lean_ctor_get(x_49, 0);
lean_inc(x_51);
lean_dec(x_49);
x_52 = 3;
x_53 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8521_(x_6, x_52);
x_53 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8529_(x_6, x_52);
if (x_53 == 0)
{
uint8_t x_54; lean_object* x_55; lean_object* x_56;

8
stage0/stdlib/Lean/Meta/WHNF.c generated
View file

@ -131,7 +131,7 @@ size_t lean_usize_shift_right(size_t, size_t);
static lean_object* l_Lean_Meta_reduceNative_x3f___closed__14;
LEAN_EXPORT lean_object* l_Lean_Meta_smartUnfoldingMatch_x3f(lean_object*);
lean_object* l_Lean_Expr_getRevArg_x21(lean_object*, lean_object*);
uint8_t l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8521_(uint8_t, uint8_t);
uint8_t l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8529_(uint8_t, uint8_t);
static lean_object* l_Lean_Meta_toCtorIfLit___closed__16;
uint8_t lean_usize_dec_lt(size_t, size_t);
static lean_object* l_Lean_getConstInfoCtor___at___private_Lean_Meta_WHNF_0__Lean_Meta_toCtorWhenStructure___spec__1___closed__3;
@ -8975,7 +8975,7 @@ lean_inc(x_9);
lean_dec(x_7);
x_10 = 2;
x_11 = lean_unbox(x_8);
x_12 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8521_(x_11, x_10);
x_12 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8529_(x_11, x_10);
if (x_12 == 0)
{
lean_object* x_13; uint8_t x_14; lean_object* x_15;
@ -19419,7 +19419,7 @@ x_10 = lean_ctor_get(x_7, 1);
x_11 = 3;
x_12 = lean_unbox(x_9);
lean_dec(x_9);
x_13 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8521_(x_12, x_11);
x_13 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8529_(x_12, x_11);
if (x_13 == 0)
{
lean_object* x_14;
@ -19451,7 +19451,7 @@ lean_dec(x_7);
x_18 = 3;
x_19 = lean_unbox(x_16);
lean_dec(x_16);
x_20 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8521_(x_19, x_18);
x_20 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8529_(x_19, x_18);
if (x_20 == 0)
{
lean_object* x_21; lean_object* x_22;

264
stage0/stdlib/Lean/Parser/Extension.c generated
View file

@ -36,6 +36,7 @@ LEAN_EXPORT lean_object* l_Lean_Parser_evalParserConstUnsafe(lean_object*, lean_
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3517____closed__2;
LEAN_EXPORT lean_object* l_Lean_Parser_mkParserContext(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insert___at___private_Lean_Parser_Extension_0__Lean_Parser_addParserCategoryCore___spec__4(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5224____closed__2;
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
static lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_BuiltinParserAttribute_add___closed__1;
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3517____closed__4;
@ -44,6 +45,7 @@ LEAN_EXPORT lean_object* l_Std_PersistentHashMap_foldlMAux___at___private_Lean_P
LEAN_EXPORT lean_object* l_Lean_Parser_parserOfStack___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_addBuiltinParserCategory___closed__1;
lean_object* l_Lean_throwError___at_Lean_registerTagAttribute___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213____closed__2;
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3335____closed__4;
static lean_object* l_Lean_Parser_ParserExtension_instInhabitedOLeanEntry___closed__1;
LEAN_EXPORT lean_object* l_Lean_Parser_instCoeParserParserAliasValue(lean_object*);
@ -52,6 +54,7 @@ uint8_t lean_usize_dec_eq(size_t, size_t);
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Parser_addToken___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_uget(lean_object*, size_t);
LEAN_EXPORT lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_BuiltinParserAttribute_add___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5224____closed__1;
lean_object* lean_io_error_to_string(lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3785____closed__1;
LEAN_EXPORT lean_object* l_Lean_Parser_getBinaryAlias___rarg(lean_object*, lean_object*, lean_object*);
@ -71,9 +74,9 @@ LEAN_EXPORT uint8_t l_Lean_Parser_leadingIdentBehavior(lean_object*, lean_object
LEAN_EXPORT lean_object* l_Lean_Parser_addParser(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_categoryParserFnRef;
static lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_BuiltinParserAttribute_add___lambda__2___closed__12;
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____lambda__1___closed__2;
LEAN_EXPORT lean_object* l_Lean_Parser_withOpenDeclFn(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_addBuiltinParserCategory___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213____closed__1;
static lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_addBuiltinParserCategory___closed__2;
LEAN_EXPORT lean_object* l_Lean_Parser_compileParserDescr_visit___lambda__2(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_getConstAlias___rarg___boxed(lean_object*, lean_object*, lean_object*);
@ -99,7 +102,6 @@ extern lean_object* l_Lean_declRangeExt;
static lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_BuiltinParserAttribute_add___lambda__4___closed__2;
LEAN_EXPORT lean_object* l_Lean_Parser_registerBuiltinDynamicParserAttribute(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_getConstAlias___rarg___closed__2;
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____lambda__1___closed__1;
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3335____closed__3;
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_forM___at___private_Lean_Parser_Extension_0__Lean_Parser_ParserAttribute_add___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_getConstInfo___at_Lean_registerInitAttrUnsafe___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
@ -135,6 +137,7 @@ static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3335
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_foldlMAux___at_Lean_Parser_getSyntaxNodeKinds___spec__2___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_evalInsideQuot___elambda__1___closed__1;
LEAN_EXPORT lean_object* l_Lean_findDeclarationRangesCore_x3f___at___private_Lean_Parser_Extension_0__Lean_Parser_BuiltinParserAttribute_add___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213____closed__3;
uint8_t lean_usize_dec_lt(size_t, size_t);
uint8_t l_Lean_NameMap_contains___rarg(lean_object*, lean_object*);
extern lean_object* l_Lean_nameLitKind;
@ -148,9 +151,7 @@ LEAN_EXPORT lean_object* l_Lean_ofExcept___at_Lean_Parser_addToken___spec__1(lea
LEAN_EXPORT lean_object* l_Lean_Parser_addParserCategory(lean_object*, lean_object*, uint8_t);
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_findAtAux___at_Lean_Parser_getCategory___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_ScopedEnvExtension_add___at_Lean_Parser_addToken___spec__3___closed__1;
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____closed__1;
static lean_object* l_Lean_Parser_declareTrailingBuiltinParser___closed__1;
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199____closed__4;
static lean_object* l_Lean_Parser_mkParserOfConstantUnsafe___closed__2;
LEAN_EXPORT lean_object* l_Lean_Parser_getUnaryAlias(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_ParserAttribute_add(lean_object*);
@ -179,12 +180,12 @@ static size_t l_Std_PersistentHashMap_containsAux___at___private_Lean_Parser_Ext
LEAN_EXPORT lean_object* l_Lean_Parser_addSyntaxNodeKind(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_ofExcept___at_Lean_Parser_mkParserOfConstantUnsafe___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_compileParserDescr_visit___lambda__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5191____closed__4;
static lean_object* l_List_forM___at___private_Lean_Parser_Extension_0__Lean_Parser_ParserAttribute_add___spec__1___closed__2;
static lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_BuiltinParserAttribute_add___lambda__2___closed__17;
lean_object* l_Lean_ResolveName_resolveNamespace_x3f(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_BuiltinParserAttribute_add___lambda__4___closed__1;
static lean_object* l_Lean_Parser_withOpenDeclFnCore___closed__4;
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____lambda__1(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_mkParserAttributeImpl___elambda__1(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_internal_parseQuotWithCurrentStage;
lean_object* lean_array_fget(lean_object*, lean_object*);
@ -194,7 +195,6 @@ uint8_t l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attribu
LEAN_EXPORT lean_object* l_Lean_Parser_getBinaryAlias___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_nonReservedSymbolFnAux(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_updateBuiltinTokens___closed__2;
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____closed__2;
static lean_object* l_Lean_Parser_declareLeadingBuiltinParser___closed__4;
LEAN_EXPORT lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_ParserAttribute_add___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3139____lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -239,11 +239,11 @@ LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3785_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3517_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3335_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5188_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5210_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5177_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5202_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5224_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5191_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_180_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_6_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_74_(lean_object*);
@ -252,7 +252,6 @@ LEAN_EXPORT lean_object* l_Std_PersistentHashMap_containsAtAux___at___private_Le
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Parser_getSyntaxNodeKinds___spec__3(lean_object*, size_t, size_t, lean_object*);
static lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_BuiltinParserAttribute_add___lambda__2___closed__1;
LEAN_EXPORT lean_object* l_Lean_Parser_ParserExtension_addEntryImpl(lean_object*, lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____closed__3;
lean_object* l_Lean_Option_register___at_Std_Format_initFn____x40_Lean_Data_Format___hyg_54____spec__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Std_PersistentHashMap_contains___at___private_Lean_Parser_Extension_0__Lean_Parser_addParserCategoryCore___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_ParserExtension_State_categories___default;
@ -263,6 +262,7 @@ static lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_BuiltinPars
LEAN_EXPORT lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_BuiltinParserAttribute_add(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_foldlMAux___at_Lean_Parser_getSyntaxNodeKinds___spec__2___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Internal_isStage0(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_parserOfStack___elambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_BuiltinParserAttribute_add___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_foldlMAux___at_Lean_Parser_getSyntaxNodeKinds___spec__2(lean_object*, lean_object*);
@ -275,7 +275,6 @@ LEAN_EXPORT lean_object* l_Lean_Parser_instCoeForAllParserParserAliasValue(lean_
lean_object* l_Lean_Name_toExprAux(lean_object*);
static lean_object* l_Lean_Parser_mkParserOfConstantUnsafe___closed__4;
lean_object* l_Std_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5177____closed__4;
static lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_BuiltinParserAttribute_add___lambda__2___closed__19;
uint64_t l_Lean_Name_hash(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_addToken(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
@ -320,6 +319,7 @@ static lean_object* l_Lean_Parser_withOpenDeclFnCore___closed__3;
LEAN_EXPORT lean_object* l_Lean_Parser_addParserTokens(lean_object*, lean_object*);
uint32_t lean_string_utf8_get(lean_object*, lean_object*);
static lean_object* l_Lean_findDeclarationRanges_x3f___at___private_Lean_Parser_Extension_0__Lean_Parser_BuiltinParserAttribute_add___spec__1___closed__1;
static uint8_t l_Lean_Parser_isValidSyntaxNodeKind___closed__1;
LEAN_EXPORT lean_object* l_Lean_Parser_parserOfStackFn___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_parserOfStack(lean_object*, lean_object*);
static lean_object* l_Lean_Parser_registerAliasCore___rarg___closed__1;
@ -340,6 +340,7 @@ LEAN_EXPORT lean_object* l_Lean_Parser_withOpen(lean_object*);
extern lean_object* l_Lean_instInhabitedSyntax;
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Parser_getSyntaxNodeKinds___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_getParserPriority___closed__4;
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____closed__3;
static lean_object* l_Lean_Parser_withOpenDeclFnCore___closed__6;
static lean_object* l_Lean_Parser_mkParserOfConstantUnsafe___closed__6;
size_t lean_usize_mul(size_t, size_t);
@ -360,7 +361,6 @@ LEAN_EXPORT lean_object* l_Lean_Parser_registerAlias(lean_object*, lean_object*,
LEAN_EXPORT lean_object* l_Lean_Parser_isParserAlias___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_foldl___at_Lean_Parser_addLeadingParser___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
size_t lean_usize_of_nat(lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5177____closed__3;
LEAN_EXPORT lean_object* l_Lean_Parser_addTrailingParser(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_parserOfStackFn___closed__4;
lean_object* l_Lean_ConstantInfo_type(lean_object*);
@ -394,6 +394,7 @@ extern lean_object* l_Lean_identKind;
LEAN_EXPORT lean_object* l_Lean_Parser_getAlias___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_trailingLoop(lean_object*, lean_object*, lean_object*);
uint8_t lean_uint32_dec_eq(uint32_t, uint32_t);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5191____closed__3;
static lean_object* l_Lean_Parser_throwUnknownParserCategory___rarg___closed__2;
LEAN_EXPORT uint8_t l_Std_PersistentHashMap_containsAux___at___private_Lean_Parser_Extension_0__Lean_Parser_addParserCategoryCore___spec__2(lean_object*, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAux_traverse___at___private_Lean_Parser_Extension_0__Lean_Parser_addParserCategoryCore___spec__6(size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -406,10 +407,10 @@ LEAN_EXPORT lean_object* l_Lean_Parser_registerAliasCore___rarg___lambda__1___bo
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Parser_Extension_0__Lean_Parser_withNamespaces___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_mkParserAttributeImpl___elambda__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getNumArgs(lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199____closed__3;
static lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_BuiltinParserAttribute_add___lambda__2___closed__5;
extern lean_object* l_Lean_scientificLitKind;
LEAN_EXPORT lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_BuiltinParserAttribute_add___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213____closed__4;
LEAN_EXPORT lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_throwParserCategoryAlreadyDefined___rarg(lean_object*);
static lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_BuiltinParserAttribute_add___lambda__3___closed__1;
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3181____closed__1;
@ -422,6 +423,7 @@ LEAN_EXPORT uint8_t l_Lean_Parser_isParserCategory(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_BuiltinParserAttribute_add___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
uint8_t lean_usize_dec_le(size_t, size_t);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____closed__1;
LEAN_EXPORT lean_object* l_IO_ofExcept___at___private_Lean_Parser_Extension_0__Lean_Parser_addBuiltinParserCategory___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_categoryParser(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_ensureConstantParserAlias(lean_object*, lean_object*);
@ -447,6 +449,7 @@ static lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_BuiltinPars
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3335____closed__7;
uint8_t lean_is_aux_recursor(lean_object*, lean_object*);
lean_object* l_Lean_Parser_symbolInfo(lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____closed__2;
LEAN_EXPORT lean_object* l_Lean_Parser_parserAttributeHooks;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Parser_withOpenDeclFnCore___spec__1(size_t, size_t, lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3139____lambda__2___closed__2;
@ -457,6 +460,7 @@ LEAN_EXPORT lean_object* l_Lean_Parser_ParserExtension_State_kinds___default;
extern lean_object* l_Lean_Parser_epsilonInfo;
LEAN_EXPORT lean_object* l_IO_ofExcept___at_Lean_Parser_mkParserOfConstantUnsafe___spec__1___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_getParserPriority(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____lambda__1(lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3181____closed__4;
LEAN_EXPORT lean_object* l_Lean_Parser_builtinSyntaxNodeKindSetRef;
LEAN_EXPORT lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_BuiltinParserAttribute_add___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -478,19 +482,19 @@ LEAN_EXPORT lean_object* l_Lean_Parser_runParserAttributeHooks(lean_object*, lea
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Lean_Parser_ParserExtension_instInhabitedEntry___closed__1;
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Parser_Extension_0__Lean_Parser_ParserAttribute_add___spec__5(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____lambda__1___closed__2;
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3335____closed__8;
static lean_object* l_Lean_Parser_withOpenFn___closed__2;
static lean_object* l_Lean_Parser_mkParserOfConstantUnsafe___closed__7;
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5191____closed__1;
static lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_addTokenConfig___closed__1;
LEAN_EXPORT lean_object* l_Lean_ScopedEnvExtension_add___at_Lean_Parser_addToken___spec__3(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_declareLeadingBuiltinParser___closed__3;
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5188____closed__1;
lean_object* lean_panic_fn(lean_object*, lean_object*);
lean_object* l_String_trim(lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_35____closed__1;
lean_object* l_Lean_Parser_leadingParserAux(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_mkParserAttributeImpl___elambda__2(lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5177____closed__2;
lean_object* l_Lean_Parser_nodeFn(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_registerAliasCore___rarg___lambda__2___closed__2;
lean_object* l_Lean_Parser_TokenMap_insert___rarg(lean_object*, lean_object*, lean_object*);
@ -524,10 +528,10 @@ LEAN_EXPORT lean_object* l_Lean_Parser_parserOfStackFn(lean_object*, lean_object
LEAN_EXPORT lean_object* l_Lean_Parser_registerAliasCore___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_ofExcept___at_Lean_Parser_mkParserOfConstantUnsafe___spec__3___boxed(lean_object*, lean_object*);
static lean_object* l_Std_PersistentHashMap_foldlMAux___at_Lean_Parser_getSyntaxNodeKinds___spec__2___closed__1;
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____lambda__1___closed__1;
static lean_object* l_Lean_Parser_getParserPriority___closed__3;
lean_object* l_Lean_mkNatLit(lean_object*);
lean_object* l_Lean_mkStrLit(lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199____closed__2;
LEAN_EXPORT lean_object* l_Lean_Parser_leadingIdentBehavior___boxed(lean_object*, lean_object*);
static lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_BuiltinParserAttribute_add___lambda__2___closed__10;
LEAN_EXPORT lean_object* l_Lean_Parser_registerAliasCore___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -537,6 +541,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_addPar
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3517____closed__3;
LEAN_EXPORT lean_object* l_Lean_Parser_registerAliasCore___rarg___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_ParserExtension_mkInitial___closed__1;
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5202____closed__1;
lean_object* lean_usize_to_nat(size_t);
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAtCollisionNodeAux___at___private_Lean_Parser_Extension_0__Lean_Parser_addParserCategoryCore___spec__7(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3139____closed__5;
@ -549,29 +554,25 @@ LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg
LEAN_EXPORT lean_object* l_Lean_Parser_withOpenFn(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_mkParserOfConstantUnsafe___closed__3;
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_containsAux___at_Lean_Parser_isValidSyntaxNodeKind___spec__2___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5210____closed__1;
static lean_object* l_Lean_Parser_mkParserOfConstantUnsafe___closed__5;
extern lean_object* l_Lean_builtinDeclRanges;
uint8_t lean_string_utf8_at_end(lean_object*, lean_object*);
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5191____closed__2;
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3181____closed__2;
static lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_BuiltinParserAttribute_add___lambda__2___closed__3;
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5188____closed__2;
LEAN_EXPORT lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_BuiltinParserAttribute_add___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_getAlias___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_mkEmptyEntries(lean_object*, lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3139____closed__7;
LEAN_EXPORT lean_object* l_Lean_Parser_ParserExtension_Entry_toOLeanEntry(lean_object*);
lean_object* l_Lean_ScopedEnvExtension_activateScoped___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5177____closed__1;
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3335____closed__6;
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3181____lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_BuiltinParserAttribute_add___closed__3;
LEAN_EXPORT lean_object* l_Lean_Parser_withOpenDeclFnCore(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5210____closed__2;
lean_object* l_Lean_Parser_Trie_find_x3f_loop___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_getCategory(lean_object*, lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199____closed__1;
static lean_object* l_Lean_Parser_getConstAlias___rarg___closed__4;
LEAN_EXPORT lean_object* l_Lean_Parser_instCoeForAllParserParserAliasValue__1(lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_foldlMAux_traverse___at___private_Lean_Parser_Extension_0__Lean_Parser_ParserAttribute_add___spec__6___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -588,6 +589,7 @@ static lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_addTokenCon
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_contains___at_Lean_Parser_isValidSyntaxNodeKind___spec__1___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_registerParserCategory___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5202____closed__2;
lean_object* l_Lean_Parser_setLhsPrecFn___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_andthenFn(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_6____closed__1() {
@ -8475,6 +8477,15 @@ lean_dec(x_2);
return x_6;
}
}
static uint8_t _init_l_Lean_Parser_isValidSyntaxNodeKind___closed__1() {
_start:
{
lean_object* x_1; uint8_t x_2;
x_1 = lean_box(0);
x_2 = LEAN_IS_STAGE0;
return x_2;
}
}
LEAN_EXPORT uint8_t l_Lean_Parser_isValidSyntaxNodeKind(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -8482,12 +8493,38 @@ lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t
x_3 = l_Lean_Parser_ParserExtension_instInhabitedState;
x_4 = l_Lean_Parser_isParserCategory___closed__1;
x_5 = l_Lean_ScopedEnvExtension_getState___rarg(x_3, x_4, x_1);
lean_dec(x_1);
x_6 = lean_ctor_get(x_5, 1);
lean_inc(x_6);
lean_dec(x_5);
lean_inc(x_2);
x_7 = l_Std_PersistentHashMap_contains___at_Lean_Parser_isValidSyntaxNodeKind___spec__1(x_6, x_2);
return x_7;
if (x_7 == 0)
{
uint8_t x_8;
x_8 = l_Lean_Parser_isValidSyntaxNodeKind___closed__1;
if (x_8 == 0)
{
uint8_t x_9;
lean_dec(x_2);
lean_dec(x_1);
x_9 = 0;
return x_9;
}
else
{
uint8_t x_10;
x_10 = l_Lean_Environment_contains(x_1, x_2);
return x_10;
}
}
else
{
uint8_t x_11;
lean_dec(x_2);
lean_dec(x_1);
x_11 = 1;
return x_11;
}
}
}
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_containsAtAux___at_Lean_Parser_isValidSyntaxNodeKind___spec__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
@ -11710,7 +11747,7 @@ x_5 = l_Lean_registerBuiltinAttribute(x_4, x_3);
return x_5;
}
}
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____lambda__1___closed__1() {
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____lambda__1___closed__1() {
_start:
{
lean_object* x_1;
@ -11718,23 +11755,23 @@ x_1 = lean_mk_string("invalid parser attribute implementation builder arguments"
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____lambda__1___closed__2() {
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____lambda__1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____lambda__1___closed__1;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____lambda__1___closed__1;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____lambda__1(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____lambda__1(lean_object* x_1) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
lean_object* x_2;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____lambda__1___closed__2;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____lambda__1___closed__2;
return x_2;
}
else
@ -11752,7 +11789,7 @@ if (lean_obj_tag(x_4) == 0)
{
lean_object* x_5;
lean_dec(x_3);
x_5 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____lambda__1___closed__2;
x_5 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____lambda__1___closed__2;
return x_5;
}
else
@ -11786,7 +11823,7 @@ lean_object* x_12;
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_3);
x_12 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____lambda__1___closed__2;
x_12 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____lambda__1___closed__2;
return x_12;
}
}
@ -11796,7 +11833,7 @@ lean_object* x_13;
lean_dec(x_6);
lean_dec(x_4);
lean_dec(x_3);
x_13 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____lambda__1___closed__2;
x_13 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____lambda__1___closed__2;
return x_13;
}
}
@ -11806,13 +11843,13 @@ else
lean_object* x_14;
lean_dec(x_3);
lean_dec(x_1);
x_14 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____lambda__1___closed__2;
x_14 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____lambda__1___closed__2;
return x_14;
}
}
}
}
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____closed__1() {
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____closed__1() {
_start:
{
lean_object* x_1;
@ -11820,30 +11857,30 @@ x_1 = lean_mk_string("parserAttr");
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____closed__2() {
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____closed__1;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____closed__3() {
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____lambda__1), 1, 0);
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____lambda__1), 1, 0);
return x_1;
}
}
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071_(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____closed__2;
x_3 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____closed__2;
x_3 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____closed__3;
x_4 = l_Lean_registerAttributeImplBuilder(x_2, x_3, x_1);
return x_4;
}
@ -11875,7 +11912,7 @@ lean_ctor_set(x_13, 1, x_12);
x_14 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_14, 0, x_10);
lean_ctor_set(x_14, 1, x_13);
x_15 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____closed__2;
x_15 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____closed__2;
x_16 = l_Lean_registerAttributeOfBuilder(x_8, x_15, x_14, x_9);
return x_16;
}
@ -11915,7 +11952,7 @@ x_7 = l_Lean_Parser_registerParserCategory(x_1, x_2, x_3, x_6, x_5);
return x_7;
}
}
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5177____closed__1() {
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5191____closed__1() {
_start:
{
lean_object* x_1;
@ -11923,17 +11960,17 @@ x_1 = lean_mk_string("builtinTermParser");
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5177____closed__2() {
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5191____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5177____closed__1;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5191____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5177____closed__3() {
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5191____closed__3() {
_start:
{
lean_object* x_1;
@ -11941,28 +11978,28 @@ x_1 = lean_mk_string("term");
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5177____closed__4() {
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5191____closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5177____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5191____closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5177_(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5191_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5177____closed__2;
x_3 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5177____closed__4;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5191____closed__2;
x_3 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5191____closed__4;
x_4 = 0;
x_5 = l_Lean_Parser_registerBuiltinParserAttribute(x_2, x_3, x_4, x_1);
return x_5;
}
}
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5188____closed__1() {
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5202____closed__1() {
_start:
{
lean_object* x_1;
@ -11970,27 +12007,27 @@ x_1 = lean_mk_string("termParser");
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5188____closed__2() {
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5202____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5188____closed__1;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5202____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5188_(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5202_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5188____closed__2;
x_3 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5177____closed__4;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5202____closed__2;
x_3 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5191____closed__4;
x_4 = l_Lean_Parser_registerBuiltinDynamicParserAttribute(x_2, x_3, x_1);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199____closed__1() {
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213____closed__1() {
_start:
{
lean_object* x_1;
@ -11998,17 +12035,17 @@ x_1 = lean_mk_string("builtinCommandParser");
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199____closed__2() {
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199____closed__1;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199____closed__3() {
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213____closed__3() {
_start:
{
lean_object* x_1;
@ -12016,28 +12053,28 @@ x_1 = lean_mk_string("command");
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199____closed__4() {
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213____closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213____closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199_(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199____closed__2;
x_3 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199____closed__4;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213____closed__2;
x_3 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213____closed__4;
x_4 = 0;
x_5 = l_Lean_Parser_registerBuiltinParserAttribute(x_2, x_3, x_4, x_1);
return x_5;
}
}
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5210____closed__1() {
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5224____closed__1() {
_start:
{
lean_object* x_1;
@ -12045,22 +12082,22 @@ x_1 = lean_mk_string("commandParser");
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5210____closed__2() {
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5224____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5210____closed__1;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5224____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5210_(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5224_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5210____closed__2;
x_3 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199____closed__4;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5224____closed__2;
x_3 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213____closed__4;
x_4 = l_Lean_Parser_registerBuiltinDynamicParserAttribute(x_2, x_3, x_1);
return x_4;
}
@ -12069,7 +12106,7 @@ LEAN_EXPORT lean_object* l_Lean_Parser_commandParser(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199____closed__4;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213____closed__4;
x_3 = l_Lean_Parser_categoryParser(x_2, x_1);
return x_3;
}
@ -13371,6 +13408,7 @@ if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_ScopedEnvExtension_add___at_Lean_Parser_addToken___spec__3___closed__1 = _init_l_Lean_ScopedEnvExtension_add___at_Lean_Parser_addToken___spec__3___closed__1();
lean_mark_persistent(l_Lean_ScopedEnvExtension_add___at_Lean_Parser_addToken___spec__3___closed__1);
l_Lean_Parser_isValidSyntaxNodeKind___closed__1 = _init_l_Lean_Parser_isValidSyntaxNodeKind___closed__1();
l_Std_PersistentHashMap_foldlMAux___at_Lean_Parser_getSyntaxNodeKinds___spec__2___closed__1 = _init_l_Std_PersistentHashMap_foldlMAux___at_Lean_Parser_getSyntaxNodeKinds___spec__2___closed__1();
lean_mark_persistent(l_Std_PersistentHashMap_foldlMAux___at_Lean_Parser_getSyntaxNodeKinds___spec__2___closed__1);
l_Lean_Parser_mkParserState___closed__1 = _init_l_Lean_Parser_mkParserState___closed__1();
@ -13485,53 +13523,53 @@ l_Lean_Parser_mkParserAttributeImpl___closed__1 = _init_l_Lean_Parser_mkParserAt
lean_mark_persistent(l_Lean_Parser_mkParserAttributeImpl___closed__1);
l_Lean_Parser_mkParserAttributeImpl___closed__2 = _init_l_Lean_Parser_mkParserAttributeImpl___closed__2();
lean_mark_persistent(l_Lean_Parser_mkParserAttributeImpl___closed__2);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____lambda__1___closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____lambda__1___closed__1();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____lambda__1___closed__1);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____lambda__1___closed__2 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____lambda__1___closed__2();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____lambda__1___closed__2);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____closed__1();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____closed__1);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____closed__2 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____closed__2();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____closed__2);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____closed__3 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____closed__3();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071____closed__3);
res = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5071_(lean_io_mk_world());
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____lambda__1___closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____lambda__1___closed__1();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____lambda__1___closed__1);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____lambda__1___closed__2 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____lambda__1___closed__2();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____lambda__1___closed__2);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____closed__1();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____closed__1);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____closed__2 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____closed__2();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____closed__2);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____closed__3 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____closed__3();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085____closed__3);
res = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5085_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5177____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5177____closed__1();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5177____closed__1);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5177____closed__2 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5177____closed__2();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5177____closed__2);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5177____closed__3 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5177____closed__3();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5177____closed__3);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5177____closed__4 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5177____closed__4();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5177____closed__4);
res = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5177_(lean_io_mk_world());
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5191____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5191____closed__1();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5191____closed__1);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5191____closed__2 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5191____closed__2();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5191____closed__2);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5191____closed__3 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5191____closed__3();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5191____closed__3);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5191____closed__4 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5191____closed__4();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5191____closed__4);
res = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5191_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5188____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5188____closed__1();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5188____closed__1);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5188____closed__2 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5188____closed__2();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5188____closed__2);
res = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5188_(lean_io_mk_world());
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5202____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5202____closed__1();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5202____closed__1);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5202____closed__2 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5202____closed__2();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5202____closed__2);
res = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5202_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199____closed__1();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199____closed__1);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199____closed__2 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199____closed__2();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199____closed__2);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199____closed__3 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199____closed__3();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199____closed__3);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199____closed__4 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199____closed__4();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199____closed__4);
res = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5199_(lean_io_mk_world());
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213____closed__1();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213____closed__1);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213____closed__2 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213____closed__2();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213____closed__2);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213____closed__3 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213____closed__3();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213____closed__3);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213____closed__4 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213____closed__4();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213____closed__4);
res = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5213_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5210____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5210____closed__1();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5210____closed__1);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5210____closed__2 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5210____closed__2();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5210____closed__2);
res = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5210_(lean_io_mk_world());
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5224____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5224____closed__1();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5224____closed__1);
l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5224____closed__2 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5224____closed__2();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5224____closed__2);
res = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_5224_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_withOpenDeclFnCore___closed__1 = _init_l_Lean_Parser_withOpenDeclFnCore___closed__1();

3892
stage0/stdlib/Lean/Server/Rpc/RequestHandling.c generated
View file

File diff suppressed because it is too large Load diff

12
stage0/stdlib/Lean/Util/Path.c generated
View file

@ -77,8 +77,8 @@ extern lean_object* l_System_instInhabitedFilePath;
LEAN_EXPORT lean_object* l_Lean_SearchPath_findModuleWithExt___lambda__1___boxed(lean_object*, lean_object*);
static lean_object* l_Lean_addSearchPathFromEnv___closed__1;
static lean_object* l_Lean_modToFilePath_go___closed__3;
uint8_t l_Lean_Internal_isStage0(lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_810____at_Lean_SearchPath_findAllWithExt___spec__1___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Util_Path_0__Lean_isStage0___boxed(lean_object*);
LEAN_EXPORT lean_object* l_List_foldl___at_Lean_moduleNameOfFileName___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_findOLean___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* lean_st_mk_ref(lean_object*, lean_object*);
@ -119,7 +119,6 @@ lean_object* l_System_FilePath_isDir(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_modToFilePath(lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_SearchPath_findAllWithExt___closed__1;
LEAN_EXPORT uint8_t l___private_Lean_Util_Path_0__Lean_isStage0(lean_object*);
lean_object* lean_panic_fn(lean_object*, lean_object*);
lean_object* l_String_trim(lean_object*);
static lean_object* l_Lean_moduleNameOfFileName___lambda__2___closed__2;
@ -1040,15 +1039,6 @@ return x_7;
}
}
}
LEAN_EXPORT lean_object* l___private_Lean_Util_Path_0__Lean_isStage0___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = LEAN_IS_STAGE0;
x_3 = lean_box(x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_getBuildDir___closed__1() {
_start:
{