diff --git a/stage0/src/Lean/Data/Lsp/LanguageFeatures.lean b/stage0/src/Lean/Data/Lsp/LanguageFeatures.lean index 9705471adb..c48d3b0fa3 100644 --- a/stage0/src/Lean/Data/Lsp/LanguageFeatures.lean +++ b/stage0/src/Lean/Data/Lsp/LanguageFeatures.lean @@ -20,40 +20,16 @@ structure Hover where deriving ToJson, FromJson structure HoverParams extends TextDocumentPositionParams - -instance : FromJson HoverParams := ⟨fun j => do - let tdpp ← @fromJson? TextDocumentPositionParams _ j - pure ⟨tdpp⟩⟩ - -instance : ToJson HoverParams := - ⟨fun o => toJson o.toTextDocumentPositionParams⟩ + deriving FromJson, ToJson structure DeclarationParams extends TextDocumentPositionParams - -instance : FromJson DeclarationParams := ⟨fun j => do - let tdpp ← @fromJson? TextDocumentPositionParams _ j - pure ⟨tdpp⟩⟩ - -instance : ToJson DeclarationParams := - ⟨fun o => toJson o.toTextDocumentPositionParams⟩ + deriving FromJson, ToJson structure DefinitionParams extends TextDocumentPositionParams - -instance : FromJson DefinitionParams := ⟨fun j => do - let tdpp ← @fromJson? TextDocumentPositionParams _ j - pure ⟨tdpp⟩⟩ - -instance : ToJson DefinitionParams := - ⟨fun o => toJson o.toTextDocumentPositionParams⟩ + deriving FromJson, ToJson structure TypeDefinitionParams extends TextDocumentPositionParams - -instance : FromJson TypeDefinitionParams := ⟨fun j => do - let tdpp ← @fromJson? TextDocumentPositionParams _ j - pure ⟨tdpp⟩⟩ - -instance : ToJson TypeDefinitionParams := - ⟨fun o => toJson o.toTextDocumentPositionParams⟩ + deriving FromJson, ToJson structure DocumentSymbolParams where textDocument : TextDocumentIdentifier diff --git a/stage0/src/Lean/Elab/Binders.lean b/stage0/src/Lean/Elab/Binders.lean index 4f5c6453a9..2754bee52e 100644 --- a/stage0/src/Lean/Elab/Binders.lean +++ b/stage0/src/Lean/Elab/Binders.lean @@ -69,7 +69,7 @@ def declareTacticSyntax (tactic : Syntax) : TermElabM Name := safety := DefinitionSafety.safe } addDecl decl compileDecl decl - pure name + return name /- Expand `optional (binderTactic <|> binderDefault)` @@ -78,7 +78,7 @@ def binderDefault := parser! " := " >> termParser -/ private def expandBinderModifier (type : Syntax) (optBinderModifier : Syntax) : TermElabM Syntax := do if optBinderModifier.isNone then - pure type + return type else let modifier := optBinderModifier[0] let kind := modifier.getKind @@ -96,7 +96,7 @@ private def getBinderIds (ids : Syntax) : TermElabM (Array Syntax) := ids.getArgs.mapM fun id => let k := id.getKind if k == identKind || k == `Lean.Parser.Term.hole then - pure id + return id else throwErrorAt id "identifier or `_` expected" @@ -152,11 +152,17 @@ private def addLocalVarInfoCore (lctx : LocalContext) (stx : Syntax) (fvar : Exp private def addLocalVarInfo (stx : Syntax) (fvar : Expr) : TermElabM Unit := do addLocalVarInfoCore (← getLCtx) stx fvar +private def ensureAtomicBinderName (binderView : BinderView) : TermElabM Unit := + let n := binderView.id.getId.eraseMacroScopes + unless n.isAtomic do + throwErrorAt! binderView.id "invalid binder name '{n}', it must be atomic" + private partial def elabBinderViews {α} (binderViews : Array BinderView) (catchAutoBoundImplicit : Bool) (fvars : Array Expr) (k : Array Expr → TermElabM α) : TermElabM α := let rec loop (i : Nat) (fvars : Array Expr) : TermElabM α := do if h : i < binderViews.size then let binderView := binderViews.get ⟨i, h⟩ + ensureAtomicBinderName binderView if catchAutoBoundImplicit then elabTypeWithAutoBoundImplicit binderView.type fun type => do registerFailedToInferBinderTypeInfo type binderView.type @@ -169,7 +175,7 @@ private partial def elabBinderViews {α} (binderViews : Array BinderView) (catch withLocalDecl binderView.id.getId binderView.bi type fun fvar => do addLocalVarInfo binderView.id fvar loop (i+1) (fvars.push fvar) - else + else k fvars loop 0 fvars @@ -223,7 +229,7 @@ private partial def getFunBinderIds? (stx : Syntax) : OptionT TermElabM (Array S let convertElem (stx : Syntax) : OptionT TermElabM Syntax := match stx with | `(_) => do let ident ← mkFreshIdent stx; pure ident - | `($id:ident) => pure id + | `($id:ident) => return id | _ => failure match stx with | `($f $args*) => do @@ -269,16 +275,18 @@ partial def expandFunBinders (binders : Array Syntax) (body : Syntax) : TermElab | Syntax.node `Lean.Parser.Term.hole _ => let ident ← mkFreshIdent binder let type := binder - loop body (i+1) (newBinders.push $ mkExplicitBinder ident type) + loop body (i+1) (newBinders.push <| mkExplicitBinder ident type) | Syntax.node `Lean.Parser.Term.paren args => -- `(` (termParser >> parenSpecial)? `)` -- parenSpecial := (tupleTail <|> typeAscription)? let binderBody := binder[1] - if binderBody.isNone then processAsPattern () + if binderBody.isNone then + processAsPattern () else let idents := binderBody[0] let special := binderBody[1] - if special.isNone then processAsPattern () + if special.isNone then + processAsPattern () else if special[0].getKind != `Lean.Parser.Term.typeAscription then processAsPattern () else @@ -287,9 +295,9 @@ partial def expandFunBinders (binders : Array Syntax) (body : Syntax) : TermElab match (← getFunBinderIds? idents) with | some idents => loop body (i+1) (newBinders ++ idents.map (fun ident => mkExplicitBinder ident type)) | none => processAsPattern () - | Syntax.ident _ _ _ _ => + | Syntax.ident .. => let type := mkHole binder - loop body (i+1) (newBinders.push $ mkExplicitBinder binder type) + loop body (i+1) (newBinders.push <| mkExplicitBinder binder type) | _ => processAsPattern () else pure (newBinders, body, false) @@ -315,10 +323,11 @@ private def propagateExpectedType (fvar : Expr) (fvarType : Expr) (s : State) : pure { s with expectedType? := some b } | _ => pure { s with expectedType? := none } -private partial def elabFunBinderViews (binderViews : Array BinderView) (i : Nat) (s : State) : TermElabM State := +private partial def elabFunBinderViews (binderViews : Array BinderView) (i : Nat) (s : State) : TermElabM State := do if h : i < binderViews.size then let binderView := binderViews.get ⟨i, h⟩ - withRef binderView.type $ withLCtx s.lctx s.localInsts do + ensureAtomicBinderName binderView + withRef binderView.type <| withLCtx s.lctx s.localInsts do let type ← elabType binderView.type registerFailedToInferBinderTypeInfo type binderView.type let fvarId ← mkFreshFVarId @@ -332,7 +341,7 @@ private partial def elabFunBinderViews (binderViews : Array BinderView) (i : Nat -/ let lctx := s.lctx.mkLocalDecl fvarId binderView.id.getId type binderView.bi addLocalVarInfoCore lctx binderView.id fvar - let s ← withRef binderView.id $ propagateExpectedType fvar type s + let s ← withRef binderView.id <| propagateExpectedType fvar type s let s := { s with lctx := lctx } match (← isClass? type) with | none => elabFunBinderViews binderViews (i+1) s @@ -360,7 +369,7 @@ def elabFunBinders {α} (binders : Array Syntax) (expectedType? : Option Expr) ( let lctx ← getLCtx let localInsts ← getLocalInstances let s ← FunBinders.elabFunBindersAux binders 0 { lctx := lctx, localInsts := localInsts, expectedType? := expectedType? } - resettingSynthInstanceCacheWhen (s.localInsts.size > localInsts.size) $ withLCtx s.lctx s.localInsts $ + resettingSynthInstanceCacheWhen (s.localInsts.size > localInsts.size) <| withLCtx s.lctx s.localInsts <| x s.fvars s.expectedType? /- Helper function for `expandEqnsIntoMatch` -/ @@ -473,7 +482,7 @@ def expandMatchAltsWhereDecls (matchAltsWhereDecls : Syntax) : MacroM Syntax := let (binders, body, expandedPattern) ← expandFunBinders binders body if expandedPattern then let newStx ← `(fun $binders* => $body) - withMacroExpansion stx newStx $ elabTerm newStx expectedType? + withMacroExpansion stx newStx <| elabTerm newStx expectedType? else elabFunBinders binders expectedType? fun xs expectedType? => do /- We ensure the expectedType here since it will force coercions to be applied if needed. @@ -519,7 +528,7 @@ def elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx : Syntax) (va let body ← elabTerm body expectedType? let body ← instantiateMVars body mkLambdaFVars #[x] body - pure $ mkApp f val + pure <| mkApp f val if elabBodyFirst then forallBoundedTelescope type arity fun xs type => do let valResult ← elabTermEnsuringType valStx type @@ -547,7 +556,7 @@ def expandLetEqnsDecl (letDecl : Syntax) : MacroM Syntax := do let ref := letDecl let matchAlts := letDecl[3] let val ← expandMatchAltsIntoMatch ref matchAlts - pure $ Syntax.node `Lean.Parser.Term.letIdDecl #[letDecl[0], letDecl[1], letDecl[2], mkAtomFrom ref " := ", val] + return Syntax.node `Lean.Parser.Term.letIdDecl #[letDecl[0], letDecl[1], letDecl[2], mkAtomFrom ref " := ", val] def elabLetDeclCore (stx : Syntax) (expectedType? : Option Expr) (useLetExpr : Bool) (elabBodyFirst : Bool) : TermElabM Expr := do let ref := stx @@ -568,12 +577,12 @@ def elabLetDeclCore (stx : Syntax) (expectedType? : Option Expr) (useLetExpr : B | true, true => stxNew.setKind `Lean.Parser.Term.«let*» | false, true => stxNew.setKind `Lean.Parser.Term.«let!» | false, false => unreachable! - withMacroExpansion stx stxNew $ elabTerm stxNew expectedType? + withMacroExpansion stx stxNew <| elabTerm stxNew expectedType? else if letDecl.getKind == `Lean.Parser.Term.letEqnsDecl then - let letDeclIdNew ← liftMacroM $ expandLetEqnsDecl letDecl + let letDeclIdNew ← liftMacroM <| expandLetEqnsDecl letDecl let declNew := stx[1].setArg 0 letDeclIdNew let stxNew := stx.setArg 1 declNew - withMacroExpansion stx stxNew $ elabTerm stxNew expectedType? + withMacroExpansion stx stxNew <| elabTerm stxNew expectedType? else throwUnsupportedSyntax diff --git a/stage0/src/Lean/Elab/Do.lean b/stage0/src/Lean/Elab/Do.lean index 85556c3c41..5ed400a865 100644 --- a/stage0/src/Lean/Elab/Do.lean +++ b/stage0/src/Lean/Elab/Do.lean @@ -488,7 +488,7 @@ def mkIte (ref : Syntax) (optIdent : Syntax) (cond : Syntax) (thenBranch : CodeB } private def mkUnit : MacroM Syntax := - `(PUnit.unit) + `((⟨⟩ : PUnit)) private def mkPureUnit : MacroM Syntax := `(pure PUnit.unit) diff --git a/stage0/stdlib/Lean/Data/Lsp/Basic.c b/stage0/stdlib/Lean/Data/Lsp/Basic.c index 2c98d7ca05..b2a58d612d 100644 --- a/stage0/stdlib/Lean/Data/Lsp/Basic.c +++ b/stage0/stdlib/Lean/Data/Lsp/Basic.c @@ -116,7 +116,6 @@ lean_object* l_Lean_Lsp_instFromJsonStaticRegistrationOptions; lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonTextDocumentItem____x40_Lean_Data_Lsp_Basic___hyg_1189_(lean_object*); lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonCommand____x40_Lean_Data_Lsp_Basic___hyg_750_(lean_object*); lean_object* l_Lean_Lsp_instFromJsonPosition___closed__1; -lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonWorkDoneProgressBegin____x40_Lean_Data_Lsp_Basic___hyg_1815____closed__1; lean_object* l_Lean_Lsp_instFromJsonTextEdit___closed__1; lean_object* l_Lean_Lsp_instFromJsonStaticRegistrationOptions___closed__1; lean_object* l_Lean_Lsp_instToJsonDocumentSelector(lean_object*); @@ -135,7 +134,6 @@ lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__L lean_object* l_Lean_Lsp_instBEqRange; extern lean_object* l_Lean_JsonRpc_instToJsonMessage___closed__7; lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonCancelParams____x40_Lean_Data_Lsp_Basic___hyg_59____boxed(lean_object*); -lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonWorkDoneProgressEnd____x40_Lean_Data_Lsp_Basic___hyg_1881____boxed(lean_object*); lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextEdit____x40_Lean_Data_Lsp_Basic___hyg_812____closed__1; lean_object* l_Lean_Lsp_instFromJsonMarkupKind_match__1(lean_object*); lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonVersionedTextDocumentIdentifier____x40_Lean_Data_Lsp_Basic___hyg_976____spec__1(lean_object*, lean_object*); @@ -177,6 +175,7 @@ lean_object* l_Lean_Lsp_instBEqPosition___closed__1; lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonLocationLink____x40_Lean_Data_Lsp_Basic___hyg_584____spec__1(lean_object*, lean_object*); lean_object* l_Lean_Lsp_instFromJsonRange___closed__1; lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonPosition____x40_Lean_Data_Lsp_Basic___hyg_219_(lean_object*); +lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonWorkDoneProgressEnd____x40_Lean_Data_Lsp_Basic___hyg_1872____boxed(lean_object*); lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonPosition____x40_Lean_Data_Lsp_Basic___hyg_219____spec__1___boxed(lean_object*, lean_object*); lean_object* l_Lean_Lsp_instFromJsonTextEdit; lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonCancelParams____x40_Lean_Data_Lsp_Basic___hyg_84_(lean_object*); @@ -273,7 +272,7 @@ lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextEdit____x40_L lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonMarkupContent____x40_Lean_Data_Lsp_Basic___hyg_1626____closed__3; lean_object* l_Lean_Lsp_instToJsonRange; lean_object* l_Lean_Lsp_instToJsonMarkupKind___boxed(lean_object*); -lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonWorkDoneProgressEnd____x40_Lean_Data_Lsp_Basic___hyg_1881_(lean_object*); +lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonWorkDoneProgressEnd____x40_Lean_Data_Lsp_Basic___hyg_1872_(lean_object*); extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_494____closed__1; lean_object* l_Lean_Lsp_instToJsonMarkupKind___closed__1; lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonRange____x40_Lean_Data_Lsp_Basic___hyg_353_(lean_object*); @@ -4868,94 +4867,74 @@ x_1 = l_Lean_Lsp_WorkDoneProgressBegin_kind___default___closed__1; return x_1; } } -static lean_object* _init_l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonWorkDoneProgressBegin____x40_Lean_Data_Lsp_Basic___hyg_1815____closed__1() { -_start: -{ -lean_object* x_1; -x_1 = lean_mk_string("toWorkDoneProgressReport"); -return x_1; -} -} lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonWorkDoneProgressBegin____x40_Lean_Data_Lsp_Basic___hyg_1815_(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; lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; 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_2; lean_object* x_3; lean_object* x_4; uint8_t x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -lean_inc(x_2); -x_3 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonWorkDoneProgressReport____x40_Lean_Data_Lsp_Basic___hyg_1768_(x_2); -x_4 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonWorkDoneProgressBegin____x40_Lean_Data_Lsp_Basic___hyg_1815____closed__1; -x_5 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_5, 0, x_4); -lean_ctor_set(x_5, 1, x_3); -x_6 = lean_box(0); -x_7 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_7, 0, x_5); -lean_ctor_set(x_7, 1, x_6); -x_8 = lean_ctor_get(x_2, 0); -lean_inc(x_8); -x_9 = lean_ctor_get(x_2, 1); -lean_inc(x_9); -x_10 = lean_ctor_get_uint8(x_2, sizeof(void*)*3); -x_11 = lean_ctor_get(x_2, 2); -lean_inc(x_11); +x_3 = lean_ctor_get(x_2, 0); +lean_inc(x_3); +x_4 = lean_ctor_get(x_2, 1); +lean_inc(x_4); +x_5 = lean_ctor_get_uint8(x_2, sizeof(void*)*3); +x_6 = lean_ctor_get(x_2, 2); +lean_inc(x_6); lean_dec(x_2); -x_12 = lean_alloc_ctor(3, 1, 0); -lean_ctor_set(x_12, 0, x_8); -x_13 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonMarkupContent____x40_Lean_Data_Lsp_Basic___hyg_1626____closed__2; -x_14 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_14, 0, x_13); -lean_ctor_set(x_14, 1, x_12); -x_15 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_15, 0, x_14); -lean_ctor_set(x_15, 1, x_6); -x_16 = l_Lean_JsonRpc_instToJsonMessage___closed__10; -x_17 = l_Lean_Json_opt___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonDocumentFilter____x40_Lean_Data_Lsp_Basic___hyg_1354____spec__1(x_16, x_9); -lean_dec(x_9); -x_18 = lean_alloc_ctor(1, 0, 1); -lean_ctor_set_uint8(x_18, 0, x_10); -x_19 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonWorkDoneProgressReport____x40_Lean_Data_Lsp_Basic___hyg_1768____closed__1; -x_20 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_20, 0, x_19); -lean_ctor_set(x_20, 1, x_18); -x_21 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_21, 0, x_20); -lean_ctor_set(x_21, 1, x_6); -x_22 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonWorkDoneProgressReport____x40_Lean_Data_Lsp_Basic___hyg_1768____closed__2; -x_23 = l_Lean_Json_opt___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonVersionedTextDocumentIdentifier____x40_Lean_Data_Lsp_Basic___hyg_976____spec__1(x_22, x_11); -x_24 = lean_ctor_get(x_1, 1); -lean_inc(x_24); +x_7 = lean_alloc_ctor(3, 1, 0); +lean_ctor_set(x_7, 0, x_3); +x_8 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonMarkupContent____x40_Lean_Data_Lsp_Basic___hyg_1626____closed__2; +x_9 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_9, 0, x_8); +lean_ctor_set(x_9, 1, x_7); +x_10 = lean_box(0); +x_11 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_11, 0, x_9); +lean_ctor_set(x_11, 1, x_10); +x_12 = l_Lean_JsonRpc_instToJsonMessage___closed__10; +x_13 = l_Lean_Json_opt___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonDocumentFilter____x40_Lean_Data_Lsp_Basic___hyg_1354____spec__1(x_12, x_4); +lean_dec(x_4); +x_14 = lean_alloc_ctor(1, 0, 1); +lean_ctor_set_uint8(x_14, 0, x_5); +x_15 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonWorkDoneProgressReport____x40_Lean_Data_Lsp_Basic___hyg_1768____closed__1; +x_16 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_16, 0, x_15); +lean_ctor_set(x_16, 1, x_14); +x_17 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_17, 0, x_16); +lean_ctor_set(x_17, 1, x_10); +x_18 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonWorkDoneProgressReport____x40_Lean_Data_Lsp_Basic___hyg_1768____closed__2; +x_19 = l_Lean_Json_opt___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonVersionedTextDocumentIdentifier____x40_Lean_Data_Lsp_Basic___hyg_976____spec__1(x_18, x_6); +x_20 = lean_ctor_get(x_1, 1); +lean_inc(x_20); lean_dec(x_1); -x_25 = lean_alloc_ctor(3, 1, 0); +x_21 = lean_alloc_ctor(3, 1, 0); +lean_ctor_set(x_21, 0, x_20); +x_22 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonCommand____x40_Lean_Data_Lsp_Basic___hyg_712____closed__1; +x_23 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_23, 0, x_22); +lean_ctor_set(x_23, 1, x_21); +x_24 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_24, 0, x_23); +lean_ctor_set(x_24, 1, x_10); +x_25 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_25, 0, x_24); -x_26 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonCommand____x40_Lean_Data_Lsp_Basic___hyg_712____closed__1; -x_27 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_27, 0, x_26); -lean_ctor_set(x_27, 1, x_25); +lean_ctor_set(x_25, 1, x_10); +x_26 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_26, 0, x_19); +lean_ctor_set(x_26, 1, x_25); +x_27 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_27, 0, x_17); +lean_ctor_set(x_27, 1, x_26); x_28 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_28, 0, x_27); -lean_ctor_set(x_28, 1, x_6); +lean_ctor_set(x_28, 0, x_13); +lean_ctor_set(x_28, 1, x_27); x_29 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_29, 0, x_28); -lean_ctor_set(x_29, 1, x_6); -x_30 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_30, 0, x_23); -lean_ctor_set(x_30, 1, x_29); -x_31 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_31, 0, x_21); -lean_ctor_set(x_31, 1, x_30); -x_32 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_32, 0, x_17); -lean_ctor_set(x_32, 1, x_31); -x_33 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_33, 0, x_15); -lean_ctor_set(x_33, 1, x_32); -x_34 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_34, 0, x_7); -lean_ctor_set(x_34, 1, x_33); -x_35 = l_List_join___rarg(x_34); -x_36 = l_Lean_Json_mkObj(x_35); -return x_36; +lean_ctor_set(x_29, 0, x_11); +lean_ctor_set(x_29, 1, x_28); +x_30 = l_List_join___rarg(x_29); +x_31 = l_Lean_Json_mkObj(x_30); +return x_31; } } static lean_object* _init_l_Lean_Lsp_instToJsonWorkDoneProgressBegin___closed__1() { @@ -4990,7 +4969,7 @@ x_1 = lean_box(0); return x_1; } } -lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonWorkDoneProgressEnd____x40_Lean_Data_Lsp_Basic___hyg_1881_(lean_object* x_1) { +lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonWorkDoneProgressEnd____x40_Lean_Data_Lsp_Basic___hyg_1872_(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; 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; @@ -5020,11 +4999,11 @@ x_14 = l_Lean_Json_mkObj(x_13); return x_14; } } -lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonWorkDoneProgressEnd____x40_Lean_Data_Lsp_Basic___hyg_1881____boxed(lean_object* x_1) { +lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonWorkDoneProgressEnd____x40_Lean_Data_Lsp_Basic___hyg_1872____boxed(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonWorkDoneProgressEnd____x40_Lean_Data_Lsp_Basic___hyg_1881_(x_1); +x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonWorkDoneProgressEnd____x40_Lean_Data_Lsp_Basic___hyg_1872_(x_1); lean_dec(x_1); return x_2; } @@ -5033,7 +5012,7 @@ static lean_object* _init_l_Lean_Lsp_instToJsonWorkDoneProgressEnd___closed__1() _start: { lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonWorkDoneProgressEnd____x40_Lean_Data_Lsp_Basic___hyg_1881____boxed), 1, 0); +x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonWorkDoneProgressEnd____x40_Lean_Data_Lsp_Basic___hyg_1872____boxed), 1, 0); return x_1; } } @@ -5335,8 +5314,6 @@ l_Lean_Lsp_WorkDoneProgressBegin_kind___default___closed__1 = _init_l_Lean_Lsp_W lean_mark_persistent(l_Lean_Lsp_WorkDoneProgressBegin_kind___default___closed__1); l_Lean_Lsp_WorkDoneProgressBegin_kind___default = _init_l_Lean_Lsp_WorkDoneProgressBegin_kind___default(); lean_mark_persistent(l_Lean_Lsp_WorkDoneProgressBegin_kind___default); -l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonWorkDoneProgressBegin____x40_Lean_Data_Lsp_Basic___hyg_1815____closed__1 = _init_l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonWorkDoneProgressBegin____x40_Lean_Data_Lsp_Basic___hyg_1815____closed__1(); -lean_mark_persistent(l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonWorkDoneProgressBegin____x40_Lean_Data_Lsp_Basic___hyg_1815____closed__1); l_Lean_Lsp_instToJsonWorkDoneProgressBegin___closed__1 = _init_l_Lean_Lsp_instToJsonWorkDoneProgressBegin___closed__1(); lean_mark_persistent(l_Lean_Lsp_instToJsonWorkDoneProgressBegin___closed__1); l_Lean_Lsp_instToJsonWorkDoneProgressBegin = _init_l_Lean_Lsp_instToJsonWorkDoneProgressBegin(); diff --git a/stage0/stdlib/Lean/Data/Lsp/LanguageFeatures.c b/stage0/stdlib/Lean/Data/Lsp/LanguageFeatures.c index 89d6f0b5be..c9a985eabf 100644 --- a/stage0/stdlib/Lean/Data/Lsp/LanguageFeatures.c +++ b/stage0/stdlib/Lean/Data/Lsp/LanguageFeatures.c @@ -14,22 +14,25 @@ extern "C" { #endif size_t l_USize_add(size_t, size_t); +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg(lean_object*, lean_object*); lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__31; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__59; -lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg___closed__3; -lean_object* l_Lean_Lsp_instToJsonHoverParams(lean_object*); -lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1299_(lean_object*); +lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____spec__2___rarg(lean_object*, size_t, size_t, lean_object*); +lean_object* l_Lean_Lsp_instToJsonHoverParams; +lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonRange____x40_Lean_Data_Lsp_Basic___hyg_387____spec__1(lean_object*, lean_object*); lean_object* lean_array_uget(lean_object*, size_t); +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonHoverParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_87_(lean_object*); lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__61; -lean_object* l_Lean_Lsp_instFromJsonDefinitionParams___boxed(lean_object*); lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__75; lean_object* lean_array_uset(lean_object*, size_t, lean_object*); lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__26; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__58; -lean_object* l_Lean_Lsp_instFromJsonHoverParams___boxed(lean_object*); +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDefinitionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_249____boxed(lean_object*); +lean_object* l_Lean_Lsp_instFromJsonHoverParams___closed__1; lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1299____spec__1(lean_object*, lean_object*); +lean_object* l_Lean_Lsp_instToJsonDefinitionParams___closed__1; extern lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonMarkupContent____x40_Lean_Data_Lsp_Basic___hyg_1626____closed__2; -lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg___closed__1; +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDeclarationParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_168____boxed(lean_object*); lean_object* l_Lean_Lsp_DocumentSymbolAux_children_x3f___default(lean_object*); lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonLocationLink____x40_Lean_Data_Lsp_Basic___hyg_631____spec__1(lean_object*, lean_object*); lean_object* l_Lean_Lsp_instToJsonDocumentSymbolAux___rarg(lean_object*); @@ -37,21 +40,25 @@ lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__12; lean_object* l_Lean_Lsp_instToJsonDocumentSymbol; lean_object* l_Lean_Lsp_instToJsonSymbolKind_match__1(lean_object*); lean_object* lean_array_get_size(lean_object*); -lean_object* l_Lean_Lsp_instFromJsonDeclarationParams(lean_object*); -lean_object* l_Lean_Lsp_instToJsonDefinitionParams(lean_object*); -lean_object* l_Lean_Lsp_instFromJsonDefinitionParams(lean_object*); +lean_object* l_Lean_Lsp_instFromJsonDeclarationParams; +lean_object* l_Lean_Lsp_instToJsonDefinitionParams; +lean_object* l_Lean_Lsp_instFromJsonDefinitionParams; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__71; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__7; lean_object* l_Lean_Json_opt___at_Lean_Lsp_instToJsonDocumentSymbol_go___spec__2(lean_object*, lean_object*); lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__42; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__53; +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDeclarationParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_168_(lean_object*); lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__37; +lean_object* l_Lean_Lsp_instToJsonDeclarationParams___closed__1; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__55; lean_object* l_Lean_Lsp_instToJsonSymbolKind_match__1___rarg___boxed(lean_object**); +lean_object* l_Lean_Lsp_instToJsonTypeDefinitionParams___closed__1; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__3; lean_object* l_List_join___rarg(lean_object*); uint8_t l_USize_decLt(size_t, size_t); lean_object* l_Lean_Lsp_instToJsonHover___closed__1; +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonTypeDefinitionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_374_(lean_object*); lean_object* l_Lean_Lsp_instToJsonDocumentSymbolParams; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__14; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__28; @@ -65,7 +72,7 @@ lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJs lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__10; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__32; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__73; -lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____spec__2(lean_object*); lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__20; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__30; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__43; @@ -74,61 +81,67 @@ lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__56; lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_LanguageFeatures___hyg_11_(lean_object*); lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__16; lean_object* l_Array_mapMUnsafe_map___at_Lean_Lsp_instToJsonDocumentSymbol_go___spec__3(size_t, size_t, lean_object*); -lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg___closed__2; lean_object* l_Lean_Lsp_Hover_range_x3f___default; +lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____spec__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__63; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__24; lean_object* l_Lean_Lsp_instToJsonSymbolKind_match__1___rarg(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_mapMUnsafe_map___at_Lean_Lsp_instToJsonDocumentSymbol_go___spec__3___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__49; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__50; +lean_object* l_Lean_Lsp_instFromJsonDefinitionParams___closed__1; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__6; -lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____spec__2___rarg(lean_object*, size_t, size_t, lean_object*); +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDeclarationParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_212_(lean_object*); +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDefinitionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_249_(lean_object*); lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__34; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__48; lean_object* l_Lean_Lsp_instToJsonSymbolKind(uint8_t); lean_object* l_Lean_Lsp_instFromJsonDocumentSymbolParams; -lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____at_Lean_Lsp_instToJsonDocumentSymbol_go___spec__1(lean_object*); -lean_object* l_Lean_Lsp_instFromJsonTypeDefinitionParams(lean_object*); -lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____spec__1(lean_object*); -lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1265_(lean_object*); -lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg___closed__4; +lean_object* l_Lean_Lsp_instFromJsonTypeDefinitionParams; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__72; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__23; lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonLocationLink____x40_Lean_Data_Lsp_Basic___hyg_584____spec__1(lean_object*, lean_object*); lean_object* l_Lean_Lsp_instToJsonDocumentSymbol_go_match__1(lean_object*); lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__13; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__41; -lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376_(lean_object*); +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548_(lean_object*); +lean_object* l_Lean_Lsp_instFromJsonTypeDefinitionParams___closed__1; lean_object* l_Lean_Lsp_instToJsonDocumentSymbolAux(lean_object*); -lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_239_(lean_object*); +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDefinitionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_293_(lean_object*); +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_411_(lean_object*); lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__38; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__21; lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonHover____x40_Lean_Data_Lsp_LanguageFeatures___hyg_40____boxed(lean_object*); -lean_object* l_Lean_Lsp_instToJsonDeclarationParams(lean_object*); +lean_object* l_Lean_Lsp_instToJsonHoverParams___closed__1; +lean_object* l_Lean_Lsp_instToJsonDeclarationParams; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__22; size_t lean_usize_of_nat(lean_object*); extern lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonLocation____x40_Lean_Data_Lsp_Basic___hyg_499____closed__2; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__62; extern lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentEdit____x40_Lean_Data_Lsp_Basic___hyg_1053____closed__1; +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonHoverParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_87____boxed(lean_object*); lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__54; lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentIdentifier____x40_Lean_Data_Lsp_Basic___hyg_915_(lean_object*); lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__33; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__25; -lean_object* l_Lean_Lsp_instFromJsonDeclarationParams___boxed(lean_object*); +lean_object* l_Lean_Lsp_instFromJsonDeclarationParams___closed__1; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__29; lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonMarkupContent____x40_Lean_Data_Lsp_Basic___hyg_1660_(lean_object*); lean_object* l_Lean_Lsp_DocumentSymbolAux_detail_x3f___default; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__52; +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg___closed__2; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__46; lean_object* l_Lean_Json_getObjValD(lean_object*, lean_object*); -lean_object* l_Lean_Lsp_instFromJsonHoverParams(lean_object*); +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_411____boxed(lean_object*); +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg___closed__1; +lean_object* l_Lean_Lsp_instFromJsonHoverParams; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__65; +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonHoverParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_131_(lean_object*); +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg___closed__4; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__70; +lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__35; -lean_object* l_Lean_Lsp_instFromJsonTypeDefinitionParams___boxed(lean_object*); lean_object* l_Lean_Lsp_instToJsonHover; -lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg(lean_object*, lean_object*); lean_object* l_Lean_Lsp_instToJsonDocumentSymbol_go(lean_object*); lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__36; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__51; @@ -145,32 +158,36 @@ lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__74; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__60; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__47; extern lean_object* l_Lean_JsonNumber_toString___closed__1; -lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_239____boxed(lean_object*); +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg___closed__3; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__44; +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____at_Lean_Lsp_instToJsonDocumentSymbol_go___spec__1(lean_object*); lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonHover____x40_Lean_Data_Lsp_LanguageFeatures___hyg_40____spec__1___boxed(lean_object*, lean_object*); +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonTypeDefinitionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_330_(lean_object*); lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__1; +extern lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1265____closed__1; lean_object* l_Lean_Lsp_instToJsonSymbolKind___boxed(lean_object*); lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonHover____x40_Lean_Data_Lsp_LanguageFeatures___hyg_40_(lean_object*); lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__57; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__17; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__8; -lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_269_(lean_object*); +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_441_(lean_object*); lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonRange____x40_Lean_Data_Lsp_Basic___hyg_353_(lean_object*); lean_object* l_Lean_Lsp_instFromJsonHover; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__45; lean_object* l_Lean_Lsp_instFromJsonHover___closed__1; -lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____spec__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__67; lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____spec__1(lean_object*); lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__9; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__40; +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonTypeDefinitionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_330____boxed(lean_object*); lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__27; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__4; lean_object* l_Lean_Lsp_instToJsonDocumentSymbolParams___closed__1; lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__68; lean_object* l_Lean_Lsp_instToJsonDocumentSymbolResult(lean_object*); -lean_object* l_Lean_Lsp_instToJsonTypeDefinitionParams(lean_object*); -lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____spec__2(lean_object*); +lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonPosition____x40_Lean_Data_Lsp_Basic___hyg_185_(lean_object*); +lean_object* l_Lean_Lsp_instToJsonTypeDefinitionParams; lean_object* l_Lean_Lsp_instFromJsonDocumentSymbolParams___closed__1; lean_object* lean_nat_to_int(lean_object*); lean_object* l_Lean_Lsp_instToJsonDocumentSymbol_go_match__1___rarg(lean_object*, lean_object*); @@ -342,203 +359,551 @@ x_1 = l_Lean_Lsp_instFromJsonHover___closed__1; return x_1; } } -lean_object* l_Lean_Lsp_instFromJsonHoverParams(lean_object* x_1) { +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonHoverParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_87_(lean_object* x_1) { _start: { -lean_object* x_2; -x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1299_(x_1); -if (lean_obj_tag(x_2) == 0) +lean_object* x_2; lean_object* x_3; +x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentEdit____x40_Lean_Data_Lsp_Basic___hyg_1053____closed__1; +x_3 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1299____spec__1(x_1, x_2); +if (lean_obj_tag(x_3) == 0) { -lean_object* x_3; -x_3 = lean_box(0); -return x_3; +lean_object* x_4; +x_4 = lean_box(0); +return x_4; } else { -uint8_t x_4; -x_4 = !lean_is_exclusive(x_2); -if (x_4 == 0) -{ -return x_2; -} -else -{ -lean_object* x_5; lean_object* x_6; -x_5 = lean_ctor_get(x_2, 0); +lean_object* x_5; lean_object* x_6; lean_object* x_7; +x_5 = lean_ctor_get(x_3, 0); lean_inc(x_5); -lean_dec(x_2); -x_6 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_6, 0, x_5); -return x_6; +lean_dec(x_3); +x_6 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1265____closed__1; +x_7 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonRange____x40_Lean_Data_Lsp_Basic___hyg_387____spec__1(x_1, x_6); +if (lean_obj_tag(x_7) == 0) +{ +lean_object* x_8; +lean_dec(x_5); +x_8 = lean_box(0); +return x_8; +} +else +{ +uint8_t x_9; +x_9 = !lean_is_exclusive(x_7); +if (x_9 == 0) +{ +lean_object* x_10; lean_object* x_11; +x_10 = lean_ctor_get(x_7, 0); +x_11 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_11, 0, x_5); +lean_ctor_set(x_11, 1, x_10); +lean_ctor_set(x_7, 0, x_11); +return x_7; +} +else +{ +lean_object* x_12; lean_object* x_13; lean_object* x_14; +x_12 = lean_ctor_get(x_7, 0); +lean_inc(x_12); +lean_dec(x_7); +x_13 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_13, 0, x_5); +lean_ctor_set(x_13, 1, x_12); +x_14 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_14, 0, x_13); +return x_14; } } } } -lean_object* l_Lean_Lsp_instFromJsonHoverParams___boxed(lean_object* x_1) { +} +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonHoverParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_87____boxed(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = l_Lean_Lsp_instFromJsonHoverParams(x_1); +x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonHoverParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_87_(x_1); lean_dec(x_1); return x_2; } } -lean_object* l_Lean_Lsp_instToJsonHoverParams(lean_object* x_1) { +static lean_object* _init_l_Lean_Lsp_instFromJsonHoverParams___closed__1() { _start: { -lean_object* x_2; -x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1265_(x_1); -return x_2; +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonHoverParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_87____boxed), 1, 0); +return x_1; } } -lean_object* l_Lean_Lsp_instFromJsonDeclarationParams(lean_object* x_1) { +static lean_object* _init_l_Lean_Lsp_instFromJsonHoverParams() { _start: { -lean_object* x_2; -x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1299_(x_1); -if (lean_obj_tag(x_2) == 0) +lean_object* x_1; +x_1 = l_Lean_Lsp_instFromJsonHoverParams___closed__1; +return x_1; +} +} +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonHoverParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_131_(lean_object* x_1) { +_start: { -lean_object* x_3; -x_3 = lean_box(0); -return x_3; +lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentIdentifier____x40_Lean_Data_Lsp_Basic___hyg_915_(x_2); +x_4 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentEdit____x40_Lean_Data_Lsp_Basic___hyg_1053____closed__1; +x_5 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_5, 0, x_4); +lean_ctor_set(x_5, 1, x_3); +x_6 = lean_box(0); +x_7 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_7, 0, x_5); +lean_ctor_set(x_7, 1, x_6); +x_8 = lean_ctor_get(x_1, 1); +lean_inc(x_8); +lean_dec(x_1); +x_9 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonPosition____x40_Lean_Data_Lsp_Basic___hyg_185_(x_8); +x_10 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1265____closed__1; +x_11 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_11, 0, x_10); +lean_ctor_set(x_11, 1, x_9); +x_12 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_12, 0, x_11); +lean_ctor_set(x_12, 1, x_6); +x_13 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_13, 0, x_12); +lean_ctor_set(x_13, 1, x_6); +x_14 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_14, 0, x_7); +lean_ctor_set(x_14, 1, x_13); +x_15 = l_List_join___rarg(x_14); +x_16 = l_Lean_Json_mkObj(x_15); +return x_16; +} +} +static lean_object* _init_l_Lean_Lsp_instToJsonHoverParams___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonHoverParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_131_), 1, 0); +return x_1; +} +} +static lean_object* _init_l_Lean_Lsp_instToJsonHoverParams() { +_start: +{ +lean_object* x_1; +x_1 = l_Lean_Lsp_instToJsonHoverParams___closed__1; +return x_1; +} +} +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDeclarationParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_168_(lean_object* x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; +x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentEdit____x40_Lean_Data_Lsp_Basic___hyg_1053____closed__1; +x_3 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1299____spec__1(x_1, x_2); +if (lean_obj_tag(x_3) == 0) +{ +lean_object* x_4; +x_4 = lean_box(0); +return x_4; } else { -uint8_t x_4; -x_4 = !lean_is_exclusive(x_2); -if (x_4 == 0) -{ -return x_2; -} -else -{ -lean_object* x_5; lean_object* x_6; -x_5 = lean_ctor_get(x_2, 0); +lean_object* x_5; lean_object* x_6; lean_object* x_7; +x_5 = lean_ctor_get(x_3, 0); lean_inc(x_5); -lean_dec(x_2); -x_6 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_6, 0, x_5); -return x_6; +lean_dec(x_3); +x_6 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1265____closed__1; +x_7 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonRange____x40_Lean_Data_Lsp_Basic___hyg_387____spec__1(x_1, x_6); +if (lean_obj_tag(x_7) == 0) +{ +lean_object* x_8; +lean_dec(x_5); +x_8 = lean_box(0); +return x_8; +} +else +{ +uint8_t x_9; +x_9 = !lean_is_exclusive(x_7); +if (x_9 == 0) +{ +lean_object* x_10; lean_object* x_11; +x_10 = lean_ctor_get(x_7, 0); +x_11 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_11, 0, x_5); +lean_ctor_set(x_11, 1, x_10); +lean_ctor_set(x_7, 0, x_11); +return x_7; +} +else +{ +lean_object* x_12; lean_object* x_13; lean_object* x_14; +x_12 = lean_ctor_get(x_7, 0); +lean_inc(x_12); +lean_dec(x_7); +x_13 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_13, 0, x_5); +lean_ctor_set(x_13, 1, x_12); +x_14 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_14, 0, x_13); +return x_14; } } } } -lean_object* l_Lean_Lsp_instFromJsonDeclarationParams___boxed(lean_object* x_1) { +} +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDeclarationParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_168____boxed(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = l_Lean_Lsp_instFromJsonDeclarationParams(x_1); +x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDeclarationParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_168_(x_1); lean_dec(x_1); return x_2; } } -lean_object* l_Lean_Lsp_instToJsonDeclarationParams(lean_object* x_1) { +static lean_object* _init_l_Lean_Lsp_instFromJsonDeclarationParams___closed__1() { _start: { -lean_object* x_2; -x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1265_(x_1); -return x_2; +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDeclarationParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_168____boxed), 1, 0); +return x_1; } } -lean_object* l_Lean_Lsp_instFromJsonDefinitionParams(lean_object* x_1) { +static lean_object* _init_l_Lean_Lsp_instFromJsonDeclarationParams() { _start: { -lean_object* x_2; -x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1299_(x_1); -if (lean_obj_tag(x_2) == 0) +lean_object* x_1; +x_1 = l_Lean_Lsp_instFromJsonDeclarationParams___closed__1; +return x_1; +} +} +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDeclarationParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_212_(lean_object* x_1) { +_start: { -lean_object* x_3; -x_3 = lean_box(0); -return x_3; +lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentIdentifier____x40_Lean_Data_Lsp_Basic___hyg_915_(x_2); +x_4 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentEdit____x40_Lean_Data_Lsp_Basic___hyg_1053____closed__1; +x_5 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_5, 0, x_4); +lean_ctor_set(x_5, 1, x_3); +x_6 = lean_box(0); +x_7 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_7, 0, x_5); +lean_ctor_set(x_7, 1, x_6); +x_8 = lean_ctor_get(x_1, 1); +lean_inc(x_8); +lean_dec(x_1); +x_9 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonPosition____x40_Lean_Data_Lsp_Basic___hyg_185_(x_8); +x_10 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1265____closed__1; +x_11 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_11, 0, x_10); +lean_ctor_set(x_11, 1, x_9); +x_12 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_12, 0, x_11); +lean_ctor_set(x_12, 1, x_6); +x_13 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_13, 0, x_12); +lean_ctor_set(x_13, 1, x_6); +x_14 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_14, 0, x_7); +lean_ctor_set(x_14, 1, x_13); +x_15 = l_List_join___rarg(x_14); +x_16 = l_Lean_Json_mkObj(x_15); +return x_16; +} +} +static lean_object* _init_l_Lean_Lsp_instToJsonDeclarationParams___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDeclarationParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_212_), 1, 0); +return x_1; +} +} +static lean_object* _init_l_Lean_Lsp_instToJsonDeclarationParams() { +_start: +{ +lean_object* x_1; +x_1 = l_Lean_Lsp_instToJsonDeclarationParams___closed__1; +return x_1; +} +} +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDefinitionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_249_(lean_object* x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; +x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentEdit____x40_Lean_Data_Lsp_Basic___hyg_1053____closed__1; +x_3 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1299____spec__1(x_1, x_2); +if (lean_obj_tag(x_3) == 0) +{ +lean_object* x_4; +x_4 = lean_box(0); +return x_4; } else { -uint8_t x_4; -x_4 = !lean_is_exclusive(x_2); -if (x_4 == 0) -{ -return x_2; -} -else -{ -lean_object* x_5; lean_object* x_6; -x_5 = lean_ctor_get(x_2, 0); +lean_object* x_5; lean_object* x_6; lean_object* x_7; +x_5 = lean_ctor_get(x_3, 0); lean_inc(x_5); -lean_dec(x_2); -x_6 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_6, 0, x_5); -return x_6; +lean_dec(x_3); +x_6 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1265____closed__1; +x_7 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonRange____x40_Lean_Data_Lsp_Basic___hyg_387____spec__1(x_1, x_6); +if (lean_obj_tag(x_7) == 0) +{ +lean_object* x_8; +lean_dec(x_5); +x_8 = lean_box(0); +return x_8; +} +else +{ +uint8_t x_9; +x_9 = !lean_is_exclusive(x_7); +if (x_9 == 0) +{ +lean_object* x_10; lean_object* x_11; +x_10 = lean_ctor_get(x_7, 0); +x_11 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_11, 0, x_5); +lean_ctor_set(x_11, 1, x_10); +lean_ctor_set(x_7, 0, x_11); +return x_7; +} +else +{ +lean_object* x_12; lean_object* x_13; lean_object* x_14; +x_12 = lean_ctor_get(x_7, 0); +lean_inc(x_12); +lean_dec(x_7); +x_13 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_13, 0, x_5); +lean_ctor_set(x_13, 1, x_12); +x_14 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_14, 0, x_13); +return x_14; } } } } -lean_object* l_Lean_Lsp_instFromJsonDefinitionParams___boxed(lean_object* x_1) { +} +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDefinitionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_249____boxed(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = l_Lean_Lsp_instFromJsonDefinitionParams(x_1); +x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDefinitionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_249_(x_1); lean_dec(x_1); return x_2; } } -lean_object* l_Lean_Lsp_instToJsonDefinitionParams(lean_object* x_1) { +static lean_object* _init_l_Lean_Lsp_instFromJsonDefinitionParams___closed__1() { _start: { -lean_object* x_2; -x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1265_(x_1); -return x_2; +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDefinitionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_249____boxed), 1, 0); +return x_1; } } -lean_object* l_Lean_Lsp_instFromJsonTypeDefinitionParams(lean_object* x_1) { +static lean_object* _init_l_Lean_Lsp_instFromJsonDefinitionParams() { _start: { -lean_object* x_2; -x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1299_(x_1); -if (lean_obj_tag(x_2) == 0) +lean_object* x_1; +x_1 = l_Lean_Lsp_instFromJsonDefinitionParams___closed__1; +return x_1; +} +} +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDefinitionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_293_(lean_object* x_1) { +_start: { -lean_object* x_3; -x_3 = lean_box(0); -return x_3; +lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentIdentifier____x40_Lean_Data_Lsp_Basic___hyg_915_(x_2); +x_4 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentEdit____x40_Lean_Data_Lsp_Basic___hyg_1053____closed__1; +x_5 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_5, 0, x_4); +lean_ctor_set(x_5, 1, x_3); +x_6 = lean_box(0); +x_7 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_7, 0, x_5); +lean_ctor_set(x_7, 1, x_6); +x_8 = lean_ctor_get(x_1, 1); +lean_inc(x_8); +lean_dec(x_1); +x_9 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonPosition____x40_Lean_Data_Lsp_Basic___hyg_185_(x_8); +x_10 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1265____closed__1; +x_11 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_11, 0, x_10); +lean_ctor_set(x_11, 1, x_9); +x_12 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_12, 0, x_11); +lean_ctor_set(x_12, 1, x_6); +x_13 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_13, 0, x_12); +lean_ctor_set(x_13, 1, x_6); +x_14 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_14, 0, x_7); +lean_ctor_set(x_14, 1, x_13); +x_15 = l_List_join___rarg(x_14); +x_16 = l_Lean_Json_mkObj(x_15); +return x_16; +} +} +static lean_object* _init_l_Lean_Lsp_instToJsonDefinitionParams___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDefinitionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_293_), 1, 0); +return x_1; +} +} +static lean_object* _init_l_Lean_Lsp_instToJsonDefinitionParams() { +_start: +{ +lean_object* x_1; +x_1 = l_Lean_Lsp_instToJsonDefinitionParams___closed__1; +return x_1; +} +} +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonTypeDefinitionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_330_(lean_object* x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; +x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentEdit____x40_Lean_Data_Lsp_Basic___hyg_1053____closed__1; +x_3 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1299____spec__1(x_1, x_2); +if (lean_obj_tag(x_3) == 0) +{ +lean_object* x_4; +x_4 = lean_box(0); +return x_4; } else { -uint8_t x_4; -x_4 = !lean_is_exclusive(x_2); -if (x_4 == 0) -{ -return x_2; -} -else -{ -lean_object* x_5; lean_object* x_6; -x_5 = lean_ctor_get(x_2, 0); +lean_object* x_5; lean_object* x_6; lean_object* x_7; +x_5 = lean_ctor_get(x_3, 0); lean_inc(x_5); -lean_dec(x_2); -x_6 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_6, 0, x_5); -return x_6; +lean_dec(x_3); +x_6 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1265____closed__1; +x_7 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonRange____x40_Lean_Data_Lsp_Basic___hyg_387____spec__1(x_1, x_6); +if (lean_obj_tag(x_7) == 0) +{ +lean_object* x_8; +lean_dec(x_5); +x_8 = lean_box(0); +return x_8; +} +else +{ +uint8_t x_9; +x_9 = !lean_is_exclusive(x_7); +if (x_9 == 0) +{ +lean_object* x_10; lean_object* x_11; +x_10 = lean_ctor_get(x_7, 0); +x_11 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_11, 0, x_5); +lean_ctor_set(x_11, 1, x_10); +lean_ctor_set(x_7, 0, x_11); +return x_7; +} +else +{ +lean_object* x_12; lean_object* x_13; lean_object* x_14; +x_12 = lean_ctor_get(x_7, 0); +lean_inc(x_12); +lean_dec(x_7); +x_13 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_13, 0, x_5); +lean_ctor_set(x_13, 1, x_12); +x_14 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_14, 0, x_13); +return x_14; } } } } -lean_object* l_Lean_Lsp_instFromJsonTypeDefinitionParams___boxed(lean_object* x_1) { +} +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonTypeDefinitionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_330____boxed(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = l_Lean_Lsp_instFromJsonTypeDefinitionParams(x_1); +x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonTypeDefinitionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_330_(x_1); lean_dec(x_1); return x_2; } } -lean_object* l_Lean_Lsp_instToJsonTypeDefinitionParams(lean_object* x_1) { +static lean_object* _init_l_Lean_Lsp_instFromJsonTypeDefinitionParams___closed__1() { _start: { -lean_object* x_2; -x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1265_(x_1); -return x_2; +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonTypeDefinitionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_330____boxed), 1, 0); +return x_1; } } -lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_239_(lean_object* x_1) { +static lean_object* _init_l_Lean_Lsp_instFromJsonTypeDefinitionParams() { +_start: +{ +lean_object* x_1; +x_1 = l_Lean_Lsp_instFromJsonTypeDefinitionParams___closed__1; +return x_1; +} +} +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonTypeDefinitionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_374_(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; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentIdentifier____x40_Lean_Data_Lsp_Basic___hyg_915_(x_2); +x_4 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentEdit____x40_Lean_Data_Lsp_Basic___hyg_1053____closed__1; +x_5 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_5, 0, x_4); +lean_ctor_set(x_5, 1, x_3); +x_6 = lean_box(0); +x_7 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_7, 0, x_5); +lean_ctor_set(x_7, 1, x_6); +x_8 = lean_ctor_get(x_1, 1); +lean_inc(x_8); +lean_dec(x_1); +x_9 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonPosition____x40_Lean_Data_Lsp_Basic___hyg_185_(x_8); +x_10 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1265____closed__1; +x_11 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_11, 0, x_10); +lean_ctor_set(x_11, 1, x_9); +x_12 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_12, 0, x_11); +lean_ctor_set(x_12, 1, x_6); +x_13 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_13, 0, x_12); +lean_ctor_set(x_13, 1, x_6); +x_14 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_14, 0, x_7); +lean_ctor_set(x_14, 1, x_13); +x_15 = l_List_join___rarg(x_14); +x_16 = l_Lean_Json_mkObj(x_15); +return x_16; +} +} +static lean_object* _init_l_Lean_Lsp_instToJsonTypeDefinitionParams___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonTypeDefinitionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_374_), 1, 0); +return x_1; +} +} +static lean_object* _init_l_Lean_Lsp_instToJsonTypeDefinitionParams() { +_start: +{ +lean_object* x_1; +x_1 = l_Lean_Lsp_instToJsonTypeDefinitionParams___closed__1; +return x_1; +} +} +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_411_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; @@ -571,11 +936,11 @@ return x_7; } } } -lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_239____boxed(lean_object* x_1) { +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_411____boxed(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_239_(x_1); +x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_411_(x_1); lean_dec(x_1); return x_2; } @@ -584,7 +949,7 @@ static lean_object* _init_l_Lean_Lsp_instFromJsonDocumentSymbolParams___closed__ _start: { lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_239____boxed), 1, 0); +x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_411____boxed), 1, 0); return x_1; } } @@ -596,7 +961,7 @@ x_1 = l_Lean_Lsp_instFromJsonDocumentSymbolParams___closed__1; return x_1; } } -lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_269_(lean_object* x_1) { +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_441_(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; lean_object* x_7; lean_object* x_8; lean_object* x_9; @@ -621,7 +986,7 @@ static lean_object* _init_l_Lean_Lsp_instToJsonDocumentSymbolParams___closed__1( _start: { lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_269_), 1, 0); +x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_441_), 1, 0); return x_1; } } @@ -2494,7 +2859,7 @@ x_2 = lean_box(0); return x_2; } } -lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____spec__2___rarg(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) { +lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____spec__2___rarg(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) { _start: { uint8_t x_5; @@ -2525,15 +2890,15 @@ goto _start; } } } -lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____spec__2(lean_object* x_1) { +lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____spec__2(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____spec__2___rarg___boxed), 4, 0); +x_2 = lean_alloc_closure((void*)(l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____spec__2___rarg___boxed), 4, 0); return x_2; } } -lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { if (lean_obj_tag(x_3) == 0) @@ -2555,7 +2920,7 @@ x_7 = lean_usize_of_nat(x_6); lean_dec(x_6); x_8 = 0; x_9 = x_5; -x_10 = l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____spec__2___rarg(x_1, x_7, x_8, x_9); +x_10 = l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____spec__2___rarg(x_1, x_7, x_8, x_9); x_11 = x_10; x_12 = lean_alloc_ctor(4, 1, 0); lean_ctor_set(x_12, 0, x_11); @@ -2570,15 +2935,15 @@ return x_15; } } } -lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____spec__1(lean_object* x_1) { +lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____spec__1(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_Lean_Json_opt___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____spec__1___rarg), 3, 0); +x_2 = lean_alloc_closure((void*)(l_Lean_Json_opt___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____spec__1___rarg), 3, 0); return x_2; } } -static lean_object* _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg___closed__1() { +static lean_object* _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg___closed__1() { _start: { lean_object* x_1; @@ -2586,7 +2951,7 @@ x_1 = lean_mk_string("name"); return x_1; } } -static lean_object* _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg___closed__2() { +static lean_object* _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg___closed__2() { _start: { lean_object* x_1; @@ -2594,7 +2959,7 @@ x_1 = lean_mk_string("detail"); return x_1; } } -static lean_object* _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg___closed__3() { +static lean_object* _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg___closed__3() { _start: { lean_object* x_1; @@ -2602,7 +2967,7 @@ x_1 = lean_mk_string("selectionRange"); return x_1; } } -static lean_object* _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg___closed__4() { +static lean_object* _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg___closed__4() { _start: { lean_object* x_1; @@ -2610,7 +2975,7 @@ x_1 = lean_mk_string("children"); return x_1; } } -lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg(lean_object* x_1, lean_object* x_2) { +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; lean_object* x_4; uint8_t x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; @@ -2628,7 +2993,7 @@ lean_inc(x_8); lean_dec(x_2); x_9 = lean_alloc_ctor(3, 1, 0); lean_ctor_set(x_9, 0, x_3); -x_10 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg___closed__1; +x_10 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg___closed__1; x_11 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_11, 0, x_10); lean_ctor_set(x_11, 1, x_9); @@ -2636,7 +3001,7 @@ x_12 = lean_box(0); x_13 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_13, 0, x_11); lean_ctor_set(x_13, 1, x_12); -x_14 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg___closed__2; +x_14 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg___closed__2; x_15 = l_Lean_Json_opt___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonDocumentFilter____x40_Lean_Data_Lsp_Basic___hyg_1354____spec__1(x_14, x_4); lean_dec(x_4); x_16 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonRange____x40_Lean_Data_Lsp_Basic___hyg_353_(x_6); @@ -2648,15 +3013,15 @@ x_19 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_19, 0, x_18); lean_ctor_set(x_19, 1, x_12); x_20 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonRange____x40_Lean_Data_Lsp_Basic___hyg_353_(x_7); -x_21 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg___closed__3; +x_21 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg___closed__3; x_22 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_22, 0, x_21); lean_ctor_set(x_22, 1, x_20); x_23 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_23, 0, x_22); lean_ctor_set(x_23, 1, x_12); -x_24 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg___closed__4; -x_25 = l_Lean_Json_opt___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____spec__1___rarg(x_1, x_24, x_8); +x_24 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg___closed__4; +x_25 = l_Lean_Json_opt___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____spec__1___rarg(x_1, x_24, x_8); x_26 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_26, 0, x_25); lean_ctor_set(x_26, 1, x_12); @@ -2875,15 +3240,15 @@ return x_37; } } } -lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376_(lean_object* x_1) { +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548_(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg), 2, 0); +x_2 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg), 2, 0); return x_2; } } -lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____spec__2___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____spec__2___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { size_t x_5; size_t x_6; lean_object* x_7; @@ -2891,7 +3256,7 @@ x_5 = lean_unbox_usize(x_2); lean_dec(x_2); x_6 = lean_unbox_usize(x_3); lean_dec(x_3); -x_7 = l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____spec__2___rarg(x_1, x_5, x_6, x_4); +x_7 = l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____spec__2___rarg(x_1, x_5, x_6, x_4); return x_7; } } @@ -2899,7 +3264,7 @@ lean_object* l_Lean_Lsp_instToJsonDocumentSymbolAux___rarg(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg), 2, 1); +x_2 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg), 2, 1); lean_closure_set(x_2, 0, x_1); return x_2; } @@ -2946,7 +3311,7 @@ x_6 = lean_array_uget(x_3, x_2); x_7 = lean_unsigned_to_nat(0u); x_8 = lean_array_uset(x_3, x_2, x_7); x_9 = x_6; -x_10 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____at_Lean_Lsp_instToJsonDocumentSymbol_go___spec__1(x_9); +x_10 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____at_Lean_Lsp_instToJsonDocumentSymbol_go___spec__1(x_9); x_11 = 1; x_12 = x_2 + x_11; x_13 = x_10; @@ -2993,7 +3358,7 @@ return x_14; } } } -lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____at_Lean_Lsp_instToJsonDocumentSymbol_go___spec__1(lean_object* x_1) { +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____at_Lean_Lsp_instToJsonDocumentSymbol_go___spec__1(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; @@ -3011,7 +3376,7 @@ lean_inc(x_7); lean_dec(x_1); x_8 = lean_alloc_ctor(3, 1, 0); lean_ctor_set(x_8, 0, x_2); -x_9 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg___closed__1; +x_9 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg___closed__1; x_10 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_10, 0, x_9); lean_ctor_set(x_10, 1, x_8); @@ -3019,7 +3384,7 @@ x_11 = lean_box(0); x_12 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_12, 0, x_10); lean_ctor_set(x_12, 1, x_11); -x_13 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg___closed__2; +x_13 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg___closed__2; x_14 = l_Lean_Json_opt___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonDocumentFilter____x40_Lean_Data_Lsp_Basic___hyg_1354____spec__1(x_13, x_3); lean_dec(x_3); x_15 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonRange____x40_Lean_Data_Lsp_Basic___hyg_353_(x_5); @@ -3031,14 +3396,14 @@ x_18 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_18, 0, x_17); lean_ctor_set(x_18, 1, x_11); x_19 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonRange____x40_Lean_Data_Lsp_Basic___hyg_353_(x_6); -x_20 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg___closed__3; +x_20 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg___closed__3; x_21 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_21, 0, x_20); lean_ctor_set(x_21, 1, x_19); x_22 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_22, 0, x_21); lean_ctor_set(x_22, 1, x_11); -x_23 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg___closed__4; +x_23 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg___closed__4; x_24 = l_Lean_Json_opt___at_Lean_Lsp_instToJsonDocumentSymbol_go___spec__2(x_23, x_7); x_25 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_25, 0, x_24); @@ -3262,7 +3627,7 @@ lean_object* l_Lean_Lsp_instToJsonDocumentSymbol_go(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____at_Lean_Lsp_instToJsonDocumentSymbol_go___spec__1(x_1); +x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____at_Lean_Lsp_instToJsonDocumentSymbol_go___spec__1(x_1); return x_2; } } @@ -3339,6 +3704,38 @@ l_Lean_Lsp_instFromJsonHover___closed__1 = _init_l_Lean_Lsp_instFromJsonHover___ lean_mark_persistent(l_Lean_Lsp_instFromJsonHover___closed__1); l_Lean_Lsp_instFromJsonHover = _init_l_Lean_Lsp_instFromJsonHover(); lean_mark_persistent(l_Lean_Lsp_instFromJsonHover); +l_Lean_Lsp_instFromJsonHoverParams___closed__1 = _init_l_Lean_Lsp_instFromJsonHoverParams___closed__1(); +lean_mark_persistent(l_Lean_Lsp_instFromJsonHoverParams___closed__1); +l_Lean_Lsp_instFromJsonHoverParams = _init_l_Lean_Lsp_instFromJsonHoverParams(); +lean_mark_persistent(l_Lean_Lsp_instFromJsonHoverParams); +l_Lean_Lsp_instToJsonHoverParams___closed__1 = _init_l_Lean_Lsp_instToJsonHoverParams___closed__1(); +lean_mark_persistent(l_Lean_Lsp_instToJsonHoverParams___closed__1); +l_Lean_Lsp_instToJsonHoverParams = _init_l_Lean_Lsp_instToJsonHoverParams(); +lean_mark_persistent(l_Lean_Lsp_instToJsonHoverParams); +l_Lean_Lsp_instFromJsonDeclarationParams___closed__1 = _init_l_Lean_Lsp_instFromJsonDeclarationParams___closed__1(); +lean_mark_persistent(l_Lean_Lsp_instFromJsonDeclarationParams___closed__1); +l_Lean_Lsp_instFromJsonDeclarationParams = _init_l_Lean_Lsp_instFromJsonDeclarationParams(); +lean_mark_persistent(l_Lean_Lsp_instFromJsonDeclarationParams); +l_Lean_Lsp_instToJsonDeclarationParams___closed__1 = _init_l_Lean_Lsp_instToJsonDeclarationParams___closed__1(); +lean_mark_persistent(l_Lean_Lsp_instToJsonDeclarationParams___closed__1); +l_Lean_Lsp_instToJsonDeclarationParams = _init_l_Lean_Lsp_instToJsonDeclarationParams(); +lean_mark_persistent(l_Lean_Lsp_instToJsonDeclarationParams); +l_Lean_Lsp_instFromJsonDefinitionParams___closed__1 = _init_l_Lean_Lsp_instFromJsonDefinitionParams___closed__1(); +lean_mark_persistent(l_Lean_Lsp_instFromJsonDefinitionParams___closed__1); +l_Lean_Lsp_instFromJsonDefinitionParams = _init_l_Lean_Lsp_instFromJsonDefinitionParams(); +lean_mark_persistent(l_Lean_Lsp_instFromJsonDefinitionParams); +l_Lean_Lsp_instToJsonDefinitionParams___closed__1 = _init_l_Lean_Lsp_instToJsonDefinitionParams___closed__1(); +lean_mark_persistent(l_Lean_Lsp_instToJsonDefinitionParams___closed__1); +l_Lean_Lsp_instToJsonDefinitionParams = _init_l_Lean_Lsp_instToJsonDefinitionParams(); +lean_mark_persistent(l_Lean_Lsp_instToJsonDefinitionParams); +l_Lean_Lsp_instFromJsonTypeDefinitionParams___closed__1 = _init_l_Lean_Lsp_instFromJsonTypeDefinitionParams___closed__1(); +lean_mark_persistent(l_Lean_Lsp_instFromJsonTypeDefinitionParams___closed__1); +l_Lean_Lsp_instFromJsonTypeDefinitionParams = _init_l_Lean_Lsp_instFromJsonTypeDefinitionParams(); +lean_mark_persistent(l_Lean_Lsp_instFromJsonTypeDefinitionParams); +l_Lean_Lsp_instToJsonTypeDefinitionParams___closed__1 = _init_l_Lean_Lsp_instToJsonTypeDefinitionParams___closed__1(); +lean_mark_persistent(l_Lean_Lsp_instToJsonTypeDefinitionParams___closed__1); +l_Lean_Lsp_instToJsonTypeDefinitionParams = _init_l_Lean_Lsp_instToJsonTypeDefinitionParams(); +lean_mark_persistent(l_Lean_Lsp_instToJsonTypeDefinitionParams); l_Lean_Lsp_instFromJsonDocumentSymbolParams___closed__1 = _init_l_Lean_Lsp_instFromJsonDocumentSymbolParams___closed__1(); lean_mark_persistent(l_Lean_Lsp_instFromJsonDocumentSymbolParams___closed__1); l_Lean_Lsp_instFromJsonDocumentSymbolParams = _init_l_Lean_Lsp_instFromJsonDocumentSymbolParams(); @@ -3501,14 +3898,14 @@ l_Lean_Lsp_instToJsonSymbolKind___closed__76 = _init_l_Lean_Lsp_instToJsonSymbol lean_mark_persistent(l_Lean_Lsp_instToJsonSymbolKind___closed__76); l_Lean_Lsp_DocumentSymbolAux_detail_x3f___default = _init_l_Lean_Lsp_DocumentSymbolAux_detail_x3f___default(); lean_mark_persistent(l_Lean_Lsp_DocumentSymbolAux_detail_x3f___default); -l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg___closed__1 = _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg___closed__1(); -lean_mark_persistent(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg___closed__1); -l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg___closed__2 = _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg___closed__2(); -lean_mark_persistent(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg___closed__2); -l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg___closed__3 = _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg___closed__3(); -lean_mark_persistent(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg___closed__3); -l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg___closed__4 = _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg___closed__4(); -lean_mark_persistent(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_376____rarg___closed__4); +l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg___closed__1 = _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg___closed__1(); +lean_mark_persistent(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg___closed__1); +l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg___closed__2 = _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg___closed__2(); +lean_mark_persistent(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg___closed__2); +l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg___closed__3 = _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg___closed__3(); +lean_mark_persistent(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg___closed__3); +l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg___closed__4 = _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg___closed__4(); +lean_mark_persistent(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_548____rarg___closed__4); l_Lean_Lsp_instToJsonDocumentSymbol___closed__1 = _init_l_Lean_Lsp_instToJsonDocumentSymbol___closed__1(); lean_mark_persistent(l_Lean_Lsp_instToJsonDocumentSymbol___closed__1); l_Lean_Lsp_instToJsonDocumentSymbol = _init_l_Lean_Lsp_instToJsonDocumentSymbol(); diff --git a/stage0/stdlib/Lean/Elab/Binders.c b/stage0/stdlib/Lean/Elab/Binders.c index 69ce91e763..cb13dc4af7 100644 --- a/stage0/stdlib/Lean/Elab/Binders.c +++ b/stage0/stdlib/Lean/Elab/Binders.c @@ -33,8 +33,10 @@ extern lean_object* l_Array_term_____x5b___x3a___x5d___closed__2; lean_object* l_Lean_Elab_Term_quoteAutoTactic___closed__3; extern lean_object* l_myMacro____x40_Init_Notation___hyg_14424____closed__12; lean_object* l_Lean_registerTraceClass(lean_object*, lean_object*); +lean_object* lean_erase_macro_scopes(lean_object*); lean_object* l_Lean_Elab_Term_expandWhereDecls___closed__1; lean_object* l_Lean_Elab_Term_elabLetDeclAux___lambda__1___closed__3; +lean_object* l_Lean_stringToMessageData(lean_object*); lean_object* l_Lean_Elab_Term_elabDepArrow___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_matchBinder___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_expandFunBinders_loop_match__2(lean_object*); @@ -113,6 +115,7 @@ lean_object* l___regBuiltin_Lean_Elab_Term_elabArrow___closed__1; lean_object* l_Lean_Elab_Term_quoteAutoTactic___closed__4; extern lean_object* l_Lean_MessageData_nil; lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_registerFailedToInferBinderTypeInfo___closed__2; +lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___closed__3; lean_object* l_Lean_Elab_Term_elabFunBinders___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_declareTacticSyntax___closed__2; lean_object* l_Lean_Elab_Term_quoteAutoTactic___closed__22; @@ -163,6 +166,8 @@ extern lean_object* l_Lean_Parser_Term_binderTactic___elambda__1___closed__2; lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_FunBinders_elabFunBinderViews(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_Term_elabArrow(lean_object*); lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_myMacro____x40_Init_Notation___hyg_14642__expandListLit___spec__1(lean_object*, lean_object*); +lean_object* l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_myMacro____x40_Init_Notation___hyg_13855____closed__9; lean_object* l_Lean_Elab_Term_elabLetDeclAux___lambda__2___closed__1; lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandBinderModifier___closed__2; @@ -225,7 +230,7 @@ lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_addLocalVarInfo(lea lean_object* l_Lean_Meta_mkLambdaFVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_getFunBinderIds_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Syntax_addPrec___closed__5; -lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Binders___hyg_5310_(lean_object*); +lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Binders___hyg_5373_(lean_object*); extern lean_object* l_myMacro____x40_Init_Notation___hyg_12938____closed__12; lean_object* l_Lean_Elab_Term_quoteAutoTactic___closed__20; lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandBinderModifier___closed__8; @@ -273,6 +278,7 @@ extern lean_object* l_myMacro____x40_Init_Notation___hyg_2191____closed__2; lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_matchBinder___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_getCurrMacroScope(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandMatchAltsIntoMatchAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +uint8_t l_Lean_Name_isAtomic(lean_object*); lean_object* l_Lean_Meta_withLocalDecl___at_Lean_Elab_Term_elabLetDeclAux___spec__2(lean_object*); lean_object* l_Lean_Elab_Term_expandOptType(lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_registerFailedToInferBinderTypeInfo___closed__3; @@ -376,11 +382,14 @@ lean_object* l_Lean_mkApp(lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_expandFunBinders_loop_match__1(lean_object*); extern lean_object* l_myMacro____x40_Init_Notation___hyg_12336____closed__10; extern lean_object* l_Lean_Parser_Term_explicitBinder___elambda__1___closed__1; +lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Syntax_getArgs(lean_object*); lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandMatchAltsIntoMatchAux___spec__1(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*); lean_object* l_instInhabitedReaderT___rarg___boxed(lean_object*, lean_object*); lean_object* l_Lean_Syntax_getKind(lean_object*); +lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___closed__1; lean_object* l_Lean_Meta_saveAndResetSynthInstanceCache___rarg(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___closed__2; lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_FunBinders_propagateExpectedType_match__1(lean_object*); extern lean_object* l_myMacro____x40_Init_Notation___hyg_2191____closed__1; lean_object* l_Lean_Elab_Term_expandMatchAltsWhereDecls_loop_match__1(lean_object*); @@ -394,6 +403,7 @@ lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_quoteAutoTactic___spec extern lean_object* l_Lean_Parser_Tactic_match___elambda__1___closed__1; lean_object* l_Lean_Elab_Term_elabLetDeclCore_match__2(lean_object*); lean_object* l_Lean_Elab_Term_quoteAutoTactic___closed__12; +lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_quoteAutoTactic_match__1(lean_object*); lean_object* l_Lean_Meta_forallBoundedTelescope___at_Lean_Elab_Term_elabLetDeclAux___spec__1(lean_object*); lean_object* l_Lean_Elab_Term_elabLetDeclAux___lambda__1___closed__2; @@ -404,6 +414,7 @@ lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_expandFunBinders_loop___ lean_object* l_Lean_Elab_Term_mkExplicitBinder(lean_object*, lean_object*); extern lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_checkTypesAndAssign___closed__8; lean_object* l_Lean_Elab_Term_adaptExpander(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___closed__4; lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_FunBinders_elabFunBinderViews___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Term_quoteAutoTactic___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_FunBinders_elabFunBindersAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -449,6 +460,7 @@ lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_matchBinder___boxed lean_object* l_Lean_Elab_Term_expandWhereDecls_match__1(lean_object*); lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_getBinderIds___spec__1___closed__3; lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_elabForall___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_myMacro____x40_Init_Notation___hyg_1264____closed__7; lean_object* l_ReaderT_instMonadReaderT___rarg(lean_object*); lean_object* l_Lean_Elab_Term_quoteAutoTactic___closed__17; @@ -5110,6 +5122,157 @@ lean_dec(x_3); return x_10; } } +lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) { +_start: +{ +uint8_t x_10; +x_10 = !lean_is_exclusive(x_7); +if (x_10 == 0) +{ +lean_object* x_11; lean_object* x_12; lean_object* x_13; +x_11 = lean_ctor_get(x_7, 3); +x_12 = l_Lean_replaceRef(x_1, x_11); +lean_dec(x_11); +lean_ctor_set(x_7, 3, x_12); +x_13 = l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1(x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9); +lean_dec(x_7); +return x_13; +} +else +{ +lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; +x_14 = lean_ctor_get(x_7, 0); +x_15 = lean_ctor_get(x_7, 1); +x_16 = lean_ctor_get(x_7, 2); +x_17 = lean_ctor_get(x_7, 3); +x_18 = lean_ctor_get(x_7, 4); +x_19 = lean_ctor_get(x_7, 5); +x_20 = lean_ctor_get(x_7, 6); +x_21 = lean_ctor_get(x_7, 7); +lean_inc(x_21); +lean_inc(x_20); +lean_inc(x_19); +lean_inc(x_18); +lean_inc(x_17); +lean_inc(x_16); +lean_inc(x_15); +lean_inc(x_14); +lean_dec(x_7); +x_22 = l_Lean_replaceRef(x_1, x_17); +lean_dec(x_17); +x_23 = lean_alloc_ctor(0, 8, 0); +lean_ctor_set(x_23, 0, x_14); +lean_ctor_set(x_23, 1, x_15); +lean_ctor_set(x_23, 2, x_16); +lean_ctor_set(x_23, 3, x_22); +lean_ctor_set(x_23, 4, x_18); +lean_ctor_set(x_23, 5, x_19); +lean_ctor_set(x_23, 6, x_20); +lean_ctor_set(x_23, 7, x_21); +x_24 = l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1(x_2, x_3, x_4, x_5, x_6, x_23, x_8, x_9); +lean_dec(x_23); +return x_24; +} +} +} +static lean_object* _init_l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("invalid binder name '"); +return x_1; +} +} +static lean_object* _init_l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___closed__1; +x_2 = l_Lean_stringToMessageData(x_1); +return x_2; +} +} +static lean_object* _init_l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("', it must be atomic"); +return x_1; +} +} +static lean_object* _init_l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___closed__3; +x_2 = l_Lean_stringToMessageData(x_1); +return x_2; +} +} +lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) { +_start: +{ +lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12; +x_9 = lean_ctor_get(x_1, 0); +x_10 = l_Lean_Syntax_getId(x_9); +x_11 = lean_erase_macro_scopes(x_10); +x_12 = l_Lean_Name_isAtomic(x_11); +if (x_12 == 0) +{ +lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; +x_13 = lean_alloc_ctor(4, 1, 0); +lean_ctor_set(x_13, 0, x_11); +x_14 = l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___closed__2; +x_15 = lean_alloc_ctor(10, 2, 0); +lean_ctor_set(x_15, 0, x_14); +lean_ctor_set(x_15, 1, x_13); +x_16 = l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___closed__4; +x_17 = lean_alloc_ctor(10, 2, 0); +lean_ctor_set(x_17, 0, x_15); +lean_ctor_set(x_17, 1, x_16); +x_18 = l_Lean_throwErrorAt___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___spec__1(x_9, x_17, x_2, x_3, x_4, x_5, x_6, x_7, x_8); +return x_18; +} +else +{ +lean_object* x_19; lean_object* x_20; +lean_dec(x_11); +lean_dec(x_6); +lean_dec(x_2); +x_19 = lean_box(0); +x_20 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_20, 0, x_19); +lean_ctor_set(x_20, 1, x_8); +return x_20; +} +} +} +lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) { +_start: +{ +lean_object* x_10; +x_10 = l_Lean_throwErrorAt___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___spec__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9); +lean_dec(x_8); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_1); +return x_10; +} +} +lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) { +_start: +{ +lean_object* x_9; +x_9 = l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8); +lean_dec(x_7); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_1); +return x_9; +} +} lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_elabBinderViews_loop___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, uint8_t x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13, lean_object* x_14) { _start: { @@ -5169,53 +5332,61 @@ return x_15; } else { -lean_object* x_16; +lean_object* x_16; lean_object* x_17; x_16 = lean_array_fget(x_1, x_4); +lean_inc(x_10); +lean_inc(x_6); +x_17 = l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName(x_16, x_6, x_7, x_8, x_9, x_10, x_11, x_12); +if (lean_obj_tag(x_17) == 0) +{ if (x_2 == 0) { -lean_object* x_17; lean_object* x_18; -x_17 = lean_ctor_get(x_16, 1); -lean_inc(x_17); +lean_object* x_18; lean_object* x_19; lean_object* x_20; +x_18 = lean_ctor_get(x_17, 1); +lean_inc(x_18); +lean_dec(x_17); +x_19 = lean_ctor_get(x_16, 1); +lean_inc(x_19); lean_inc(x_11); lean_inc(x_10); lean_inc(x_9); lean_inc(x_8); lean_inc(x_7); lean_inc(x_6); -lean_inc(x_17); -x_18 = l_Lean_Elab_Term_elabType(x_17, x_6, x_7, x_8, x_9, x_10, x_11, x_12); -if (lean_obj_tag(x_18) == 0) -{ -lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; uint8_t x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; -x_19 = lean_ctor_get(x_18, 0); lean_inc(x_19); -x_20 = lean_ctor_get(x_18, 1); -lean_inc(x_20); -lean_dec(x_18); -x_21 = l___private_Lean_Elab_Binders_0__Lean_Elab_Term_registerFailedToInferBinderTypeInfo(x_19, x_17, x_6, x_7, x_8, x_9, x_10, x_11, x_20); -x_22 = lean_ctor_get(x_21, 1); +x_20 = l_Lean_Elab_Term_elabType(x_19, x_6, x_7, x_8, x_9, x_10, x_11, x_18); +if (lean_obj_tag(x_20) == 0) +{ +lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; uint8_t x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; +x_21 = lean_ctor_get(x_20, 0); +lean_inc(x_21); +x_22 = lean_ctor_get(x_20, 1); lean_inc(x_22); -lean_dec(x_21); -x_23 = lean_ctor_get(x_16, 0); -lean_inc(x_23); -x_24 = l_Lean_Syntax_getId(x_23); -x_25 = lean_ctor_get_uint8(x_16, sizeof(void*)*2); +lean_dec(x_20); +x_23 = l___private_Lean_Elab_Binders_0__Lean_Elab_Term_registerFailedToInferBinderTypeInfo(x_21, x_19, x_6, x_7, x_8, x_9, x_10, x_11, x_22); +x_24 = lean_ctor_get(x_23, 1); +lean_inc(x_24); +lean_dec(x_23); +x_25 = lean_ctor_get(x_16, 0); +lean_inc(x_25); +x_26 = l_Lean_Syntax_getId(x_25); +x_27 = lean_ctor_get_uint8(x_16, sizeof(void*)*2); lean_dec(x_16); -x_26 = lean_box(x_2); -x_27 = lean_alloc_closure((void*)(l___private_Lean_Elab_Binders_0__Lean_Elab_Term_elabBinderViews_loop___rarg___lambda__1___boxed), 14, 6); -lean_closure_set(x_27, 0, x_23); -lean_closure_set(x_27, 1, x_4); -lean_closure_set(x_27, 2, x_5); -lean_closure_set(x_27, 3, x_1); -lean_closure_set(x_27, 4, x_26); -lean_closure_set(x_27, 5, x_3); -x_28 = l_Lean_Meta_withLocalDecl___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImplicitLambda___spec__1___rarg(x_24, x_25, x_19, x_27, x_6, x_7, x_8, x_9, x_10, x_11, x_22); -return x_28; +x_28 = lean_box(x_2); +x_29 = lean_alloc_closure((void*)(l___private_Lean_Elab_Binders_0__Lean_Elab_Term_elabBinderViews_loop___rarg___lambda__1___boxed), 14, 6); +lean_closure_set(x_29, 0, x_25); +lean_closure_set(x_29, 1, x_4); +lean_closure_set(x_29, 2, x_5); +lean_closure_set(x_29, 3, x_1); +lean_closure_set(x_29, 4, x_28); +lean_closure_set(x_29, 5, x_3); +x_30 = l_Lean_Meta_withLocalDecl___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImplicitLambda___spec__1___rarg(x_26, x_27, x_21, x_29, x_6, x_7, x_8, x_9, x_10, x_11, x_24); +return x_30; } else { -uint8_t x_29; -lean_dec(x_17); +uint8_t x_31; +lean_dec(x_19); lean_dec(x_16); lean_dec(x_11); lean_dec(x_10); @@ -5227,43 +5398,80 @@ lean_dec(x_5); lean_dec(x_4); lean_dec(x_3); lean_dec(x_1); -x_29 = !lean_is_exclusive(x_18); -if (x_29 == 0) +x_31 = !lean_is_exclusive(x_20); +if (x_31 == 0) { -return x_18; +return x_20; } else { -lean_object* x_30; lean_object* x_31; lean_object* x_32; -x_30 = lean_ctor_get(x_18, 0); -x_31 = lean_ctor_get(x_18, 1); -lean_inc(x_31); -lean_inc(x_30); -lean_dec(x_18); -x_32 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_32, 0, x_30); -lean_ctor_set(x_32, 1, x_31); -return x_32; +lean_object* x_32; lean_object* x_33; lean_object* x_34; +x_32 = lean_ctor_get(x_20, 0); +x_33 = lean_ctor_get(x_20, 1); +lean_inc(x_33); +lean_inc(x_32); +lean_dec(x_20); +x_34 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_34, 0, x_32); +lean_ctor_set(x_34, 1, x_33); +return x_34; } } } else { -lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; -x_33 = lean_ctor_get(x_16, 1); -lean_inc(x_33); -x_34 = lean_box(x_2); -lean_inc(x_33); -x_35 = lean_alloc_closure((void*)(l___private_Lean_Elab_Binders_0__Lean_Elab_Term_elabBinderViews_loop___rarg___lambda__2___boxed), 15, 7); -lean_closure_set(x_35, 0, x_33); -lean_closure_set(x_35, 1, x_16); -lean_closure_set(x_35, 2, x_4); -lean_closure_set(x_35, 3, x_5); -lean_closure_set(x_35, 4, x_1); -lean_closure_set(x_35, 5, x_34); -lean_closure_set(x_35, 6, x_3); -x_36 = l_Lean_Elab_Term_elabTypeWithAutoBoundImplicit___rarg(x_33, x_35, x_6, x_7, x_8, x_9, x_10, x_11, x_12); -return x_36; +lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; +x_35 = lean_ctor_get(x_17, 1); +lean_inc(x_35); +lean_dec(x_17); +x_36 = lean_ctor_get(x_16, 1); +lean_inc(x_36); +x_37 = lean_box(x_2); +lean_inc(x_36); +x_38 = lean_alloc_closure((void*)(l___private_Lean_Elab_Binders_0__Lean_Elab_Term_elabBinderViews_loop___rarg___lambda__2___boxed), 15, 7); +lean_closure_set(x_38, 0, x_36); +lean_closure_set(x_38, 1, x_16); +lean_closure_set(x_38, 2, x_4); +lean_closure_set(x_38, 3, x_5); +lean_closure_set(x_38, 4, x_1); +lean_closure_set(x_38, 5, x_37); +lean_closure_set(x_38, 6, x_3); +x_39 = l_Lean_Elab_Term_elabTypeWithAutoBoundImplicit___rarg(x_36, x_38, x_6, x_7, x_8, x_9, x_10, x_11, x_35); +return x_39; +} +} +else +{ +uint8_t x_40; +lean_dec(x_16); +lean_dec(x_11); +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_1); +x_40 = !lean_is_exclusive(x_17); +if (x_40 == 0) +{ +return x_17; +} +else +{ +lean_object* x_41; lean_object* x_42; lean_object* x_43; +x_41 = lean_ctor_get(x_17, 0); +x_42 = lean_ctor_get(x_17, 1); +lean_inc(x_42); +lean_inc(x_41); +lean_dec(x_17); +x_43 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_43, 0, x_41); +lean_ctor_set(x_43, 1, x_42); +return x_43; +} } } } @@ -18113,77 +18321,119 @@ return x_13; } else { -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; uint8_t x_21; +lean_object* x_14; lean_object* x_15; x_14 = lean_array_fget(x_1, x_2); -x_15 = lean_ctor_get(x_14, 1); -lean_inc(x_15); -x_16 = lean_ctor_get(x_3, 1); -lean_inc(x_16); -x_17 = lean_ctor_get(x_3, 2); -lean_inc(x_17); -lean_inc(x_15); -x_18 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabType), 8, 1); -lean_closure_set(x_18, 0, x_15); -lean_inc(x_17); -lean_inc(x_16); -lean_inc(x_15); -x_19 = lean_alloc_closure((void*)(l___private_Lean_Elab_Binders_0__Lean_Elab_Term_FunBinders_elabFunBinderViews___lambda__1___boxed), 15, 7); -lean_closure_set(x_19, 0, x_15); -lean_closure_set(x_19, 1, x_3); -lean_closure_set(x_19, 2, x_16); -lean_closure_set(x_19, 3, x_17); -lean_closure_set(x_19, 4, x_14); -lean_closure_set(x_19, 5, x_2); -lean_closure_set(x_19, 6, x_1); -x_20 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Term_instMonadLogTermElabM___spec__2___rarg), 9, 2); -lean_closure_set(x_20, 0, x_18); -lean_closure_set(x_20, 1, x_19); -x_21 = !lean_is_exclusive(x_8); -if (x_21 == 0) +lean_inc(x_8); +lean_inc(x_4); +x_15 = l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName(x_14, x_4, x_5, x_6, x_7, x_8, x_9, x_10); +if (lean_obj_tag(x_15) == 0) { -lean_object* x_22; lean_object* x_23; lean_object* x_24; -x_22 = lean_ctor_get(x_8, 3); -x_23 = l_Lean_replaceRef(x_15, x_22); -lean_dec(x_22); +lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; uint8_t x_23; +x_16 = lean_ctor_get(x_15, 1); +lean_inc(x_16); lean_dec(x_15); -lean_ctor_set(x_8, 3, x_23); -x_24 = l_Lean_Meta_withLCtx___at_Lean_Elab_Term_elabSyntheticHole___spec__1___rarg(x_16, x_17, x_20, x_4, x_5, x_6, x_7, x_8, x_9, x_10); -return x_24; +x_17 = lean_ctor_get(x_14, 1); +lean_inc(x_17); +x_18 = lean_ctor_get(x_3, 1); +lean_inc(x_18); +x_19 = lean_ctor_get(x_3, 2); +lean_inc(x_19); +lean_inc(x_17); +x_20 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabType), 8, 1); +lean_closure_set(x_20, 0, x_17); +lean_inc(x_19); +lean_inc(x_18); +lean_inc(x_17); +x_21 = lean_alloc_closure((void*)(l___private_Lean_Elab_Binders_0__Lean_Elab_Term_FunBinders_elabFunBinderViews___lambda__1___boxed), 15, 7); +lean_closure_set(x_21, 0, x_17); +lean_closure_set(x_21, 1, x_3); +lean_closure_set(x_21, 2, x_18); +lean_closure_set(x_21, 3, x_19); +lean_closure_set(x_21, 4, x_14); +lean_closure_set(x_21, 5, x_2); +lean_closure_set(x_21, 6, x_1); +x_22 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Term_instMonadLogTermElabM___spec__2___rarg), 9, 2); +lean_closure_set(x_22, 0, x_20); +lean_closure_set(x_22, 1, x_21); +x_23 = !lean_is_exclusive(x_8); +if (x_23 == 0) +{ +lean_object* x_24; lean_object* x_25; lean_object* x_26; +x_24 = lean_ctor_get(x_8, 3); +x_25 = l_Lean_replaceRef(x_17, x_24); +lean_dec(x_24); +lean_dec(x_17); +lean_ctor_set(x_8, 3, x_25); +x_26 = l_Lean_Meta_withLCtx___at_Lean_Elab_Term_elabSyntheticHole___spec__1___rarg(x_18, x_19, x_22, x_4, x_5, x_6, x_7, x_8, x_9, x_16); +return x_26; } else { -lean_object* x_25; lean_object* x_26; 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; -x_25 = lean_ctor_get(x_8, 0); -x_26 = lean_ctor_get(x_8, 1); -x_27 = lean_ctor_get(x_8, 2); -x_28 = lean_ctor_get(x_8, 3); -x_29 = lean_ctor_get(x_8, 4); -x_30 = lean_ctor_get(x_8, 5); -x_31 = lean_ctor_get(x_8, 6); -x_32 = lean_ctor_get(x_8, 7); +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; +x_27 = lean_ctor_get(x_8, 0); +x_28 = lean_ctor_get(x_8, 1); +x_29 = lean_ctor_get(x_8, 2); +x_30 = lean_ctor_get(x_8, 3); +x_31 = lean_ctor_get(x_8, 4); +x_32 = lean_ctor_get(x_8, 5); +x_33 = lean_ctor_get(x_8, 6); +x_34 = lean_ctor_get(x_8, 7); +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_inc(x_26); -lean_inc(x_25); lean_dec(x_8); -x_33 = l_Lean_replaceRef(x_15, x_28); -lean_dec(x_28); +x_35 = l_Lean_replaceRef(x_17, x_30); +lean_dec(x_30); +lean_dec(x_17); +x_36 = lean_alloc_ctor(0, 8, 0); +lean_ctor_set(x_36, 0, x_27); +lean_ctor_set(x_36, 1, x_28); +lean_ctor_set(x_36, 2, x_29); +lean_ctor_set(x_36, 3, x_35); +lean_ctor_set(x_36, 4, x_31); +lean_ctor_set(x_36, 5, x_32); +lean_ctor_set(x_36, 6, x_33); +lean_ctor_set(x_36, 7, x_34); +x_37 = l_Lean_Meta_withLCtx___at_Lean_Elab_Term_elabSyntheticHole___spec__1___rarg(x_18, x_19, x_22, x_4, x_5, x_6, x_7, x_36, x_9, x_16); +return x_37; +} +} +else +{ +uint8_t x_38; +lean_dec(x_14); +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +lean_dec(x_1); +x_38 = !lean_is_exclusive(x_15); +if (x_38 == 0) +{ +return x_15; +} +else +{ +lean_object* x_39; lean_object* x_40; lean_object* x_41; +x_39 = lean_ctor_get(x_15, 0); +x_40 = lean_ctor_get(x_15, 1); +lean_inc(x_40); +lean_inc(x_39); lean_dec(x_15); -x_34 = lean_alloc_ctor(0, 8, 0); -lean_ctor_set(x_34, 0, x_25); -lean_ctor_set(x_34, 1, x_26); -lean_ctor_set(x_34, 2, x_27); -lean_ctor_set(x_34, 3, x_33); -lean_ctor_set(x_34, 4, x_29); -lean_ctor_set(x_34, 5, x_30); -lean_ctor_set(x_34, 6, x_31); -lean_ctor_set(x_34, 7, x_32); -x_35 = l_Lean_Meta_withLCtx___at_Lean_Elab_Term_elabSyntheticHole___spec__1___rarg(x_16, x_17, x_20, x_4, x_5, x_6, x_7, x_34, x_9, x_10); -return x_35; +x_41 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_41, 0, x_39); +lean_ctor_set(x_41, 1, x_40); +return x_41; +} } } } @@ -18760,7 +19010,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_Elab_Term_quoteAutoTactic___closed__1; x_2 = l_Lean_Elab_Term_expandWhereDecls___closed__3; -x_3 = lean_unsigned_to_nat(375u); +x_3 = lean_unsigned_to_nat(384u); x_4 = lean_unsigned_to_nat(9u); x_5 = l_Lean_Name_getString_x21___closed__3; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -22374,7 +22624,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_Elab_Term_quoteAutoTactic___closed__1; x_2 = l_Lean_Elab_Term_elabLetDeclCore___closed__1; -x_3 = lean_unsigned_to_nat(570u); +x_3 = lean_unsigned_to_nat(579u); x_4 = lean_unsigned_to_nat(24u); x_5 = l_Lean_Name_getString_x21___closed__3; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -22879,7 +23129,7 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); return x_5; } } -lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Binders___hyg_5310_(lean_object* x_1) { +lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Binders___hyg_5373_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; @@ -23023,6 +23273,14 @@ l___private_Lean_Elab_Binders_0__Lean_Elab_Term_registerFailedToInferBinderTypeI lean_mark_persistent(l___private_Lean_Elab_Binders_0__Lean_Elab_Term_registerFailedToInferBinderTypeInfo___closed__2); l___private_Lean_Elab_Binders_0__Lean_Elab_Term_registerFailedToInferBinderTypeInfo___closed__3 = _init_l___private_Lean_Elab_Binders_0__Lean_Elab_Term_registerFailedToInferBinderTypeInfo___closed__3(); lean_mark_persistent(l___private_Lean_Elab_Binders_0__Lean_Elab_Term_registerFailedToInferBinderTypeInfo___closed__3); +l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___closed__1 = _init_l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___closed__1(); +lean_mark_persistent(l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___closed__1); +l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___closed__2 = _init_l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___closed__2(); +lean_mark_persistent(l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___closed__2); +l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___closed__3 = _init_l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___closed__3(); +lean_mark_persistent(l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___closed__3); +l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___closed__4 = _init_l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___closed__4(); +lean_mark_persistent(l___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___closed__4); l___regBuiltin_Lean_Elab_Term_elabForall___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_elabForall___closed__1(); lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabForall___closed__1); res = l___regBuiltin_Lean_Elab_Term_elabForall(lean_io_mk_world()); @@ -23100,7 +23358,7 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabLetStarDecl___closed__1); res = l___regBuiltin_Lean_Elab_Term_elabLetStarDecl(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); -res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Binders___hyg_5310_(lean_io_mk_world()); +res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Binders___hyg_5373_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); return lean_io_result_mk_ok(lean_box(0)); diff --git a/stage0/stdlib/Lean/Elab/Declaration.c b/stage0/stdlib/Lean/Elab/Declaration.c index 70ea79e7eb..42a0560e2f 100644 --- a/stage0/stdlib/Lean/Elab/Declaration.c +++ b/stage0/stdlib/Lean/Elab/Declaration.c @@ -35,7 +35,6 @@ lean_object* l_Lean_Elab_Command_elabAxiom___lambda__2___boxed(lean_object*, lea lean_object* l_Lean_Meta_mkForallFVars(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__5(lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_nullKind; -lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Command_elabAxiom___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Command_expandInitCmd___closed__7; lean_object* l_Lean_Elab_Command_elabMutualDef(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__8(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*); @@ -129,7 +128,6 @@ lean_object* l_Lean_Name_toStringWithSep(lean_object*, lean_object*); extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1128____closed__11; extern lean_object* l_Lean_Parser_Command_check___elambda__1___closed__2; lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_myMacro____x40_Init_Notation___hyg_14642__expandListLit___spec__1(lean_object*, lean_object*); -lean_object* l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Declaration_0__Lean_Elab_Command_classInductiveSyntaxToView(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_myMacro____x40_Init_Notation___hyg_13855____closed__9; lean_object* l_Lean_setEnv___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__4(lean_object*, lean_object*, lean_object*, lean_object*); @@ -237,7 +235,6 @@ lean_object* l_Lean_Elab_Command_expandMutualPreamble(lean_object*, lean_object* lean_object* l_Lean_PersistentEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabBinders___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1128____closed__1; -lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Command_elabAxiom___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_myMacro____x40_Init_NotationExtra___hyg_3363____closed__18; extern lean_object* l_Lean_nullKind___closed__2; extern lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_535____closed__2; @@ -281,6 +278,7 @@ extern lean_object* l_Lean_Elab_Command_elabStructure___closed__1; lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__3___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Command_elabAttr_match__1___boxed(lean_object*, lean_object*); lean_object* l_Lean_Elab_Command_expandMutualNamespace_match__2(lean_object*); +lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_expandMutualElement___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1128____closed__25; lean_object* l_Lean_Elab_Command_getMainModule___rarg(lean_object*, lean_object*); @@ -1973,59 +1971,6 @@ return x_19; } } } -lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Command_elabAxiom___spec__4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) { -_start: -{ -uint8_t x_10; -x_10 = !lean_is_exclusive(x_7); -if (x_10 == 0) -{ -lean_object* x_11; lean_object* x_12; lean_object* x_13; -x_11 = lean_ctor_get(x_7, 3); -x_12 = l_Lean_replaceRef(x_1, x_11); -lean_dec(x_11); -lean_ctor_set(x_7, 3, x_12); -x_13 = l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1(x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9); -lean_dec(x_7); -return x_13; -} -else -{ -lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; -x_14 = lean_ctor_get(x_7, 0); -x_15 = lean_ctor_get(x_7, 1); -x_16 = lean_ctor_get(x_7, 2); -x_17 = lean_ctor_get(x_7, 3); -x_18 = lean_ctor_get(x_7, 4); -x_19 = lean_ctor_get(x_7, 5); -x_20 = lean_ctor_get(x_7, 6); -x_21 = lean_ctor_get(x_7, 7); -lean_inc(x_21); -lean_inc(x_20); -lean_inc(x_19); -lean_inc(x_18); -lean_inc(x_17); -lean_inc(x_16); -lean_inc(x_15); -lean_inc(x_14); -lean_dec(x_7); -x_22 = l_Lean_replaceRef(x_1, x_17); -lean_dec(x_17); -x_23 = lean_alloc_ctor(0, 8, 0); -lean_ctor_set(x_23, 0, x_14); -lean_ctor_set(x_23, 1, x_15); -lean_ctor_set(x_23, 2, x_16); -lean_ctor_set(x_23, 3, x_22); -lean_ctor_set(x_23, 4, x_18); -lean_ctor_set(x_23, 5, x_19); -lean_ctor_set(x_23, 6, x_20); -lean_ctor_set(x_23, 7, x_21); -x_24 = l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1(x_2, x_3, x_4, x_5, x_6, x_23, x_8, x_9); -lean_dec(x_23); -return x_24; -} -} -} lean_object* l_Lean_Elab_Command_elabAxiom___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) { _start: { @@ -2147,7 +2092,7 @@ x_47 = lean_alloc_ctor(2, 1, 0); lean_ctor_set(x_47, 0, x_46); x_48 = lean_alloc_ctor(0, 1, 0); lean_ctor_set(x_48, 0, x_47); -x_49 = l_Lean_throwErrorAt___at_Lean_Elab_Command_elabAxiom___spec__4(x_7, x_48, x_9, x_10, x_11, x_12, x_13, x_14, x_40); +x_49 = l_Lean_throwErrorAt___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_ensureAtomicBinderName___spec__1(x_7, x_48, x_9, x_10, x_11, x_12, x_13, x_14, x_40); lean_dec(x_14); lean_dec(x_12); lean_dec(x_11); @@ -2931,19 +2876,6 @@ lean_dec(x_3); return x_6; } } -lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Command_elabAxiom___spec__4___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) { -_start: -{ -lean_object* x_10; -x_10 = l_Lean_throwErrorAt___at_Lean_Elab_Command_elabAxiom___spec__4(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9); -lean_dec(x_8); -lean_dec(x_6); -lean_dec(x_5); -lean_dec(x_4); -lean_dec(x_1); -return x_10; -} -} lean_object* l_Lean_Elab_Command_elabAxiom___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) { _start: { diff --git a/stage0/stdlib/Lean/Elab/Do.c b/stage0/stdlib/Lean/Elab/Do.c index 8ab7adc4bd..87cf9be79b 100644 --- a/stage0/stdlib/Lean/Elab/Do.c +++ b/stage0/stdlib/Lean/Elab/Do.c @@ -80,6 +80,7 @@ lean_object* l_Lean_Elab_Term_Do_CodeBlocl_toMessageData(lean_object*); lean_object* l_Lean_throwError___at_Lean_Elab_Term_Do_concat___spec__2___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_Term_Do_ToCodeBlock_doUnlessToCode___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_Do_pullExitPointsAux___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*); +extern lean_object* l_instReprSigma___rarg___closed__2; lean_object* l_Std_RBNode_insert___at_Lean_NameSet_insert___spec__1(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_Do_getLetIdDeclVar(lean_object*); lean_object* l_Lean_throwError___at_Lean_Elab_Term_Do_getLetDeclVars___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -183,6 +184,7 @@ extern lean_object* l_Array_forInUnsafe_loop___at_myMacro____x40_Init_NotationEx lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_getDoSeq___boxed(lean_object*); extern lean_object* l_Lean_Meta_mkPure___closed__4; extern lean_object* l_myMacro____x40_Init_Notation___hyg_12336____closed__4; +extern lean_object* l_Lean_Parser_Term_anonymousCtor___elambda__1___closed__2; lean_object* l_Lean_Elab_Term_Do_concat___closed__2; size_t l_USize_sub(size_t, size_t); extern lean_object* l_Lean_Parser_Term_doIfLetBind___elambda__1___closed__1; @@ -281,6 +283,7 @@ lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_expandDoIf_x3f_match_ lean_object* l_Lean_Elab_Term_Do_ToTerm_declToTerm_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Array_anyMUnsafe_any___at_Lean_Elab_Term_Do_hasReturn___spec__2___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_synthesizeInst(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__8; extern lean_object* l_Lean_Parser_Term_proj___elambda__1___closed__1; lean_object* l_Array_anyMUnsafe_any___at_Lean_Elab_Term_Do_hasTerminalAction___spec__2___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_Do_ToTerm_mkNestedKind_match__1___rarg(uint8_t, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -293,7 +296,6 @@ lean_object* l_Lean_Elab_Term_Do_ToTerm_returnToTerm___closed__36; lean_object* l_Lean_MessageData_joinSep(lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_Quotation_getPatternsVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Term_tupleTail___elambda__1___closed__2; -lean_object* l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__4; lean_object* l_Std_RBNode_fold___at___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_union___spec__1(lean_object*, lean_object*); lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_Do_CodeBlocl_toMessageData_loop___spec__2___closed__1; extern lean_object* l_myMacro____x40_Init_Notation___hyg_12336____closed__8; @@ -471,7 +473,6 @@ lean_object* l_Lean_Elab_Term_Do_ToTerm_breakToTerm___closed__2; lean_object* l_Lean_Elab_Term_Do_ToTerm_breakToTerm___closed__21; lean_object* l_Lean_throwError___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_Do_ToTerm_Kind_isRegular_match__1(lean_object*); -lean_object* l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__20; lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doReassignArrowToCode___closed__8; lean_object* l_Lean_Elab_Term_Do_ToTerm_Kind_isRegular_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_Do_ToCodeBlock_doSeqToCode___spec__9___rarg(lean_object*); @@ -489,6 +490,7 @@ lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_Do_concat___ lean_object* l_Lean_Elab_Term_Do_hasExitPointPred_loop___at_Lean_Elab_Term_Do_hasExitPoint___spec__1___boxed(lean_object*); lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doReassignArrowToCode___closed__4; lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_Do_ToCodeBlock_getTryCatchUpdatedVars___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__7; lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_Do_getPatternVarNames___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_Do_mkAuxDeclFor___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_Do_hasReturn_match__1___rarg(lean_object*, lean_object*, lean_object*); @@ -684,7 +686,6 @@ lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doForToCode___closed__16; extern lean_object* l_Lean_KernelException_toMessageData___closed__15; uint8_t l_Array_isEmpty___rarg(lean_object*); extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_832____closed__10; -lean_object* l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__5; lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_Do_mkAuxDeclFor___rarg___lambda__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_Do_getDoHaveVar___boxed(lean_object*); @@ -801,6 +802,7 @@ lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_Do_ToTerm_mkJoinPoint___ lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_hasLiftMethod_match__1(lean_object*); lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_Do_CodeBlocl_toMessageData_loop___spec__2(lean_object*, lean_object*, size_t, size_t, lean_object*); lean_object* l_Lean_Elab_Term_Do_hasTerminalAction___boxed(lean_object*); +lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__6; uint8_t l_Lean_Elab_Term_Do_hasExitPointPred_loop___at_Lean_Elab_Term_Do_hasExitPoint___spec__1(lean_object*); lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_Do_getPatternVarsEx___spec__1(size_t, size_t, lean_object*); lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_mkIdBindFor___closed__1; @@ -815,7 +817,7 @@ lean_object* l_Lean_Elab_Term_Do_ToTerm_breakToTerm___closed__15; extern lean_object* l_myMacro____x40_Init_Notation___hyg_10982____closed__5; lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doForToCode___closed__24; lean_object* l_Lean_Elab_Term_Do_hasExitPointPred_loop___at_Lean_Elab_Term_Do_hasTerminalAction___spec__1___boxed(lean_object*); -lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_27039_(lean_object*); +lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_27109_(lean_object*); lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_ensureEOS___closed__3; lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doReassignArrowToCode___closed__3; lean_object* l_Lean_Elab_Term_getPatternVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -982,7 +984,6 @@ lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_expandDoIf_x3f_match_ lean_object* l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__9; lean_object* l___regBuiltin_Lean_Elab_Term_expandTermReturn___closed__1; lean_object* l_Lean_Elab_Term_Do_mkFreshJP___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__19; lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doForToCode___closed__5; lean_object* l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult_match__1___rarg(uint8_t, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Term_doHave___elambda__1___closed__2; @@ -1184,6 +1185,7 @@ lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_expandDoIf_x3f___lamb lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doForToCode___closed__18; lean_object* l_Lean_Elab_Term_Do_mkTerminalAction(lean_object*); lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__11___closed__8; +extern lean_object* l_instReprSigma___rarg___closed__6; lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__3___closed__2; lean_object* l_Lean_Elab_Term_Do_ToTerm_continueToTerm___closed__27; extern lean_object* l_myMacro____x40_Init_NotationExtra___hyg_2903____closed__4; @@ -1242,7 +1244,6 @@ lean_object* l_Lean_Elab_Term_Do_ToTerm_continueToTerm___closed__3; lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doForToCode___closed__22; lean_object* l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_Do_hasExitPoint___boxed(lean_object*); -lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__7; lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__11___boxed(lean_object**); extern lean_object* l_Lean_Meta_Match_Alt_toMessageData___closed__3; lean_object* l_Lean_Elab_getBetterRef(lean_object*, lean_object*); @@ -14721,19 +14722,27 @@ return x_80; static lean_object* _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__1() { _start: { -lean_object* x_1; lean_object* x_2; -x_1 = l_instReprPUnit___closed__1; -x_2 = lean_string_utf8_byte_size(x_1); -return x_2; +lean_object* x_1; +x_1 = lean_mk_string("PUnit"); +return x_1; } } static lean_object* _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__2() { _start: { +lean_object* x_1; lean_object* x_2; +x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__1; +x_2 = lean_string_utf8_byte_size(x_1); +return x_2; +} +} +static lean_object* _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__3() { +_start: +{ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_instReprPUnit___closed__1; +x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__1; x_2 = lean_unsigned_to_nat(0u); -x_3 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__1; +x_3 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__2; x_4 = lean_alloc_ctor(0, 3, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_2); @@ -14741,20 +14750,12 @@ lean_ctor_set(x_4, 2, x_3); return x_4; } } -static lean_object* _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__3() { -_start: -{ -lean_object* x_1; -x_1 = lean_mk_string("PUnit"); -return x_1; -} -} static lean_object* _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__4() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__3; +x_2 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } @@ -14763,9 +14764,11 @@ static lean_object* _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit__ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__4; -x_2 = l_Lean_instToExprUnit___lambda__1___closed__1; -x_3 = lean_name_mk_string(x_1, x_2); +x_1 = lean_box(0); +x_2 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__4; +x_3 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_3, 0, x_2); +lean_ctor_set(x_3, 1, x_1); return x_3; } } @@ -14775,18 +14778,6 @@ _start: lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); x_2 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__5; -x_3 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_3, 0, x_2); -lean_ctor_set(x_3, 1, x_1); -return x_3; -} -} -static lean_object* _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__7() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__6; x_3 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_3, 0, x_2); lean_ctor_set(x_3, 1, x_1); @@ -14801,51 +14792,165 @@ x_3 = l_Lean_MonadRef_mkInfoFromRefPos___at_myMacro____x40_Init_Notation___hyg_1 x_4 = !lean_is_exclusive(x_3); if (x_4 == 0) { -lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; +lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; 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; lean_object* x_44; x_5 = lean_ctor_get(x_3, 0); x_6 = lean_ctor_get(x_1, 2); lean_inc(x_6); x_7 = lean_ctor_get(x_1, 1); lean_inc(x_7); lean_dec(x_1); -x_8 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__5; -x_9 = l_Lean_addMacroScope(x_7, x_8, x_6); -x_10 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__2; -x_11 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__7; -x_12 = lean_alloc_ctor(3, 4, 0); -lean_ctor_set(x_12, 0, x_5); -lean_ctor_set(x_12, 1, x_10); -lean_ctor_set(x_12, 2, x_9); -lean_ctor_set(x_12, 3, x_11); -lean_ctor_set(x_3, 0, x_12); +x_8 = l_prec_x28___x29___closed__3; +lean_inc(x_5); +x_9 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_9, 0, x_5); +lean_ctor_set(x_9, 1, x_8); +x_10 = l_Array_empty___closed__1; +x_11 = lean_array_push(x_10, x_9); +x_12 = l_instReprSigma___rarg___closed__2; +lean_inc(x_5); +x_13 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_13, 0, x_5); +lean_ctor_set(x_13, 1, x_12); +x_14 = lean_array_push(x_10, x_13); +x_15 = l_myMacro____x40_Init_Notation___hyg_1398____closed__8; +x_16 = lean_array_push(x_14, x_15); +x_17 = l_instReprSigma___rarg___closed__6; +lean_inc(x_5); +x_18 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_18, 0, x_5); +lean_ctor_set(x_18, 1, x_17); +x_19 = lean_array_push(x_16, x_18); +x_20 = l_Lean_Parser_Term_anonymousCtor___elambda__1___closed__2; +x_21 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_21, 0, x_20); +lean_ctor_set(x_21, 1, x_19); +x_22 = lean_array_push(x_10, x_21); +x_23 = l_myMacro____x40_Init_Notation___hyg_13855____closed__9; +lean_inc(x_5); +x_24 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_24, 0, x_5); +lean_ctor_set(x_24, 1, x_23); +x_25 = lean_array_push(x_10, x_24); +x_26 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__4; +x_27 = l_Lean_addMacroScope(x_7, x_26, x_6); +x_28 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__3; +x_29 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__6; +lean_inc(x_5); +x_30 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_30, 0, x_5); +lean_ctor_set(x_30, 1, x_28); +lean_ctor_set(x_30, 2, x_27); +lean_ctor_set(x_30, 3, x_29); +x_31 = lean_array_push(x_25, x_30); +x_32 = l_myMacro____x40_Init_Notation___hyg_13855____closed__8; +x_33 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_33, 0, x_32); +lean_ctor_set(x_33, 1, x_31); +x_34 = lean_array_push(x_10, x_33); +x_35 = l_Lean_nullKind___closed__2; +x_36 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_36, 0, x_35); +lean_ctor_set(x_36, 1, x_34); +x_37 = lean_array_push(x_22, x_36); +x_38 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_38, 0, x_35); +lean_ctor_set(x_38, 1, x_37); +x_39 = lean_array_push(x_11, x_38); +x_40 = l_prec_x28___x29___closed__7; +x_41 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_41, 0, x_5); +lean_ctor_set(x_41, 1, x_40); +x_42 = lean_array_push(x_39, x_41); +x_43 = l_myMacro____x40_Init_Notation___hyg_12336____closed__8; +x_44 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_44, 0, x_43); +lean_ctor_set(x_44, 1, x_42); +lean_ctor_set(x_3, 0, x_44); return x_3; } 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; lean_object* x_21; lean_object* x_22; -x_13 = lean_ctor_get(x_3, 0); -x_14 = lean_ctor_get(x_3, 1); -lean_inc(x_14); -lean_inc(x_13); +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; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; +x_45 = lean_ctor_get(x_3, 0); +x_46 = lean_ctor_get(x_3, 1); +lean_inc(x_46); +lean_inc(x_45); lean_dec(x_3); -x_15 = lean_ctor_get(x_1, 2); -lean_inc(x_15); -x_16 = lean_ctor_get(x_1, 1); -lean_inc(x_16); +x_47 = lean_ctor_get(x_1, 2); +lean_inc(x_47); +x_48 = lean_ctor_get(x_1, 1); +lean_inc(x_48); lean_dec(x_1); -x_17 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__5; -x_18 = l_Lean_addMacroScope(x_16, x_17, x_15); -x_19 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__2; -x_20 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__7; -x_21 = lean_alloc_ctor(3, 4, 0); -lean_ctor_set(x_21, 0, x_13); -lean_ctor_set(x_21, 1, x_19); -lean_ctor_set(x_21, 2, x_18); -lean_ctor_set(x_21, 3, x_20); -x_22 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_22, 0, x_21); -lean_ctor_set(x_22, 1, x_14); -return x_22; +x_49 = l_prec_x28___x29___closed__3; +lean_inc(x_45); +x_50 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_50, 0, x_45); +lean_ctor_set(x_50, 1, x_49); +x_51 = l_Array_empty___closed__1; +x_52 = lean_array_push(x_51, x_50); +x_53 = l_instReprSigma___rarg___closed__2; +lean_inc(x_45); +x_54 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_54, 0, x_45); +lean_ctor_set(x_54, 1, x_53); +x_55 = lean_array_push(x_51, x_54); +x_56 = l_myMacro____x40_Init_Notation___hyg_1398____closed__8; +x_57 = lean_array_push(x_55, x_56); +x_58 = l_instReprSigma___rarg___closed__6; +lean_inc(x_45); +x_59 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_59, 0, x_45); +lean_ctor_set(x_59, 1, x_58); +x_60 = lean_array_push(x_57, x_59); +x_61 = l_Lean_Parser_Term_anonymousCtor___elambda__1___closed__2; +x_62 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_62, 0, x_61); +lean_ctor_set(x_62, 1, x_60); +x_63 = lean_array_push(x_51, x_62); +x_64 = l_myMacro____x40_Init_Notation___hyg_13855____closed__9; +lean_inc(x_45); +x_65 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_65, 0, x_45); +lean_ctor_set(x_65, 1, x_64); +x_66 = lean_array_push(x_51, x_65); +x_67 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__4; +x_68 = l_Lean_addMacroScope(x_48, x_67, x_47); +x_69 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__3; +x_70 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__6; +lean_inc(x_45); +x_71 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_71, 0, x_45); +lean_ctor_set(x_71, 1, x_69); +lean_ctor_set(x_71, 2, x_68); +lean_ctor_set(x_71, 3, x_70); +x_72 = lean_array_push(x_66, x_71); +x_73 = l_myMacro____x40_Init_Notation___hyg_13855____closed__8; +x_74 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_74, 0, x_73); +lean_ctor_set(x_74, 1, x_72); +x_75 = lean_array_push(x_51, x_74); +x_76 = l_Lean_nullKind___closed__2; +x_77 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_77, 0, x_76); +lean_ctor_set(x_77, 1, x_75); +x_78 = lean_array_push(x_63, x_77); +x_79 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_79, 0, x_76); +lean_ctor_set(x_79, 1, x_78); +x_80 = lean_array_push(x_52, x_79); +x_81 = l_prec_x28___x29___closed__7; +x_82 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_82, 0, x_45); +lean_ctor_set(x_82, 1, x_81); +x_83 = lean_array_push(x_80, x_82); +x_84 = l_myMacro____x40_Init_Notation___hyg_12336____closed__8; +x_85 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_85, 0, x_84); +lean_ctor_set(x_85, 1, x_83); +x_86 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_86, 0, x_85); +lean_ctor_set(x_86, 1, x_46); +return x_86; } } } @@ -14885,21 +14990,54 @@ return x_3; static lean_object* _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__4() { _start: { +lean_object* x_1; lean_object* x_2; +x_1 = l_instReprPUnit___closed__1; +x_2 = lean_string_utf8_byte_size(x_1); +return x_2; +} +} +static lean_object* _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__5() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_instReprPUnit___closed__1; +x_2 = lean_unsigned_to_nat(0u); +x_3 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__4; +x_4 = lean_alloc_ctor(0, 3, 0); +lean_ctor_set(x_4, 0, x_1); +lean_ctor_set(x_4, 1, x_2); +lean_ctor_set(x_4, 2, x_3); +return x_4; +} +} +static lean_object* _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__6() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__4; +x_2 = l_Lean_instToExprUnit___lambda__1___closed__1; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +static lean_object* _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__7() { +_start: +{ lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__5; +x_2 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__6; x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_2); lean_ctor_set(x_3, 1, x_1); return x_3; } } -static lean_object* _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__5() { +static lean_object* _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__8() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__4; +x_2 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__7; x_3 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_3, 0, x_2); lean_ctor_set(x_3, 1, x_1); @@ -14935,10 +15073,10 @@ lean_ctor_set(x_12, 2, x_9); lean_ctor_set(x_12, 3, x_11); x_13 = l_Array_empty___closed__1; x_14 = lean_array_push(x_13, x_12); -x_15 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__5; +x_15 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__6; x_16 = l_Lean_addMacroScope(x_7, x_15, x_6); -x_17 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__2; -x_18 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__5; +x_17 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__5; +x_18 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__8; x_19 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_19, 0, x_5); lean_ctor_set(x_19, 1, x_17); @@ -14984,10 +15122,10 @@ lean_ctor_set(x_34, 2, x_31); lean_ctor_set(x_34, 3, x_33); x_35 = l_Array_empty___closed__1; x_36 = lean_array_push(x_35, x_34); -x_37 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__5; +x_37 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__6; x_38 = l_Lean_addMacroScope(x_29, x_37, x_28); -x_39 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__2; -x_40 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__5; +x_39 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__5; +x_40 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__8; x_41 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_41, 0, x_26); lean_ctor_set(x_41, 1, x_39); @@ -20038,10 +20176,10 @@ lean_ctor_set(x_35, 2, x_32); lean_ctor_set(x_35, 3, x_34); x_36 = l_Array_empty___closed__1; x_37 = lean_array_push(x_36, x_35); -x_38 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__5; +x_38 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__6; x_39 = l_Lean_addMacroScope(x_16, x_38, x_17); -x_40 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__2; -x_41 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__5; +x_40 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__5; +x_41 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__8; x_42 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_42, 0, x_21); lean_ctor_set(x_42, 1, x_40); @@ -20279,10 +20417,10 @@ lean_ctor_set(x_128, 2, x_125); lean_ctor_set(x_128, 3, x_127); x_129 = l_Array_empty___closed__1; x_130 = lean_array_push(x_129, x_128); -x_131 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__5; +x_131 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__6; x_132 = l_Lean_addMacroScope(x_106, x_131, x_107); -x_133 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__2; -x_134 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__5; +x_133 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__5; +x_134 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__8; x_135 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_135, 0, x_114); lean_ctor_set(x_135, 1, x_133); @@ -20469,10 +20607,10 @@ lean_ctor_set(x_33, 2, x_30); lean_ctor_set(x_33, 3, x_32); x_34 = l_Array_empty___closed__1; x_35 = lean_array_push(x_34, x_33); -x_36 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__5; +x_36 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__6; x_37 = l_Lean_addMacroScope(x_14, x_36, x_15); -x_38 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__2; -x_39 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__5; +x_38 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__5; +x_39 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__8; x_40 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_40, 0, x_19); lean_ctor_set(x_40, 1, x_38); @@ -20711,10 +20849,10 @@ lean_ctor_set(x_127, 2, x_124); lean_ctor_set(x_127, 3, x_126); x_128 = l_Array_empty___closed__1; x_129 = lean_array_push(x_128, x_127); -x_130 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__5; +x_130 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__6; x_131 = l_Lean_addMacroScope(x_105, x_130, x_106); -x_132 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__2; -x_133 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__5; +x_132 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__5; +x_133 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__8; x_134 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_134, 0, x_113); lean_ctor_set(x_134, 1, x_132); @@ -27362,29 +27500,6 @@ return x_3; static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__3() { _start: { -lean_object* x_1; lean_object* x_2; -x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__3; -x_2 = lean_string_utf8_byte_size(x_1); -return x_2; -} -} -static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__4() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__3; -x_2 = lean_unsigned_to_nat(0u); -x_3 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__3; -x_4 = lean_alloc_ctor(0, 3, 0); -lean_ctor_set(x_4, 0, x_1); -lean_ctor_set(x_4, 1, x_2); -lean_ctor_set(x_4, 2, x_3); -return x_4; -} -} -static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__5() { -_start: -{ lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); x_2 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__4; @@ -27394,19 +27509,19 @@ lean_ctor_set(x_3, 1, x_1); return x_3; } } -static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__6() { +static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__4() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__5; +x_2 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__3; x_3 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_3, 0, x_2); lean_ctor_set(x_3, 1, x_1); return x_3; } } -static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__7() { +static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__5() { _start: { lean_object* x_1; @@ -27414,12 +27529,12 @@ x_1 = lean_mk_string("Lean.Elab.Term.Do.ToTerm.actionTerminalToTerm"); return x_1; } } -static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__8() { +static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__6() { _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_Elab_Term_Do_ToTerm_returnToTerm___closed__17; -x_2 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__7; +x_2 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__5; x_3 = lean_unsigned_to_nat(838u); x_4 = lean_unsigned_to_nat(28u); x_5 = l_Lean_Name_getString_x21___closed__3; @@ -27427,7 +27542,7 @@ x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); return x_6; } } -static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__9() { +static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__7() { _start: { lean_object* x_1; @@ -27435,22 +27550,22 @@ x_1 = lean_mk_string("DoResultPR.«pure»"); return x_1; } } -static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__10() { +static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__8() { _start: { lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__9; +x_1 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__7; x_2 = lean_string_utf8_byte_size(x_1); return x_2; } } -static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__11() { +static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__9() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__9; +x_1 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__7; x_2 = lean_unsigned_to_nat(0u); -x_3 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__10; +x_3 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__8; x_4 = lean_alloc_ctor(0, 3, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_2); @@ -27458,7 +27573,7 @@ lean_ctor_set(x_4, 2, x_3); return x_4; } } -static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__12() { +static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__10() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; @@ -27468,31 +27583,31 @@ x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__13() { +static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__11() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__12; +x_2 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__10; x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_2); lean_ctor_set(x_3, 1, x_1); return x_3; } } -static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__14() { +static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__12() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__13; +x_2 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__11; x_3 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_3, 0, x_2); lean_ctor_set(x_3, 1, x_1); return x_3; } } -static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__15() { +static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__13() { _start: { lean_object* x_1; @@ -27500,22 +27615,22 @@ x_1 = lean_mk_string("DoResultPRBC.«pure»"); return x_1; } } -static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__16() { +static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__14() { _start: { lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__15; +x_1 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__13; x_2 = lean_string_utf8_byte_size(x_1); return x_2; } } -static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__17() { +static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__15() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__15; +x_1 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__13; x_2 = lean_unsigned_to_nat(0u); -x_3 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__16; +x_3 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__14; x_4 = lean_alloc_ctor(0, 3, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_2); @@ -27523,7 +27638,7 @@ lean_ctor_set(x_4, 2, x_3); return x_4; } } -static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__18() { +static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__16() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; @@ -27533,24 +27648,24 @@ x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__19() { +static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__17() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__18; +x_2 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__16; x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_2); lean_ctor_set(x_3, 1, x_1); return x_3; } } -static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__20() { +static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__18() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__19; +x_2 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__17; x_3 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_3, 0, x_2); lean_ctor_set(x_3, 1, x_1); @@ -28135,8 +28250,8 @@ x_264 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__4; lean_inc(x_4); lean_inc(x_6); x_265 = l_Lean_addMacroScope(x_6, x_264, x_4); -x_266 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__4; -x_267 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__6; +x_266 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__3; +x_267 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__4; lean_inc(x_240); x_268 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_268, 0, x_240); @@ -28309,8 +28424,8 @@ x_352 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__4; lean_inc(x_4); lean_inc(x_6); x_353 = l_Lean_addMacroScope(x_6, x_352, x_4); -x_354 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__4; -x_355 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__6; +x_354 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__3; +x_355 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__4; lean_inc(x_327); x_356 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_356, 0, x_327); @@ -28494,8 +28609,8 @@ x_444 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__4; lean_inc(x_4); lean_inc(x_6); x_445 = l_Lean_addMacroScope(x_6, x_444, x_4); -x_446 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__4; -x_447 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__6; +x_446 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__3; +x_447 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__4; lean_inc(x_420); x_448 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_448, 0, x_420); @@ -28714,8 +28829,8 @@ x_554 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__4; lean_inc(x_4); lean_inc(x_6); x_555 = l_Lean_addMacroScope(x_6, x_554, x_4); -x_556 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__4; -x_557 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__6; +x_556 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__3; +x_557 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__4; lean_inc(x_529); x_558 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_558, 0, x_529); @@ -28891,7 +29006,7 @@ x_640 = lean_ctor_get(x_12, 1); lean_inc(x_640); lean_dec(x_12); x_641 = l_Lean_Elab_Term_Do_ToTerm_returnToTerm___closed__16; -x_642 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__8; +x_642 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__6; x_643 = lean_panic_fn(x_641, x_642); x_644 = lean_apply_3(x_643, x_2, x_3, x_640); return x_644; @@ -28977,10 +29092,10 @@ lean_ctor_set(x_680, 1, x_678); lean_ctor_set(x_680, 2, x_677); lean_ctor_set(x_680, 3, x_679); x_681 = lean_array_push(x_656, x_680); -x_682 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__12; +x_682 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__10; x_683 = l_Lean_addMacroScope(x_6, x_682, x_4); -x_684 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__11; -x_685 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__14; +x_684 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__9; +x_685 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__12; lean_inc(x_649); x_686 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_686, 0, x_649); @@ -29127,10 +29242,10 @@ lean_ctor_set(x_755, 1, x_753); lean_ctor_set(x_755, 2, x_752); lean_ctor_set(x_755, 3, x_754); x_756 = lean_array_push(x_731, x_755); -x_757 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__12; +x_757 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__10; x_758 = l_Lean_addMacroScope(x_6, x_757, x_4); -x_759 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__11; -x_760 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__14; +x_759 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__9; +x_760 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__12; lean_inc(x_723); x_761 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_761, 0, x_723); @@ -29599,10 +29714,10 @@ lean_ctor_set(x_988, 1, x_986); lean_ctor_set(x_988, 2, x_985); lean_ctor_set(x_988, 3, x_987); x_989 = lean_array_push(x_964, x_988); -x_990 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__18; +x_990 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__16; x_991 = l_Lean_addMacroScope(x_6, x_990, x_4); -x_992 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__17; -x_993 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__20; +x_992 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__15; +x_993 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__18; lean_inc(x_957); x_994 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_994, 0, x_957); @@ -29749,10 +29864,10 @@ lean_ctor_set(x_1063, 1, x_1061); lean_ctor_set(x_1063, 2, x_1060); lean_ctor_set(x_1063, 3, x_1062); x_1064 = lean_array_push(x_1039, x_1063); -x_1065 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__18; +x_1065 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__16; x_1066 = l_Lean_addMacroScope(x_6, x_1065, x_4); -x_1067 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__17; -x_1068 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__20; +x_1067 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__15; +x_1068 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__18; lean_inc(x_1031); x_1069 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_1069, 0, x_1031); @@ -30156,8 +30271,8 @@ x_1229 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__4; lean_inc(x_4); lean_inc(x_1112); x_1230 = l_Lean_addMacroScope(x_1112, x_1229, x_4); -x_1231 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__4; -x_1232 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__6; +x_1231 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__3; +x_1232 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__4; lean_inc(x_1203); x_1233 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_1233, 0, x_1203); @@ -30351,8 +30466,8 @@ x_1322 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__4; lean_inc(x_4); lean_inc(x_1112); x_1323 = l_Lean_addMacroScope(x_1112, x_1322, x_4); -x_1324 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__4; -x_1325 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__6; +x_1324 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__3; +x_1325 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__4; lean_inc(x_1296); x_1326 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_1326, 0, x_1296); @@ -30531,7 +30646,7 @@ x_1408 = lean_ctor_get(x_1120, 1); lean_inc(x_1408); lean_dec(x_1120); x_1409 = l_Lean_Elab_Term_Do_ToTerm_returnToTerm___closed__16; -x_1410 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__8; +x_1410 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__6; x_1411 = lean_panic_fn(x_1409, x_1410); x_1412 = lean_apply_3(x_1411, x_2, x_1119, x_1408); return x_1412; @@ -30624,10 +30739,10 @@ lean_ctor_set(x_1449, 1, x_1447); lean_ctor_set(x_1449, 2, x_1446); lean_ctor_set(x_1449, 3, x_1448); x_1450 = lean_array_push(x_1425, x_1449); -x_1451 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__12; +x_1451 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__10; x_1452 = l_Lean_addMacroScope(x_1112, x_1451, x_4); -x_1453 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__11; -x_1454 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__14; +x_1453 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__9; +x_1454 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__12; lean_inc(x_1416); x_1455 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_1455, 0, x_1416); @@ -30966,10 +31081,10 @@ lean_ctor_set(x_1609, 1, x_1607); lean_ctor_set(x_1609, 2, x_1606); lean_ctor_set(x_1609, 3, x_1608); x_1610 = lean_array_push(x_1585, x_1609); -x_1611 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__18; +x_1611 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__16; x_1612 = l_Lean_addMacroScope(x_1112, x_1611, x_4); -x_1613 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__17; -x_1614 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__20; +x_1613 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__15; +x_1614 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__18; lean_inc(x_1576); x_1615 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_1615, 0, x_1576); @@ -31108,7 +31223,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__4; +x_2 = l_myMacro____x40_Init_Notation___hyg_10982____closed__7; x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_2); lean_ctor_set(x_3, 1, x_1); @@ -31131,30 +31246,6 @@ static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_myMacro____x40_Init_Notation___hyg_10982____closed__7; -x_3 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_3, 0, x_2); -lean_ctor_set(x_3, 1, x_1); -return x_3; -} -} -static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__4() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__3; -x_3 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_3, 0, x_2); -lean_ctor_set(x_3, 1, x_1); -return x_3; -} -} -static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__5() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_myMacro____x40_Init_Notation___hyg_2191____closed__2; x_2 = l_Lean_Meta_assert___closed__1; x_3 = lean_name_mk_string(x_1, x_2); @@ -31241,8 +31332,8 @@ x_36 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__4; lean_inc(x_5); lean_inc(x_11); x_37 = l_Lean_addMacroScope(x_11, x_36, x_5); -x_38 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__4; -x_39 = l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__2; +x_38 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__3; +x_39 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__6; lean_inc(x_37); lean_inc(x_24); x_40 = lean_alloc_ctor(3, 4, 0); @@ -31293,7 +31384,7 @@ x_62 = lean_ctor_get(x_60, 0); x_63 = l_myMacro____x40_Init_Notation___hyg_10982____closed__7; x_64 = l_Lean_addMacroScope(x_11, x_63, x_5); x_65 = l_myMacro____x40_Init_Notation___hyg_10982____closed__3; -x_66 = l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__4; +x_66 = l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__2; lean_inc(x_62); x_67 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_67, 0, x_62); @@ -31411,7 +31502,7 @@ lean_dec(x_60); x_119 = l_myMacro____x40_Init_Notation___hyg_10982____closed__7; x_120 = l_Lean_addMacroScope(x_11, x_119, x_5); x_121 = l_myMacro____x40_Init_Notation___hyg_10982____closed__3; -x_122 = l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__4; +x_122 = l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__2; lean_inc(x_117); x_123 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_123, 0, x_117); @@ -31559,7 +31650,7 @@ lean_ctor_set(x_187, 0, x_186); lean_ctor_set(x_187, 1, x_185); x_188 = lean_array_push(x_182, x_187); x_189 = lean_array_push(x_188, x_2); -x_190 = l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__5; +x_190 = l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__3; x_191 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_191, 0, x_190); lean_ctor_set(x_191, 1, x_189); @@ -31593,7 +31684,7 @@ lean_ctor_set(x_203, 0, x_202); lean_ctor_set(x_203, 1, x_201); x_204 = lean_array_push(x_198, x_203); x_205 = lean_array_push(x_204, x_2); -x_206 = l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__5; +x_206 = l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__3; x_207 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_207, 0, x_206); lean_ctor_set(x_207, 1, x_205); @@ -31768,8 +31859,8 @@ x_270 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__4; lean_inc(x_5); lean_inc(x_245); x_271 = l_Lean_addMacroScope(x_245, x_270, x_5); -x_272 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__4; -x_273 = l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__2; +x_272 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__3; +x_273 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__6; lean_inc(x_271); lean_inc(x_258); x_274 = lean_alloc_ctor(3, 4, 0); @@ -31827,7 +31918,7 @@ if (lean_is_exclusive(x_294)) { x_298 = l_myMacro____x40_Init_Notation___hyg_10982____closed__7; x_299 = l_Lean_addMacroScope(x_245, x_298, x_5); x_300 = l_myMacro____x40_Init_Notation___hyg_10982____closed__3; -x_301 = l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__4; +x_301 = l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__2; lean_inc(x_295); x_302 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_302, 0, x_295); @@ -31985,7 +32076,7 @@ lean_ctor_set(x_367, 0, x_366); lean_ctor_set(x_367, 1, x_365); x_368 = lean_array_push(x_362, x_367); x_369 = lean_array_push(x_368, x_2); -x_370 = l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__5; +x_370 = l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__3; x_371 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_371, 0, x_370); lean_ctor_set(x_371, 1, x_369); @@ -40014,12 +40105,12 @@ x_1798 = lean_alloc_ctor(2, 2, 0); lean_ctor_set(x_1798, 0, x_1742); lean_ctor_set(x_1798, 1, x_1797); x_1799 = lean_array_push(x_1747, x_1798); -x_1800 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__12; +x_1800 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__10; lean_inc(x_1743); lean_inc(x_1744); x_1801 = l_Lean_addMacroScope(x_1744, x_1800, x_1743); -x_1802 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__11; -x_1803 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__14; +x_1802 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__9; +x_1803 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__12; lean_inc(x_1742); x_1804 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_1804, 0, x_1742); @@ -40364,12 +40455,12 @@ x_1978 = lean_alloc_ctor(2, 2, 0); lean_ctor_set(x_1978, 0, x_1921); lean_ctor_set(x_1978, 1, x_1977); x_1979 = lean_array_push(x_1927, x_1978); -x_1980 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__12; +x_1980 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__10; lean_inc(x_1923); lean_inc(x_1924); x_1981 = l_Lean_addMacroScope(x_1924, x_1980, x_1923); -x_1982 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__11; -x_1983 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__14; +x_1982 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__9; +x_1983 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__12; lean_inc(x_1921); x_1984 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_1984, 0, x_1921); @@ -40723,12 +40814,12 @@ x_2162 = lean_alloc_ctor(2, 2, 0); lean_ctor_set(x_2162, 0, x_2106); lean_ctor_set(x_2162, 1, x_2161); x_2163 = lean_array_push(x_2111, x_2162); -x_2164 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__18; +x_2164 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__16; lean_inc(x_2107); lean_inc(x_2108); x_2165 = l_Lean_addMacroScope(x_2108, x_2164, x_2107); -x_2166 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__17; -x_2167 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__20; +x_2166 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__15; +x_2167 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__18; lean_inc(x_2106); x_2168 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_2168, 0, x_2106); @@ -41168,12 +41259,12 @@ x_2390 = lean_alloc_ctor(2, 2, 0); lean_ctor_set(x_2390, 0, x_2333); lean_ctor_set(x_2390, 1, x_2389); x_2391 = lean_array_push(x_2339, x_2390); -x_2392 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__18; +x_2392 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__16; lean_inc(x_2335); lean_inc(x_2336); x_2393 = l_Lean_addMacroScope(x_2336, x_2392, x_2335); -x_2394 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__17; -x_2395 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__20; +x_2394 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__15; +x_2395 = l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__18; lean_inc(x_2333); x_2396 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_2396, 0, x_2333); @@ -54213,10 +54304,10 @@ x_240 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_240, 0, x_239); lean_ctor_set(x_240, 1, x_238); x_241 = lean_array_push(x_235, x_240); -x_242 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__5; +x_242 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__6; x_243 = l_Lean_addMacroScope(x_172, x_242, x_169); -x_244 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__2; -x_245 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__5; +x_244 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__5; +x_245 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__8; lean_inc(x_166); x_246 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_246, 0, x_166); @@ -54682,12 +54773,12 @@ x_483 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_483, 0, x_482); lean_ctor_set(x_483, 1, x_481); x_484 = lean_array_push(x_478, x_483); -x_485 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__5; +x_485 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__6; lean_inc(x_374); lean_inc(x_377); x_486 = l_Lean_addMacroScope(x_377, x_485, x_374); -x_487 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__2; -x_488 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__5; +x_487 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__5; +x_488 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__8; lean_inc(x_371); x_489 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_489, 0, x_371); @@ -55569,10 +55660,10 @@ x_863 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_863, 0, x_862); lean_ctor_set(x_863, 1, x_861); x_864 = lean_array_push(x_858, x_863); -x_865 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__5; +x_865 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__6; x_866 = l_Lean_addMacroScope(x_795, x_865, x_792); -x_867 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__2; -x_868 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__5; +x_867 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__5; +x_868 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__8; lean_inc(x_789); x_869 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_869, 0, x_789); @@ -56038,12 +56129,12 @@ x_1106 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_1106, 0, x_1105); lean_ctor_set(x_1106, 1, x_1104); x_1107 = lean_array_push(x_1101, x_1106); -x_1108 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__5; +x_1108 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__6; lean_inc(x_997); lean_inc(x_1000); x_1109 = l_Lean_addMacroScope(x_1000, x_1108, x_997); -x_1110 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__2; -x_1111 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__5; +x_1110 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__5; +x_1111 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__8; lean_inc(x_994); x_1112 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_1112, 0, x_994); @@ -62835,7 +62926,7 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); return x_5; } } -lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_27039_(lean_object* x_1) { +lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_27109_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; @@ -63271,8 +63362,6 @@ l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__5 = _init_l___pri lean_mark_persistent(l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__5); l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__6 = _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__6(); lean_mark_persistent(l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__6); -l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__7 = _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__7(); -lean_mark_persistent(l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkUnit___closed__7); l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__1 = _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__1(); lean_mark_persistent(l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__1); l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__2 = _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__2(); @@ -63283,6 +63372,12 @@ l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__4 = _init_l__ lean_mark_persistent(l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__4); l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__5 = _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__5(); lean_mark_persistent(l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__5); +l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__6 = _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__6(); +lean_mark_persistent(l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__6); +l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__7 = _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__7(); +lean_mark_persistent(l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__7); +l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__8 = _init_l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__8(); +lean_mark_persistent(l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkPureUnit___closed__8); l_Lean_Elab_Term_Do_mkMatch___boxed__const__1 = _init_l_Lean_Elab_Term_Do_mkMatch___boxed__const__1(); lean_mark_persistent(l_Lean_Elab_Term_Do_mkMatch___boxed__const__1); l_Lean_Elab_Term_Do_concat___closed__1 = _init_l_Lean_Elab_Term_Do_concat___closed__1(); @@ -63574,20 +63669,12 @@ l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__17 = _init_l_Lean_Elab lean_mark_persistent(l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__17); l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__18 = _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__18(); lean_mark_persistent(l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__18); -l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__19 = _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__19(); -lean_mark_persistent(l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__19); -l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__20 = _init_l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__20(); -lean_mark_persistent(l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTerm___closed__20); l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__1 = _init_l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__1(); lean_mark_persistent(l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__1); l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__2 = _init_l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__2(); lean_mark_persistent(l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__2); l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__3 = _init_l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__3(); lean_mark_persistent(l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__3); -l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__4 = _init_l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__4(); -lean_mark_persistent(l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__4); -l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__5 = _init_l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__5(); -lean_mark_persistent(l_Lean_Elab_Term_Do_ToTerm_seqToTerm___closed__5); l_Lean_Elab_Term_Do_ToTerm_reassignToTerm___closed__1 = _init_l_Lean_Elab_Term_Do_ToTerm_reassignToTerm___closed__1(); lean_mark_persistent(l_Lean_Elab_Term_Do_ToTerm_reassignToTerm___closed__1); l_Lean_Elab_Term_Do_ToTerm_reassignToTerm___closed__2 = _init_l_Lean_Elab_Term_Do_ToTerm_reassignToTerm___closed__2(); @@ -63856,7 +63943,7 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Do_elabDo___closed__1); res = l___regBuiltin_Lean_Elab_Term_Do_elabDo(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); -res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_27039_(lean_io_mk_world()); +res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_27109_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); l___regBuiltin_Lean_Elab_Term_expandTermFor___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_expandTermFor___closed__1(); diff --git a/stage0/stdlib/Lean/Server/FileWorker.c b/stage0/stdlib/Lean/Server/FileWorker.c index 44d880d456..f6590d3c62 100644 --- a/stage0/stdlib/Lean/Server/FileWorker.c +++ b/stage0/stdlib/Lean/Server/FileWorker.c @@ -67,6 +67,7 @@ lean_object* lean_array_uget(lean_object*, size_t); lean_object* l_Lean_Server_FileWorker_parseParams___at_Lean_Server_FileWorker_handleRequest___spec__3(lean_object*, lean_object*, lean_object*); lean_object* lean_io_error_to_string(lean_object*); lean_object* l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap___closed__4; +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonHoverParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_87_(lean_object*); lean_object* l_Lean_Server_FileWorker_workerMain_match__1___rarg(lean_object*); lean_object* l_IO_FS_Stream_writeLspResponse___at_Lean_Server_FileWorker_handleRequest___spec__7(lean_object*, lean_object*, lean_object*); lean_object* l_List_map___at_Lean_Server_FileWorker_handleDocumentSymbol___spec__1(lean_object*); @@ -378,7 +379,7 @@ lean_object* l_IO_appDir___at_Lean_getBuiltinSearchPath___spec__1(lean_object*); lean_object* l_Lean_Server_FileWorker_handleDefinition_match__2___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Server_FileWorker_parseParams___at_Lean_Server_FileWorker_handleRequest___spec__8___boxed(lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_docStringExt; -lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_239_(lean_object*); +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_411_(lean_object*); lean_object* l_Lean_Server_FileWorker_parseParams_match__1(lean_object*, lean_object*); lean_object* l_ReaderT_pure___at_Lean_Server_FileWorker_handleHover___spec__1(lean_object*); extern lean_object* l_Lean_Parser_instInhabitedModuleParserState___closed__1; @@ -23778,7 +23779,7 @@ lean_object* l_Lean_Server_FileWorker_parseParams___at_Lean_Server_FileWorker_ha _start: { lean_object* x_4; -x_4 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_239_(x_1); +x_4 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_411_(x_1); if (lean_obj_tag(x_4) == 0) { lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; @@ -23921,7 +23922,7 @@ lean_object* l_Lean_Server_FileWorker_parseParams___at_Lean_Server_FileWorker_ha _start: { lean_object* x_4; -x_4 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1299_(x_1); +x_4 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonHoverParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_87_(x_1); if (lean_obj_tag(x_4) == 0) { lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; diff --git a/stage0/stdlib/Lean/Server/Watchdog.c b/stage0/stdlib/Lean/Server/Watchdog.c index 8fa17d554d..5491a340b8 100644 --- a/stage0/stdlib/Lean/Server/Watchdog.c +++ b/stage0/stdlib/Lean/Server/Watchdog.c @@ -42,7 +42,6 @@ lean_object* l___private_Lean_Data_Lsp_TextSync_0__Lean_Lsp_fromJsonDidOpenTextD lean_object* l_Lean_Server_Watchdog_FileWorker_writeRequest___at_Lean_Server_Watchdog_handleRequest___spec__2(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Server_Watchdog_tryWriteMessage___at_Lean_Server_Watchdog_handleRequest___spec__26(lean_object*, lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Server_Watchdog_tryWriteMessage___at_Lean_Server_Watchdog_handleEdits___spec__4___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1299_(lean_object*); lean_object* l_Lean_Server_Watchdog_tryWriteMessage___at_Lean_Server_Watchdog_handleRequest___spec__5___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Server_Watchdog_handleDidOpen(lean_object*, lean_object*, lean_object*); extern lean_object* l_Char_quote___closed__1; @@ -56,6 +55,7 @@ lean_object* lean_io_error_to_string(lean_object*); lean_object* l_Lean_Server_Watchdog_handleNotification___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Server_Watchdog_handleEdits___lambda__1___closed__1; lean_object* l_Lean_Server_Watchdog_tryWriteMessage___at_Lean_Server_Watchdog_handleEdits___spec__4(lean_object*, lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*); +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonHoverParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_87_(lean_object*); lean_object* l_IO_FS_Stream_putStrLn___at_Lean_Server_Watchdog_log___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Server_Watchdog_tryWriteMessage___rarg___closed__3; lean_object* l_Lean_Server_Watchdog_FileWorker_runEditsSignalTask_match__1(lean_object*); @@ -122,6 +122,7 @@ lean_object* lean_array_get_size(lean_object*); lean_object* lean_string_append(lean_object*, lean_object*); lean_object* l_Lean_Server_Watchdog_FileWorker_writeRequest___at_Lean_Server_Watchdog_handleRequest___spec__9(lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Server_Watchdog_0__Lean_Server_Watchdog_forwardMessages_loop___closed__3; +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDeclarationParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_168_(lean_object*); lean_object* l_Lean_Server_Watchdog_mainLoop_match__4(lean_object*); lean_object* l_Std_RBNode_forIn_visit___at_Lean_Server_Watchdog_mainLoop___spec__3(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_IO_FS_Stream_readNotificationAs___at_Lean_Server_Watchdog_initAndRunWatchdogAux___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*); @@ -150,6 +151,7 @@ lean_object* l_Lean_Server_Watchdog_startFileWorker___closed__4; uint32_t lean_uint32_of_nat(lean_object*); uint8_t l_USize_decLt(size_t, size_t); lean_object* l_Lean_Server_Watchdog_FileWorker_writeNotification___at_Lean_Server_Watchdog_handleEdits___spec__1(lean_object*, lean_object*, lean_object*); +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonTypeDefinitionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_374_(lean_object*); lean_object* l_IO_FS_Stream_readRequestAs___at_Lean_Server_Watchdog_initAndRunWatchdog___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Server_Watchdog_tryWriteMessage___at_Lean_Server_Watchdog_handleRequest___spec__19___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_IO_FS_Stream_readMessage(lean_object*, lean_object*, lean_object*); @@ -266,9 +268,11 @@ lean_object* l_Lean_Server_Watchdog_initAndRunWatchdog___lambda__1(lean_object*, lean_object* l_Lean_Json_toStructured_x3f___at_Lean_Server_Watchdog_handleCancelRequest___spec__4(lean_object*); lean_object* l_Lean_Server_Watchdog_FileWorker_errorPendingRequests(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*); extern lean_object* l___private_Init_Util_0__mkPanicMessage___closed__2; +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDeclarationParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_212_(lean_object*); lean_object* l_Lean_Server_Watchdog_FileWorker_errorPendingRequests_match__1(lean_object*); lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonCancelParams____x40_Lean_Data_Lsp_Basic___hyg_59_(lean_object*); lean_object* lean_task_map(lean_object*, lean_object*, lean_object*); +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDefinitionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_249_(lean_object*); lean_object* l_IO_FS_Stream_putStrLn___at_Lean_Server_Watchdog_handleNotification___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Server_Watchdog_FileWorker_runEditsSignalTask___lambda__1___boxed(lean_object*); lean_object* l_Lean_Server_Watchdog_handleEdits_match__1(lean_object*); @@ -293,7 +297,6 @@ lean_object* l_Lean_Server_Watchdog_handleRequest___closed__6; lean_object* l_Lean_Server_Watchdog_handleCrash(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Server_Watchdog_initAndRunWatchdogAux___closed__1; lean_object* l_Lean_Server_Watchdog_FileWorker_errorPendingRequests_match__2(lean_object*, lean_object*); -lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1265_(lean_object*); lean_object* l_Lean_Server_Watchdog_tryWriteMessage___at_Lean_Server_Watchdog_handleRequest___spec__12___closed__2; lean_object* l_Lean_Server_Watchdog_tryWriteMessage___at_Lean_Server_Watchdog_handleRequest___spec__38___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Server_Watchdog_mainLoop_match__2___rarg(lean_object*, lean_object*, lean_object*); @@ -317,8 +320,9 @@ lean_object* l_Lean_Server_Watchdog_FileWorker_stdout(lean_object*); lean_object* lean_server_watchdog_main(lean_object*, lean_object*); lean_object* l_Lean_Json_opt___at_Lean_JsonRpc_instToJsonMessage___spec__1(lean_object*, lean_object*); lean_object* l_IO_mkRef___at_Lean_Server_Watchdog_startFileWorker___spec__2___boxed(lean_object*, lean_object*, lean_object*); +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDefinitionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_293_(lean_object*); lean_object* l_Lean_Server_Watchdog_handleNotification_match__1(lean_object*); -lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_239_(lean_object*); +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_411_(lean_object*); lean_object* l_Lean_Server_Watchdog_tryWriteMessage___at_Lean_Server_Watchdog_handleRequest___spec__26___closed__1; lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_Watchdog_handleRequest___spec__6(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Server_Watchdog_tryWriteMessage___at_Lean_Server_Watchdog_handleRequest___spec__26___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -416,6 +420,7 @@ lean_object* l_Lean_Json_toStructured_x3f___at_Lean_Server_Watchdog_handleReques lean_object* l_Lean_Server_Watchdog_mainLoop_match__4___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_Watchdog_tryWriteMessage___spec__1(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_JsonRpc_instToJsonErrorCode___closed__20; +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonHoverParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_131_(lean_object*); lean_object* l_Lean_Server_Watchdog_handleRequest(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Std_RBNode_forIn_visit___at_Lean_Server_Watchdog_shutdown___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Server_Watchdog_handleRequest_match__1___rarg___closed__2; @@ -490,6 +495,7 @@ lean_object* l_Lean_Server_Watchdog_tryWriteMessage___at_Lean_Server_Watchdog_ha lean_object* l_Lean_Server_Watchdog_updateFileWorkers___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Server_Watchdog_tryWriteMessage___at_Lean_Server_Watchdog_handleRequest___spec__12___lambda__2(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Server_Watchdog_FileWorker_runEditsSignalTask_loopAction(lean_object*, lean_object*); +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonTypeDefinitionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_330_(lean_object*); lean_object* l_IO_FS_Stream_writeLspNotification___at_Lean_Server_Watchdog_handleEdits___spec__2(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Server_Watchdog_mkLeanServerCapabilities___closed__3; extern lean_object* l_Lean_JsonRpc_instToJsonMessage___closed__4; @@ -514,7 +520,7 @@ lean_object* l_Lean_Server_maybeTee(lean_object*, uint8_t, lean_object*, lean_ob lean_object* lean_io_app_dir(lean_object*); lean_object* l_IO_FS_Stream_writeLspRequest___at_Lean_Server_Watchdog_handleRequest___spec__31(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Server_Watchdog_mkLeanServerCapabilities___closed__1; -lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_269_(lean_object*); +lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_441_(lean_object*); lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_Watchdog_tryWriteMessage___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Std_RBNode_forIn_visit___at_Lean_Server_Watchdog_FileWorker_errorPendingRequests___spec__1(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Server_Watchdog_tryWriteMessage___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -11537,7 +11543,7 @@ lean_object* l_Lean_Server_Watchdog_parseParams___at_Lean_Server_Watchdog_handle _start: { lean_object* x_4; -x_4 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_239_(x_1); +x_4 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_411_(x_1); if (lean_obj_tag(x_4) == 0) { lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; @@ -11568,7 +11574,7 @@ lean_object* l_Lean_Json_toStructured_x3f___at_Lean_Server_Watchdog_handleReques _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; -x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_269_(x_1); +x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_441_(x_1); x_3 = lean_ctor_get(x_2, 0); lean_inc(x_3); lean_dec(x_2); @@ -12163,7 +12169,7 @@ lean_object* l_Lean_Server_Watchdog_parseParams___at_Lean_Server_Watchdog_handle _start: { lean_object* x_4; -x_4 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1299_(x_1); +x_4 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonTypeDefinitionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_330_(x_1); if (lean_obj_tag(x_4) == 0) { lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; @@ -12194,7 +12200,7 @@ lean_object* l_Lean_Json_toStructured_x3f___at_Lean_Server_Watchdog_handleReques _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; -x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1265_(x_1); +x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonTypeDefinitionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_374_(x_1); x_3 = lean_ctor_get(x_2, 0); lean_inc(x_3); lean_dec(x_2); @@ -12789,7 +12795,7 @@ lean_object* l_Lean_Server_Watchdog_parseParams___at_Lean_Server_Watchdog_handle _start: { lean_object* x_4; -x_4 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1299_(x_1); +x_4 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDefinitionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_249_(x_1); if (lean_obj_tag(x_4) == 0) { lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; @@ -12820,7 +12826,7 @@ lean_object* l_Lean_Json_toStructured_x3f___at_Lean_Server_Watchdog_handleReques _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; -x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1265_(x_1); +x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDefinitionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_293_(x_1); x_3 = lean_ctor_get(x_2, 0); lean_inc(x_3); lean_dec(x_2); @@ -13415,7 +13421,7 @@ lean_object* l_Lean_Server_Watchdog_parseParams___at_Lean_Server_Watchdog_handle _start: { lean_object* x_4; -x_4 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1299_(x_1); +x_4 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDeclarationParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_168_(x_1); if (lean_obj_tag(x_4) == 0) { lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; @@ -13446,7 +13452,7 @@ lean_object* l_Lean_Json_toStructured_x3f___at_Lean_Server_Watchdog_handleReques _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; -x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1265_(x_1); +x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDeclarationParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_212_(x_1); x_3 = lean_ctor_get(x_2, 0); lean_inc(x_3); lean_dec(x_2); @@ -14041,7 +14047,7 @@ lean_object* l_Lean_Server_Watchdog_parseParams___at_Lean_Server_Watchdog_handle _start: { lean_object* x_4; -x_4 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1299_(x_1); +x_4 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonHoverParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_87_(x_1); if (lean_obj_tag(x_4) == 0) { lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; @@ -14072,7 +14078,7 @@ lean_object* l_Lean_Json_toStructured_x3f___at_Lean_Server_Watchdog_handleReques _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; -x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1265_(x_1); +x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonHoverParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_131_(x_1); x_3 = lean_ctor_get(x_2, 0); lean_inc(x_3); lean_dec(x_2);