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

chore: update stage0

Browse source
This commit is contained in:
Sebastian Ullrich 2021-12-15 15:51:46 +01:00
parent c8c39aa4bb
commit 35e623fca0
46 changed files with 7450 additions and 6407 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
stage0/src/Init/Data/String/Basic.lean generated
View file

@ -126,6 +126,14 @@ def revFind (s : String) (p : Char → Bool) : Option Pos :=
if s.bsize == 0 then none
else revFindAux s p (s.prev s.bsize)
/-- Returns the first position where the two strings differ. -/
partial def firstDiffPos (a b : String) : Pos :=
let stopPos := a.bsize.min b.bsize
let rec loop (i : Pos) : Pos :=
if i == stopPos || a.get i != b.get i then i
else loop (a.next i)
loop 0
private def utf8ExtractAux₂ : List Char → Pos → Pos → List Char
| [], _, _ => []
| c::cs, i, e => if i = e then [] else c :: utf8ExtractAux₂ cs (i + csize c) e

8
stage0/src/Init/Notation.lean generated
View file

@ -137,12 +137,16 @@ infixr:100 " <$> " => Functor.map
macro_rules | `($x <|> $y) => `(binop_lazy% HOrElse.hOrElse $x $y)
macro_rules | `($x >> $y) => `(binop_lazy% HAndThen.hAndThen $x $y)
syntax (name := termDepIfThenElse) ppGroup(ppDedent("if " ident " : " term " then" ppSpace term ppDedent(ppSpace "else") ppSpace term)) : term
syntax (name := termDepIfThenElse)
ppRealGroup(ppRealFill(ppIndent("if " ident " : " term " then") ppSpace term)
ppDedent(ppSpace) ppRealFill("else " term)) : term
macro_rules
| `(if $h:ident : $c then $t:term else $e:term) => `(let_mvar% ?m := $c; wait_if_type_mvar% ?m; dite ?m (fun $h:ident => $t) (fun $h:ident => $e))
syntax (name := termIfThenElse) ppGroup(ppDedent("if " term " then" ppSpace term ppDedent(ppSpace "else") ppSpace term)) : term
syntax (name := termIfThenElse)
ppRealGroup(ppRealFill(ppIndent("if " term " then") ppSpace term)
ppDedent(ppSpace) ppRealFill("else " term)) : term
macro_rules
| `(if $c then $t:term else $e:term) => `(let_mvar% ?m := $c; wait_if_type_mvar% ?m; ite ?m $t $e)

1
stage0/src/Lean.lean generated
View file

@ -30,4 +30,5 @@ import Lean.ScopedEnvExtension
import Lean.DocString
import Lean.DeclarationRange
import Lean.LazyInitExtension
import Lean.LoadDynlib
import Lean.Widget

3
stage0/src/Lean/Compiler/IR/EmitC.lean generated
View file

@ -187,7 +187,8 @@ def emitMainFn : M Unit := do
let retTy := env.find? `main |>.get! |>.type |>.getForallBody
-- either `UInt32` or `(P)Unit`
let retTy := retTy.appArg!
emitLns ["if (lean_io_result_is_ok(res)) {",
emitLns ["lean_finalize_task_manager();",
"if (lean_io_result_is_ok(res)) {",
" int ret = " ++ if retTy.constName? == some ``UInt32 then "lean_unbox_uint32(lean_io_result_get_value(res));" else "0;",
" lean_dec_ref(res);",
" return ret;",

15
stage0/src/Lean/Data/Lsp/Extra.lean generated
View file

@ -35,8 +35,23 @@ instance : FromJson WaitForDiagnostics :=
instance : ToJson WaitForDiagnostics :=
⟨fun o => mkObj []⟩
inductive LeanFileProgressKind
| processing | fatalError
deriving Inhabited, BEq
instance : FromJson LeanFileProgressKind := ⟨fun j =>
match j.getNat? with
| Except.ok 1 => LeanFileProgressKind.processing
| Except.ok 2 => LeanFileProgressKind.fatalError
| _ => throw s!"unknown LeanFileProgressKind '{j}'"⟩
instance : ToJson LeanFileProgressKind := ⟨fun
| LeanFileProgressKind.processing => 1
| LeanFileProgressKind.fatalError => 2⟩
structure LeanFileProgressProcessingInfo where
range : Range
kind : LeanFileProgressKind := LeanFileProgressKind.processing
deriving FromJson, ToJson
/-- `$/lean/fileProgress` client<-server notification.

1
stage0/src/Lean/Elab/Match.lean generated
View file

@ -63,6 +63,7 @@ private def elabAtomicDiscr (discr : Syntax) : TermElabM Expr := do
| some e@(Expr.fvar fvarId _) =>
let localDecl ← getLocalDecl fvarId
if !isAuxDiscrName localDecl.userName then
addTermInfo discr e
return e -- it is not an auxiliary local created by `expandNonAtomicDiscrs?`
else
instantiateMVars localDecl.value

2
stage0/src/Lean/Elab/Term.lean generated
View file

@ -1438,7 +1438,7 @@ def mkConst (constName : Name) (explicitLevels : List Level := []) : TermElabM E
else
let numMissingLevels := cinfo.levelParams.length - explicitLevels.length
let us ← mkFreshLevelMVars numMissingLevels
pure $ Lean.mkConst constName (explicitLevels ++ us)
return Lean.mkConst constName (explicitLevels ++ us)
private def mkConsts (candidates : List (Name × List String)) (explicitLevels : List Level) : TermElabM (List (Expr × List String)) := do
candidates.foldlM (init := []) fun result (constName, projs) => do

17
stage0/src/Lean/LoadDynlib.lean generated Normal file
View file

@ -0,0 +1,17 @@
/-
Copyright (c) 2021 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
namespace Lean
/--
Dynamically loads a shared library so that its symbols can be used by
the Lean interpreter (e.g., for interpreting `@[extern]` declarations).
Equivalent to passing `--load-dynlib=lib` to `lean`.
Note that Lean never unloads libraries.
-/
@[extern "lean_load_dynlib"]
constant loadDynlib (path : @& System.FilePath) : IO Unit

48
stage0/src/Lean/Parser/Basic.lean generated
View file

@ -1817,54 +1817,6 @@ def categoryParserOfStackFn (offset : Nat) : ParserFn := fun ctx s =>
def categoryParserOfStack (offset : Nat) (prec : Nat := 0) : Parser :=
{ fn := fun c s => categoryParserOfStackFn offset { c with prec := prec } s }
unsafe def evalParserConstUnsafe (declName : Name) : ParserFn := fun ctx s =>
match ctx.env.evalConstCheck Parser ctx.options `Lean.Parser.Parser declName <|>
ctx.env.evalConstCheck Parser ctx.options `Lean.Parser.TrailingParser declName with
| Except.ok p => p.fn ctx s
| Except.error e => s.mkUnexpectedError s!"error running parser {declName}: {e}"
@[implementedBy evalParserConstUnsafe]
constant evalParserConst (declName : Name) : ParserFn
unsafe def parserOfStackFnUnsafe (offset : Nat) : ParserFn := fun ctx s =>
let stack := s.stxStack
if stack.size < offset + 1 then
s.mkUnexpectedError ("failed to determine parser using syntax stack, stack is too small")
else
match stack.get! (stack.size - offset - 1) with
| Syntax.ident (val := parserName) .. =>
match ctx.resolveName parserName with
| [(parserName, [])] =>
let iniSz := s.stackSize
let s := evalParserConst parserName ctx s
if !s.hasError && s.stackSize != iniSz + 1 then
s.mkUnexpectedError "expected parser to return exactly one syntax object"
else
s
| _::_::_ => s.mkUnexpectedError s!"ambiguous parser name {parserName}"
| _ => s.mkUnexpectedError s!"unknown parser {parserName}"
| _ => s.mkUnexpectedError ("failed to determine parser using syntax stack, the specified element on the stack is not an identifier")
@[implementedBy parserOfStackFnUnsafe]
constant parserOfStackFn (offset : Nat) : ParserFn
def parserOfStack (offset : Nat) (prec : Nat := 0) : Parser :=
{ fn := fun c s => parserOfStackFn offset { c with prec := prec } s }
register_builtin_option internal.parseQuotWithCurrentStage : Bool := {
defValue := false
group := "internal"
descr := "(Lean bootstrapping) use parsers from the current stage inside quotations"
}
/-- Run `declName` if possible and inside a quotation, or else `p`. The `ParserInfo` will always be taken from `p`. -/
def evalInsideQuot (declName : Name) (p : Parser) : Parser := { p with
fn := fun c s =>
if c.quotDepth > 0 && !c.suppressInsideQuot && internal.parseQuotWithCurrentStage.get c.options && c.env.contains declName then
evalParserConst declName c s
else
p.fn c s }
private def mkResult (s : ParserState) (iniSz : Nat) : ParserState :=
if s.stackSize == iniSz + 1 then s
else s.mkNode nullKind iniSz -- throw error instead?

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

@ -147,20 +147,6 @@ private def updateBuiltinTokens (info : ParserInfo) (declName : Name) : IO Unit
| Except.ok tokenTable => builtinTokenTable.set tokenTable
| Except.error msg => throw (IO.userError s!"invalid builtin parser '{declName}', {msg}")
def addBuiltinParser (catName : Name) (declName : Name) (leading : Bool) (p : Parser) (prio : Nat) : IO Unit := do
let p := evalInsideQuot declName p
let categories ← builtinParserCategoriesRef.get
let categories ← IO.ofExcept $ addParser categories catName declName leading p prio
builtinParserCategoriesRef.set categories
builtinSyntaxNodeKindSetRef.modify p.info.collectKinds
updateBuiltinTokens p.info declName
def addBuiltinLeadingParser (catName : Name) (declName : Name) (p : Parser) (prio : Nat) : IO Unit :=
addBuiltinParser catName declName true p prio
def addBuiltinTrailingParser (catName : Name) (declName : Name) (p : TrailingParser) (prio : Nat) : IO Unit :=
addBuiltinParser catName declName false p prio
def ParserExtension.addEntryImpl (s : State) (e : Entry) : State :=
match e with
| Entry.token tk =>
@ -178,34 +164,6 @@ def ParserExtension.addEntryImpl (s : State) (e : Entry) : State :=
| Except.ok categories => { s with categories := categories }
| _ => unreachable!
unsafe def mkParserOfConstantUnsafe
(categories : ParserCategories) (constName : Name) (compileParserDescr : ParserDescr → ImportM Parser) : ImportM (Bool × Parser) := do
let env := (← read).env
let opts := (← read).opts
match env.find? constName with
| none => throw ↑s!"unknow constant '{constName}'"
| some info =>
match info.type with
| Expr.const `Lean.Parser.TrailingParser _ _ =>
let p ← IO.ofExcept $ env.evalConst Parser opts constName
pure ⟨false, p⟩
| Expr.const `Lean.Parser.Parser _ _ =>
let p ← IO.ofExcept $ env.evalConst Parser opts constName
pure ⟨true, p⟩
| Expr.const `Lean.ParserDescr _ _ =>
let d ← IO.ofExcept $ env.evalConst ParserDescr opts constName
let p ← compileParserDescr d
pure ⟨true, p⟩
| Expr.const `Lean.TrailingParserDescr _ _ =>
let d ← IO.ofExcept $ env.evalConst TrailingParserDescr opts constName
let p ← compileParserDescr d
pure ⟨false, p⟩
| _ => throw ↑s!"unexpected parser type at '{constName}' (`ParserDescr`, `TrailingParserDescr`, `Parser` or `TrailingParser` expected"
@[implementedBy mkParserOfConstantUnsafe]
constant mkParserOfConstantAux
(categories : ParserCategories) (constName : Name) (compileParserDescr : ParserDescr → ImportM Parser) : ImportM (Bool × Parser)
/- Parser aliases for making `ParserDescr` extensible -/
inductive AliasValue (α : Type) where
| const (p : α)
@ -268,6 +226,32 @@ def ensureBinaryParserAlias (aliasName : Name) : IO Unit :=
def ensureConstantParserAlias (aliasName : Name) : IO Unit :=
discard $ getConstAlias parserAliasesRef aliasName
unsafe def mkParserOfConstantUnsafe (constName : Name) (compileParserDescr : ParserDescr → ImportM Parser) : ImportM (Bool × Parser) := do
let env := (← read).env
let opts := (← read).opts
match env.find? constName with
| none => throw ↑s!"unknow constant '{constName}'"
| some info =>
match info.type with
| Expr.const `Lean.Parser.TrailingParser _ _ =>
let p ← IO.ofExcept $ env.evalConst Parser opts constName
pure ⟨false, p⟩
| Expr.const `Lean.Parser.Parser _ _ =>
let p ← IO.ofExcept $ env.evalConst Parser opts constName
pure ⟨true, p⟩
| Expr.const `Lean.ParserDescr _ _ =>
let d ← IO.ofExcept $ env.evalConst ParserDescr opts constName
let p ← compileParserDescr d
pure ⟨true, p⟩
| Expr.const `Lean.TrailingParserDescr _ _ =>
let d ← IO.ofExcept $ env.evalConst TrailingParserDescr opts constName
let p ← compileParserDescr d
pure ⟨false, p⟩
| _ => throw ↑s!"unexpected parser type at '{constName}' (`ParserDescr`, `TrailingParserDescr`, `Parser` or `TrailingParser` expected"
@[implementedBy mkParserOfConstantUnsafe]
constant mkParserOfConstantAux (constName : Name) (compileParserDescr : ParserDescr → ImportM Parser) : ImportM (Bool × Parser)
partial def compileParserDescr (categories : ParserCategories) (d : ParserDescr) : ImportM Parser :=
let rec visit : ParserDescr → ImportM Parser
| ParserDescr.const n => getConstAlias parserAliasesRef n
@ -281,7 +265,7 @@ partial def compileParserDescr (categories : ParserCategories) (d : ParserDescr)
| ParserDescr.symbol tk => return symbol tk
| ParserDescr.nonReservedSymbol tk includeIdent => return nonReservedSymbol tk includeIdent
| ParserDescr.parser constName => do
let (_, p) ← mkParserOfConstantAux categories constName visit;
let (_, p) ← mkParserOfConstantAux constName visit;
pure p
| ParserDescr.cat catName prec =>
match getCategory categories catName with
@ -290,7 +274,7 @@ partial def compileParserDescr (categories : ParserCategories) (d : ParserDescr)
visit d
def mkParserOfConstant (categories : ParserCategories) (constName : Name) : ImportM (Bool × Parser) :=
mkParserOfConstantAux categories constName (compileParserDescr categories)
mkParserOfConstantAux constName (compileParserDescr categories)
structure ParserAttributeHook where
/- Called after a parser attribute is applied to a declaration. -/
@ -354,6 +338,43 @@ def leadingIdentBehavior (env : Environment) (catName : Name) : LeadingIdentBeha
| none => LeadingIdentBehavior.default
| some cat => cat.behavior
unsafe def evalParserConstUnsafe (declName : Name) : ParserFn := fun ctx s => unsafeBaseIO do
let categories := (parserExtension.getState ctx.env).categories
match (← (mkParserOfConstant categories declName { env := ctx.env, opts := ctx.options }).toBaseIO) with
| Except.ok (bool, p) => p.fn ctx s
| Except.error e => s.mkUnexpectedError e.toString
@[implementedBy evalParserConstUnsafe]
constant evalParserConst (declName : Name) : ParserFn
register_builtin_option internal.parseQuotWithCurrentStage : Bool := {
defValue := false
group := "internal"
descr := "(Lean bootstrapping) use parsers from the current stage inside quotations"
}
/-- Run `declName` if possible and inside a quotation, or else `p`. The `ParserInfo` will always be taken from `p`. -/
def evalInsideQuot (declName : Name) (p : Parser) : Parser := { p with
fn := fun c s =>
if c.quotDepth > 0 && !c.suppressInsideQuot && internal.parseQuotWithCurrentStage.get c.options && c.env.contains declName then
evalParserConst declName c s
else
p.fn c s }
def addBuiltinParser (catName : Name) (declName : Name) (leading : Bool) (p : Parser) (prio : Nat) : IO Unit := do
let p := evalInsideQuot declName p
let categories ← builtinParserCategoriesRef.get
let categories ← IO.ofExcept $ addParser categories catName declName leading p prio
builtinParserCategoriesRef.set categories
builtinSyntaxNodeKindSetRef.modify p.info.collectKinds
updateBuiltinTokens p.info declName
def addBuiltinLeadingParser (catName : Name) (declName : Name) (p : Parser) (prio : Nat) : IO Unit :=
addBuiltinParser catName declName true p prio
def addBuiltinTrailingParser (catName : Name) (declName : Name) (p : TrailingParser) (prio : Nat) : IO Unit :=
addBuiltinParser catName declName false p prio
def mkCategoryAntiquotParser (kind : Name) : Parser :=
mkAntiquot kind.toString none
@ -606,5 +627,27 @@ def withOpenDeclFn (p : ParserFn) : ParserFn := fun c s =>
fn := withOpenDeclFn p.fn
}
def parserOfStackFn (offset : Nat) : ParserFn := fun ctx s =>
let stack := s.stxStack
if stack.size < offset + 1 then
s.mkUnexpectedError ("failed to determine parser using syntax stack, stack is too small")
else
match stack.get! (stack.size - offset - 1) with
| Syntax.ident (val := parserName) .. =>
match ctx.resolveName parserName with
| [(parserName, [])] =>
let iniSz := s.stackSize
let s := evalParserConst parserName ctx s
if !s.hasError && s.stackSize != iniSz + 1 then
s.mkUnexpectedError "expected parser to return exactly one syntax object"
else
s
| _::_::_ => s.mkUnexpectedError s!"ambiguous parser name {parserName}"
| _ => s.mkUnexpectedError s!"unknown parser {parserName}"
| _ => s.mkUnexpectedError ("failed to determine parser using syntax stack, the specified element on the stack is not an identifier")
def parserOfStack (offset : Nat) (prec : Nat := 0) : Parser :=
{ fn := fun c s => parserOfStackFn offset { c with prec := prec } s }
end Parser
end Lean

14
stage0/src/Lean/Parser/Term.lean generated
View file

@ -169,7 +169,19 @@ def simpleBinderWithoutType := nodeWithAntiquot "simpleBinder" `Lean.Parser.Term
def letIdLhs : Parser := ident >> notFollowedBy (checkNoWsBefore "" >> "[") "space is required before instance '[...]' binders to distinguish them from array updates `let x[i] := e; ...`" >> many (ppSpace >> (simpleBinderWithoutType <|> bracketedBinder)) >> optType
def letIdDecl := nodeWithAntiquot "letIdDecl" `Lean.Parser.Term.letIdDecl $ atomic (letIdLhs >> " := ") >> termParser
def letPatDecl := nodeWithAntiquot "letPatDecl" `Lean.Parser.Term.letPatDecl $ atomic (termParser >> pushNone >> optType >> " := ") >> termParser
def letEqnsDecl := nodeWithAntiquot "letEqnsDecl" `Lean.Parser.Term.letEqnsDecl $ letIdLhs >> matchAlts
/-
Remark: the following `(" := " <|> matchAlts)` is a hack we use to produce a better error message at `letDecl`.
Consider this following example
```
def myFun (n : Nat) : IO Nat :=
let q ← (10 : Nat)
n + q
```
Without the hack, we get the error `expected '|'` at `←`. Reason: at `letDecl`, we use the parser `(letIdDecl <|> letPatDecl <|> letEqnsDecl)`,
`letIdDecl` and `letEqnsDecl` have the same prefix `letIdLhs`, but `letIdDecl` uses `atomic`.
Note that the hack relies on the fact that the parser `":="` never succeeds at `(" := " <|> matchAlts)`. It is there just to make sure we produce the error `expected ':=' or '|'`
-/
def letEqnsDecl := nodeWithAntiquot "letEqnsDecl" `Lean.Parser.Term.letEqnsDecl $ letIdLhs >> (" := " <|> matchAlts)
-- Remark: we use `nodeWithAntiquot` here to make sure anonymous antiquotations (e.g., `$x`) are not `letDecl`
def letDecl := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl (notFollowedBy (nonReservedSymbol "rec") "rec" >> (letIdDecl <|> letPatDecl <|> letEqnsDecl))
@[builtinTermParser] def «let» := leading_parser:leadPrec withPosition ("let " >> letDecl) >> optSemicolon termParser

12
stage0/src/Lean/Server/FileWorker.lean generated
View file

@ -98,6 +98,8 @@ section Elab
: ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do
if initial && initSnap.msgLog.hasErrors then
-- treat header processing errors as fatal so users aren't swamped with followup errors
let hOut := (←read).hOut
publishProgressAtPos m initSnap.beginPos hOut (kind := LeanFileProgressKind.fatalError)
AsyncList.nil
else
AsyncList.unfoldAsync (nextCmdSnap m . cancelTk (← read)) initSnap
@ -221,9 +223,8 @@ section Updates
def updatePendingRequests (map : PendingRequestMap → PendingRequestMap) : WorkerM Unit := do
modify fun st => { st with pendingRequests := map st.pendingRequests }
/-- Given the new document and `changePos`, the UTF-8 offset of a change into the pre-change source,
updates editable doc state. -/
def updateDocument (newMeta : DocumentMeta) (changePos : String.Pos) : WorkerM Unit := do
/-- Given the new document, updates editable doc state. -/
def updateDocument (newMeta : DocumentMeta) : WorkerM Unit := do
-- The watchdog only restarts the file worker when the syntax tree of the header changes.
-- If e.g. a newline is deleted, it will not restart this file worker, but we still
-- need to reparse the header so that the offsets are correct.
@ -241,6 +242,7 @@ section Updates
| some (ElabTaskError.ioError ioError) => throw ioError
| _ => -- No error or EOF
oldDoc.cancelTk.set
let changePos := oldDoc.meta.text.source.firstDiffPos newMeta.text.source
-- NOTE(WN): we invalidate eagerly as `endPos` consumes input greedily. To re-elaborate only
-- when really necessary, we could do a whitespace-aware `Syntax` comparison instead.
let mut validSnaps := cmdSnaps.finishedPrefix.takeWhile (fun s => s.endPos < changePos)
@ -282,8 +284,8 @@ section NotificationHandling
-- TODO(WN): This happens on restart sometimes.
IO.eprintln s!"Got outdated version number: {newVersion} ≤ {oldDoc.meta.version}"
else if ¬ changes.isEmpty then
let (newDocText, minStartOff) := foldDocumentChanges changes oldDoc.meta.text
updateDocument ⟨docId.uri, newVersion, newDocText⟩ minStartOff
let newDocText := foldDocumentChanges changes oldDoc.meta.text
updateDocument ⟨docId.uri, newVersion, newDocText⟩
def handleCancelRequest (p : CancelParams) : WorkerM Unit := do
updatePendingRequests (fun pendingRequests => pendingRequests.erase p.id)

4
stage0/src/Lean/Server/FileWorker/RequestHandling.lean generated
View file

@ -425,7 +425,9 @@ where
lastPos := ti.stx.getPos?.get!
highlightKeyword stx := do
if let Syntax.atom info val := stx then
if val.bsize > 0 && val[0].isAlpha then
if (val.length > 0 && val[0].isAlpha) ||
-- Support for keywords of the form `#<alpha>...`
(val.length > 1 && val[0] == '#' && val[1].isAlpha) then
addToken stx SemanticTokenType.keyword
addToken stx type := do
let ⟨beginPos, endPos, text, _⟩ ← read

31
stage0/src/Lean/Server/Utils.lean generated
View file

@ -105,23 +105,16 @@ def toFileUri (fname : System.FilePath) : Lsp.DocumentUri :=
open Lsp
/-- Returns the document contents with all changes applied, together with the position of the change
which lands earliest in the file. Panics if there are no changes. -/
def foldDocumentChanges (changes : @& Array Lsp.TextDocumentContentChangeEvent) (oldText : FileMap)
: FileMap × String.Pos :=
if changes.isEmpty then panic! "Lean.Server.foldDocumentChanges: empty change array" else
let accumulateChanges : FileMap × String.Pos → TextDocumentContentChangeEvent → FileMap × String.Pos :=
fun ⟨newDocText, minStartOff⟩ change =>
match change with
| TextDocumentContentChangeEvent.rangeChange (range : Range) (newText : String) =>
let startOff := oldText.lspPosToUtf8Pos range.start
let newDocText := replaceLspRange newDocText range newText
let minStartOff := minStartOff.min startOff
⟨newDocText, minStartOff⟩
| TextDocumentContentChangeEvent.fullChange (newText : String) =>
⟨newText.toFileMap, 0⟩
-- NOTE: We assume Lean files are below 16 EiB.
changes.foldl accumulateChanges (oldText, 0xffffffff)
/-- Returns the document contents with the change applied. -/
def applyDocumentChange (oldText : FileMap) : (change : Lsp.TextDocumentContentChangeEvent) → FileMap
| TextDocumentContentChangeEvent.rangeChange (range : Range) (newText : String) =>
replaceLspRange oldText range newText
| TextDocumentContentChangeEvent.fullChange (newText : String) =>
newText.toFileMap
/-- Returns the document contents with all changes applied. -/
def foldDocumentChanges (changes : Array Lsp.TextDocumentContentChangeEvent) (oldText : FileMap) : FileMap :=
changes.foldl applyDocumentChange oldText
def publishDiagnostics (m : DocumentMeta) (diagnostics : Array Lsp.Diagnostic) (hOut : FS.Stream) : IO Unit :=
hOut.writeLspNotification {
@ -144,8 +137,8 @@ def publishProgress (m : DocumentMeta) (processing : Array LeanFileProgressProce
}
}
def publishProgressAtPos (m : DocumentMeta) (pos : String.Pos) (hOut : FS.Stream) : IO Unit :=
publishProgress m #[{ range := ⟨m.text.utf8PosToLspPos pos, m.text.utf8PosToLspPos m.text.source.bsize⟩ }] hOut
def publishProgressAtPos (m : DocumentMeta) (pos : String.Pos) (hOut : FS.Stream) (kind : LeanFileProgressKind := LeanFileProgressKind.processing) : IO Unit :=
publishProgress m #[{ range := ⟨m.text.utf8PosToLspPos pos, m.text.utf8PosToLspPos m.text.source.bsize⟩, kind := kind }] hOut
def publishProgressDone (m : DocumentMeta) (hOut : FS.Stream) : IO Unit :=
publishProgress m #[] hOut

4
stage0/src/Lean/Server/Watchdog.lean generated
View file

@ -355,7 +355,7 @@ section NotificationHandling
throwServerError "Got outdated version number"
if changes.isEmpty then
return
let (newDocText, _) := foldDocumentChanges changes oldDoc.meta.text
let newDocText := foldDocumentChanges changes oldDoc.meta.text
let newMeta : DocumentMeta := ⟨doc.uri, newVersion, newDocText⟩
let newHeaderAst ← parseHeaderAst newDocText.source
if newHeaderAst != oldDoc.headerAst then
@ -591,7 +591,7 @@ def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do
capabilities := mkLeanServerCapabilities
serverInfo? := some {
name := "Lean 4 Server"
version? := "0.1"
version? := "0.1.1"
}
: InitializeResult
}

9
stage0/src/bin/lean-gdb.py generated
View file

@ -30,9 +30,6 @@ def get_cnstr_tag(o):
def get_num_objs(o):
return o['m_other']
def get_mem_kind(o):
return 0 if o['m_rc'] > 0 else 1 if o['m_rc'] < 0 else 2
def get_rc(o):
return o['m_rc']
@ -76,11 +73,7 @@ class LeanObjectPrinter:
if is_scalar(self.val):
return unbox(self.val)
else:
k = get_mem_kind(self.val)
return "{} ({})".format(LeanObjectPrinter.kinds[self.kind][0],
get_rc(self.val) if k == 0 else
get_rc(self.val) + "/MT" if k == 1 else
"PERSIST")
return "{} ({})".format(LeanObjectPrinter.kinds[self.kind][0], get_rc(self.val))
def children(self):
if is_scalar(self.val):

1
stage0/src/include/lean/lean.h generated
View file

@ -1063,6 +1063,7 @@ static inline lean_obj_res lean_thunk_get_own(b_lean_obj_arg t) {
LEAN_SHARED void lean_init_task_manager();
LEAN_SHARED void lean_init_task_manager_using(unsigned num_workers);
LEAN_SHARED void lean_finalize_task_manager();
LEAN_SHARED lean_obj_res lean_task_spawn_core(lean_obj_arg c, unsigned prio, bool keep_alive);
/* Run a closure `Unit -> A` as a `Task A` */

2
stage0/src/runtime/CMakeLists.txt generated
View file

@ -1,6 +1,6 @@
set(RUNTIME_OBJS debug.cpp thread.cpp mpz.cpp utf8.cpp
object.cpp apply.cpp exception.cpp interrupt.cpp memory.cpp
stackinfo.cpp compact.cpp init_module.cpp io.cpp hash.cpp
stackinfo.cpp compact.cpp init_module.cpp load_dynlib.cpp io.cpp hash.cpp
platform.cpp alloc.cpp allocprof.cpp sharecommon.cpp stack_overflow.cpp
process.cpp object_ref.cpp mpn.cpp)
add_library(leanrt_initial-exec STATIC ${RUNTIME_OBJS})

45
stage0/src/runtime/load_dynlib.cpp generated Normal file
View file

@ -0,0 +1,45 @@
/*
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura, Mac Malone
*/
#include "runtime/io.h"
#include "runtime/object.h"
#include "runtime/sstream.h"
#include "runtime/exception.h"
#include "runtime/load_dynlib.h"
#ifdef LEAN_WINDOWS
#include <windows.h>
#undef ERROR // thanks, wingdi.h
#else
#include <dlfcn.h>
#endif
namespace lean {
void load_dynlib(std::string path) {
#ifdef LEAN_WINDOWS
HMODULE h = LoadLibrary(path.c_str());
if (!h) {
throw exception(sstream() << "error loading library " << path << ": " << GetLastError());
}
#else
void *handle = dlopen(path.c_str(), RTLD_LAZY | RTLD_GLOBAL);
if (!handle) {
throw exception(sstream() << "error loading library, " << dlerror());
}
#endif
// NOTE: we never unload libraries
}
/* loadDynlib : System.FilePath -> IO Unit */
extern "C" LEAN_EXPORT obj_res lean_load_dynlib(b_obj_arg path, obj_arg) {
try {
load_dynlib(string_cstr(path));
return io_result_mk_ok(box(0));
} catch (exception & ex) {
return io_result_mk_error(ex.what());
}
}
}

12
stage0/src/runtime/load_dynlib.h generated Normal file
View file

@ -0,0 +1,12 @@
/*
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Mac Malone
*/
#pragma once
#include <string>
namespace lean {
void load_dynlib(std::string path);
}

7
stage0/src/runtime/object.cpp generated
View file

@ -907,6 +907,13 @@ extern "C" LEAN_EXPORT void lean_init_task_manager() {
lean_init_task_manager_using(hardware_concurrency());
}
extern "C" LEAN_EXPORT void lean_finalize_task_manager() {
if (g_task_manager) {
delete g_task_manager;
g_task_manager = nullptr;
}
}
scoped_task_manager::scoped_task_manager(unsigned num_workers) {
lean_assert(g_task_manager == nullptr);
#if defined(LEAN_MULTI_THREAD)

23
stage0/src/shell/CMakeLists.txt generated
View file

@ -214,9 +214,20 @@ add_test(NAME leanpkgtest_builtin_attr
find . -name '*.olean' -delete
leanmake")
add_test(NAME laketest
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/lake/examples"
COMMAND bash -c "
set -eu
export ${TEST_VARS}
make LAKE=lake test")
# Create a lake test for each subdirectory of `lake/examples` which contains a `test.sh` file.
# We skip the subdirectories `lean_packages` and `bootstrap` since `lake/examples/Makefile` do no consider them.
file(GLOB_RECURSE LEANLAKETESTS "${LEAN_SOURCE_DIR}/lake/examples/test.sh")
FOREACH(T ${LEANLAKETESTS})
if(NOT T MATCHES ".*lean_packages.*")
if(NOT T MATCHES ".*bootstrap.*")
GET_FILENAME_COMPONENT(T_DIR ${T} DIRECTORY)
GET_FILENAME_COMPONENT(DIR_NAME ${T_DIR} NAME)
add_test(NAME "leanlaketest_${DIR_NAME}"
WORKING_DIRECTORY "${T_DIR}"
COMMAND bash -c "
set -eu
export ${TEST_VARS}
LAKE=lake ./test.sh")
endif()
endif()
ENDFOREACH(T)

18
stage0/src/util/shell.cpp generated
View file

@ -19,6 +19,7 @@ Author: Leonardo de Moura
#include "runtime/thread.h"
#include "runtime/debug.h"
#include "runtime/sstream.h"
#include "runtime/load_dynlib.h"
#include "util/timer.h"
#include "util/macros.h"
#include "util/io.h"
@ -320,21 +321,6 @@ void load_plugin(std::string path) {
// NOTE: we never unload plugins
}
void load_library(std::string path) {
#ifdef LEAN_WINDOWS
HMODULE h = LoadLibrary(path.c_str());
if (!h) {
throw exception(sstream() << "error loading library " << path << ": " << GetLastError());
}
#else
void *handle = dlopen(path.c_str(), RTLD_LAZY | RTLD_GLOBAL);
if (!handle) {
throw exception(sstream() << "error loading library, " << dlerror());
}
#endif
// NOTE: we never unload libraries
}
namespace lean {
extern "C" object * lean_run_frontend(object * input, object * opts, object * filename, object * main_module_name, uint32_t trust_level, object * w);
pair_ref<environment, object_ref> run_new_frontend(std::string const & input, options const & opts, std::string const & file_name, name const & main_module_name, uint32_t trust_level) {
@ -553,7 +539,7 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
break;
case 'l':
check_optarg("l");
load_library(optarg);
lean::load_dynlib(optarg);
forwarded_args.push_back(string_ref("--load-dynlib=" + std::string(optarg)));
break;
default:

82
stage0/stdlib/Init/Data/String/Basic.c generated
View file

@ -55,6 +55,7 @@ LEAN_EXPORT lean_object* l_Substring_toString___boxed(lean_object*);
LEAN_EXPORT lean_object* l_String_offsetOfPosAux(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_anyAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_modify(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_firstDiffPos(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_toNat_x3f___lambda__1___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_str___boxed(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Substring_any(lean_object*, lean_object*);
@ -150,6 +151,7 @@ LEAN_EXPORT lean_object* l_String_revFindAux___boxed(lean_object*, lean_object*,
LEAN_EXPORT lean_object* l_String_revFindAux(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_String_substrEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Substring_takeWhile(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_firstDiffPos_loop(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_singleton(uint32_t);
LEAN_EXPORT lean_object* l_String_Iterator_pos(lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__Substring_takeRightWhileAux___at_Substring_trimRight___spec__1___boxed(lean_object*, lean_object*, lean_object*);
@ -161,7 +163,6 @@ LEAN_EXPORT lean_object* l_Substring_foldl(lean_object*);
LEAN_EXPORT uint32_t l_Substring_get(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Substring_any___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_takeRight(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1514____boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_getOp___boxed(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_String_endsWith(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Substring_toIterator(lean_object*);
@ -179,7 +180,7 @@ LEAN_EXPORT lean_object* l_String_revFind(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_splitOn___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_Iterator_prevn(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_foldl(lean_object*);
LEAN_EXPORT uint8_t l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1514_(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1554_(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_foldr___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Substring_beq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_endsWith___boxed(lean_object*, lean_object*);
@ -194,6 +195,7 @@ LEAN_EXPORT lean_object* l_String_splitAux(lean_object*, lean_object*, lean_obje
LEAN_EXPORT lean_object* l_String_takeRightWhile(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_String_Iterator_hasNext(lean_object*);
LEAN_EXPORT lean_object* l_String_all___lambda__1___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_firstDiffPos___boxed(lean_object*, lean_object*);
LEAN_EXPORT uint32_t l_String_front(lean_object*);
LEAN_EXPORT lean_object* l_String_dropWhile___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Substring_atEnd___boxed(lean_object*, lean_object*);
@ -221,6 +223,7 @@ LEAN_EXPORT lean_object* l_String_foldr___rarg___boxed(lean_object*, lean_object
LEAN_EXPORT lean_object* l_Substring_isNat___boxed(lean_object*);
LEAN_EXPORT lean_object* l_String_split(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_any___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1554____boxed(lean_object*, lean_object*);
LEAN_EXPORT uint32_t l_String_Iterator_curr(lean_object*);
LEAN_EXPORT lean_object* l_Substring_foldr(lean_object*);
LEAN_EXPORT lean_object* l_String_extract___boxed(lean_object*, lean_object*, lean_object*);
@ -256,6 +259,7 @@ LEAN_EXPORT lean_object* l_String_posOf___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_instLTString;
LEAN_EXPORT uint8_t l_String_substrEq_loop(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Substring_atEnd(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_firstDiffPos_loop___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_isPrefixOf___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_trim(lean_object*);
LEAN_EXPORT lean_object* l_String_mkIterator(lean_object*);
@ -994,6 +998,72 @@ lean_dec(x_1);
return x_3;
}
}
LEAN_EXPORT lean_object* l_String_firstDiffPos_loop(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
uint8_t x_5;
x_5 = lean_nat_dec_eq(x_4, x_3);
if (x_5 == 0)
{
uint32_t x_6; uint32_t x_7; uint8_t x_8;
x_6 = lean_string_utf8_get(x_1, x_4);
x_7 = lean_string_utf8_get(x_2, x_4);
x_8 = lean_uint32_dec_eq(x_6, x_7);
if (x_8 == 0)
{
return x_4;
}
else
{
lean_object* x_9;
x_9 = lean_string_utf8_next(x_1, x_4);
lean_dec(x_4);
x_4 = x_9;
goto _start;
}
}
else
{
return x_4;
}
}
}
LEAN_EXPORT lean_object* l_String_firstDiffPos_loop___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_String_firstDiffPos_loop(x_1, x_2, x_3, x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_5;
}
}
LEAN_EXPORT lean_object* l_String_firstDiffPos(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_3 = lean_string_utf8_byte_size(x_1);
x_4 = lean_string_utf8_byte_size(x_2);
x_5 = l_Nat_min(x_3, x_4);
lean_dec(x_4);
lean_dec(x_3);
x_6 = lean_unsigned_to_nat(0u);
x_7 = l_String_firstDiffPos_loop(x_1, x_2, x_5, x_6);
lean_dec(x_5);
return x_7;
}
}
LEAN_EXPORT lean_object* l_String_firstDiffPos___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_String_firstDiffPos(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_utf8ExtractAux_u2082(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -1613,7 +1683,7 @@ lean_dec(x_1);
return x_3;
}
}
LEAN_EXPORT uint8_t l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1514_(lean_object* x_1, lean_object* x_2) {
LEAN_EXPORT uint8_t l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1554_(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7;
@ -1636,11 +1706,11 @@ return x_9;
}
}
}
LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1514____boxed(lean_object* x_1, lean_object* x_2) {
LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1554____boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1514_(x_1, x_2);
x_3 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1554_(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
@ -1651,7 +1721,7 @@ LEAN_EXPORT uint8_t l_String_instDecidableEqIterator(lean_object* x_1, lean_obje
_start:
{
uint8_t x_3;
x_3 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1514_(x_1, x_2);
x_3 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1554_(x_1, x_2);
return x_3;
}
}

495
stage0/stdlib/Init/Notation.c generated
View file

@ -542,6 +542,7 @@ static lean_object* l___aux__Init__Notation______macroRules___xabterm___x3e_x3e_
static lean_object* l___aux__Init__Notation______macroRules___xabterm___x2b_x2b___xbb__1___closed__1;
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_contradiction;
static lean_object* l_Lean___aux__Init__Notation______macroRules___xabterm_x5b___x5d_xbb__1___closed__5;
static lean_object* l_termDepIfThenElse___closed__37;
LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__Or__1(lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Tactic_clear___closed__1;
static lean_object* l_termWithout__expected__type_____closed__2;
@ -797,6 +798,7 @@ static lean_object* l_Lean_Parser_Tactic_tacticRfl___closed__5;
static lean_object* l___aux__Init__Notation______macroRules___xabterm___x26_x26_x26___xbb__1___closed__3;
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_tacticAdmit;
static lean_object* l_Lean_Parser_Tactic_location___closed__1;
static lean_object* l_termDepIfThenElse___closed__34;
static lean_object* l_prec_x28___x29___closed__1;
static lean_object* l___aux__Init__Notation______macroRules___xabterm___x3c_x2a_x3e___xbb__1___closed__23;
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticRfl__1(lean_object*, lean_object*, lean_object*);
@ -863,6 +865,7 @@ static lean_object* l_Lean_Parser_Syntax_addPrec___closed__14;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules___xabterm___x3c___xbb__2(lean_object*, lean_object*, lean_object*);
static lean_object* l___aux__Init__Notation______macroRules___xabtermIfLet___x3a_x3d__Then__Else___xbb__1___closed__7;
LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__Not__1(lean_object*, lean_object*);
static lean_object* l_termDepIfThenElse___closed__38;
static lean_object* l_stx_x21_____closed__5;
static lean_object* l_prioHigh___closed__3;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules___xabterm___u2228___xbb__1(lean_object*, lean_object*, lean_object*);
@ -1478,6 +1481,7 @@ static lean_object* l_rawNatLit___closed__3;
static lean_object* l_term_x5b___x5d___closed__6;
static lean_object* l___aux__Init__Notation______macroRules___xabterm_x7e_x7e_x7e___xbb__1___closed__8;
static lean_object* l_Lean___aux__Init__Notation______macroRules__Lean__term__Matches____1___closed__13;
static lean_object* l_termDepIfThenElse___closed__36;
static lean_object* l_Lean_Parser_Tactic_failIfSuccess___closed__4;
static lean_object* l_Lean_Parser_Tactic_simp___closed__1;
static lean_object* l___aux__Init__Notation______macroRules___xabterm___x3e_x3d___xbb__1___closed__3;
@ -1571,6 +1575,7 @@ static lean_object* l_Lean_Parser_Tactic_rwRule___closed__1;
static lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__23;
static lean_object* l_term___x3c_x3d_____closed__7;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules___xabterm___x25___xbb__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_termDepIfThenElse___closed__35;
static lean_object* l_Lean_Parser_Tactic_tacticHave_____x3a_x3d_____closed__2;
static lean_object* l_Lean_Parser_Tactic_split___closed__9;
static lean_object* l_Lean_Parser_Tactic_intro___closed__6;
@ -24187,7 +24192,7 @@ static lean_object* _init_l_termDepIfThenElse___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("ppGroup");
x_1 = lean_mk_string("ppRealGroup");
return x_1;
}
}
@ -24205,7 +24210,7 @@ static lean_object* _init_l_termDepIfThenElse___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("ppDedent");
x_1 = lean_mk_string("ppRealFill");
return x_1;
}
}
@ -24223,21 +24228,39 @@ static lean_object* _init_l_termDepIfThenElse___closed__7() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("if ");
x_1 = lean_mk_string("ppIndent");
return x_1;
}
}
static lean_object* _init_l_termDepIfThenElse___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_termDepIfThenElse___closed__7;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_termDepIfThenElse___closed__9() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("if ");
return x_1;
}
}
static lean_object* _init_l_termDepIfThenElse___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_termDepIfThenElse___closed__7;
x_1 = l_termDepIfThenElse___closed__9;
x_2 = lean_alloc_ctor(5, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_termDepIfThenElse___closed__9() {
static lean_object* _init_l_termDepIfThenElse___closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2;
@ -24247,13 +24270,13 @@ lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_termDepIfThenElse___closed__10() {
static lean_object* _init_l_termDepIfThenElse___closed__12() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_termDepIfThenElse___closed__8;
x_3 = l_termDepIfThenElse___closed__9;
x_2 = l_termDepIfThenElse___closed__10;
x_3 = l_termDepIfThenElse___closed__11;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -24261,7 +24284,7 @@ lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_termDepIfThenElse___closed__11() {
static lean_object* _init_l_termDepIfThenElse___closed__13() {
_start:
{
lean_object* x_1;
@ -24269,40 +24292,14 @@ x_1 = lean_mk_string(" : ");
return x_1;
}
}
static lean_object* _init_l_termDepIfThenElse___closed__12() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_termDepIfThenElse___closed__11;
x_2 = lean_alloc_ctor(5, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_termDepIfThenElse___closed__13() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_termDepIfThenElse___closed__10;
x_3 = l_termDepIfThenElse___closed__12;
x_4 = lean_alloc_ctor(2, 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_termDepIfThenElse___closed__14() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_term___u2218_____closed__6;
x_2 = lean_unsigned_to_nat(0u);
x_3 = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
lean_object* x_1; lean_object* x_2;
x_1 = l_termDepIfThenElse___closed__13;
x_2 = lean_alloc_ctor(5, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_termDepIfThenElse___closed__15() {
@ -24310,7 +24307,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_termDepIfThenElse___closed__13;
x_2 = l_termDepIfThenElse___closed__12;
x_3 = l_termDepIfThenElse___closed__14;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
@ -24322,28 +24319,22 @@ return x_4;
static lean_object* _init_l_termDepIfThenElse___closed__16() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string(" then");
return x_1;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_term___u2218_____closed__6;
x_2 = lean_unsigned_to_nat(0u);
x_3 = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_termDepIfThenElse___closed__17() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_termDepIfThenElse___closed__16;
x_2 = lean_alloc_ctor(5, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_termDepIfThenElse___closed__18() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_termDepIfThenElse___closed__15;
x_3 = l_termDepIfThenElse___closed__17;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -24351,78 +24342,90 @@ lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_termDepIfThenElse___closed__18() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string(" then");
return x_1;
}
}
static lean_object* _init_l_termDepIfThenElse___closed__19() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_termDepIfThenElse___closed__18;
x_2 = lean_alloc_ctor(5, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_termDepIfThenElse___closed__20() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_termDepIfThenElse___closed__17;
x_3 = l_termDepIfThenElse___closed__19;
x_4 = lean_alloc_ctor(2, 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_termDepIfThenElse___closed__21() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_termDepIfThenElse___closed__8;
x_2 = l_termDepIfThenElse___closed__20;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_termDepIfThenElse___closed__22() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("ppSpace");
return x_1;
}
}
static lean_object* _init_l_termDepIfThenElse___closed__20() {
static lean_object* _init_l_termDepIfThenElse___closed__23() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_termDepIfThenElse___closed__19;
x_2 = l_termDepIfThenElse___closed__22;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_termDepIfThenElse___closed__21() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_termDepIfThenElse___closed__20;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_termDepIfThenElse___closed__22() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_termDepIfThenElse___closed__18;
x_3 = l_termDepIfThenElse___closed__21;
x_4 = lean_alloc_ctor(2, 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_termDepIfThenElse___closed__23() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_termDepIfThenElse___closed__22;
x_3 = l_termDepIfThenElse___closed__14;
x_4 = lean_alloc_ctor(2, 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_termDepIfThenElse___closed__24() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("else");
return x_1;
lean_object* x_1; lean_object* x_2;
x_1 = l_termDepIfThenElse___closed__23;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_termDepIfThenElse___closed__25() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_termDepIfThenElse___closed__24;
x_2 = lean_alloc_ctor(5, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_termDepIfThenElse___closed__21;
x_3 = l_termDepIfThenElse___closed__24;
x_4 = lean_alloc_ctor(2, 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_termDepIfThenElse___closed__26() {
@ -24430,8 +24433,8 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_termDepIfThenElse___closed__21;
x_3 = l_termDepIfThenElse___closed__25;
x_2 = l_termDepIfThenElse___closed__25;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -24454,38 +24457,40 @@ return x_3;
static lean_object* _init_l_termDepIfThenElse___closed__28() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_termDepIfThenElse___closed__23;
x_3 = l_termDepIfThenElse___closed__27;
x_4 = lean_alloc_ctor(2, 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;
lean_object* x_1;
x_1 = lean_mk_string("ppDedent");
return x_1;
}
}
static lean_object* _init_l_termDepIfThenElse___closed__29() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_termDepIfThenElse___closed__28;
x_3 = l_termDepIfThenElse___closed__21;
x_4 = lean_alloc_ctor(2, 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;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_termDepIfThenElse___closed__30() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_termDepIfThenElse___closed__29;
x_2 = l_termDepIfThenElse___closed__24;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_termDepIfThenElse___closed__31() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_termDepIfThenElse___closed__29;
x_3 = l_termDepIfThenElse___closed__14;
x_2 = l_termDepIfThenElse___closed__27;
x_3 = l_termDepIfThenElse___closed__30;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -24493,37 +24498,83 @@ lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_termDepIfThenElse___closed__31() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_termDepIfThenElse___closed__6;
x_2 = l_termDepIfThenElse___closed__30;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_termDepIfThenElse___closed__32() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_termDepIfThenElse___closed__4;
x_2 = l_termDepIfThenElse___closed__31;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
lean_object* x_1;
x_1 = lean_mk_string("else ");
return x_1;
}
}
static lean_object* _init_l_termDepIfThenElse___closed__33() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_termDepIfThenElse___closed__32;
x_2 = lean_alloc_ctor(5, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_termDepIfThenElse___closed__34() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_termDepIfThenElse___closed__33;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 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_termDepIfThenElse___closed__35() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_termDepIfThenElse___closed__6;
x_2 = l_termDepIfThenElse___closed__34;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_termDepIfThenElse___closed__36() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_termDepIfThenElse___closed__31;
x_3 = l_termDepIfThenElse___closed__35;
x_4 = lean_alloc_ctor(2, 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_termDepIfThenElse___closed__37() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_termDepIfThenElse___closed__4;
x_2 = l_termDepIfThenElse___closed__36;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_termDepIfThenElse___closed__38() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_termDepIfThenElse___closed__2;
x_2 = lean_unsigned_to_nat(1022u);
x_3 = l_termDepIfThenElse___closed__32;
x_3 = l_termDepIfThenElse___closed__37;
x_4 = lean_alloc_ctor(3, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -24535,7 +24586,7 @@ static lean_object* _init_l_termDepIfThenElse() {
_start:
{
lean_object* x_1;
x_1 = l_termDepIfThenElse___closed__33;
x_1 = l_termDepIfThenElse___closed__38;
return x_1;
}
}
@ -25230,8 +25281,8 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_termDepIfThenElse___closed__8;
x_3 = l_termDepIfThenElse___closed__14;
x_2 = l_termDepIfThenElse___closed__10;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -25245,7 +25296,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_termIfThenElse___closed__3;
x_3 = l_termDepIfThenElse___closed__17;
x_3 = l_termDepIfThenElse___closed__19;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -25256,15 +25307,13 @@ return x_4;
static lean_object* _init_l_termIfThenElse___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_termDepIfThenElse___closed__8;
x_2 = l_termIfThenElse___closed__4;
x_3 = l_termDepIfThenElse___closed__21;
x_4 = lean_alloc_ctor(2, 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;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_termIfThenElse___closed__6() {
@ -25273,7 +25322,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_termIfThenElse___closed__5;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__24;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -25287,7 +25336,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_termIfThenElse___closed__6;
x_3 = l_termDepIfThenElse___closed__27;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -25298,15 +25347,13 @@ return x_4;
static lean_object* _init_l_termIfThenElse___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_termDepIfThenElse___closed__6;
x_2 = l_termIfThenElse___closed__7;
x_3 = l_termDepIfThenElse___closed__21;
x_4 = lean_alloc_ctor(2, 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;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_termIfThenElse___closed__9() {
@ -25315,7 +25362,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_termIfThenElse___closed__8;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__30;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -25326,13 +25373,15 @@ return x_4;
static lean_object* _init_l_termIfThenElse___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_termDepIfThenElse___closed__6;
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_termIfThenElse___closed__9;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
x_3 = l_termDepIfThenElse___closed__35;
x_4 = lean_alloc_ctor(2, 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_termIfThenElse___closed__11() {
@ -25739,7 +25788,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_termDepIfThenElse___closed__8;
x_2 = l_termDepIfThenElse___closed__10;
x_3 = l_termIfLet___x3a_x3d__Then__Else_____closed__4;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
@ -25754,7 +25803,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_termIfLet___x3a_x3d__Then__Else_____closed__5;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -25800,7 +25849,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_termIfLet___x3a_x3d__Then__Else_____closed__9;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -25846,7 +25895,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_termIfLet___x3a_x3d__Then__Else_____closed__13;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -25892,7 +25941,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_termIfLet___x3a_x3d__Then__Else_____closed__17;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -27094,7 +27143,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_term_x7b_____x3a___x2f_x2f___x7d___closed__4;
x_3 = l_termDepIfThenElse___closed__9;
x_3 = l_termDepIfThenElse___closed__11;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -27107,8 +27156,8 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_termDepIfThenElse___closed__12;
x_3 = l_termDepIfThenElse___closed__14;
x_2 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -27180,7 +27229,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_term_x7b_____x3a___x2f_x2f___x7d___closed__11;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -27968,7 +28017,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_termWithout__expected__type_____closed__4;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -28333,7 +28382,7 @@ static lean_object* _init_l_term_x5b___x5d___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5;
x_1 = l_termDepIfThenElse___closed__14;
x_1 = l_termDepIfThenElse___closed__16;
x_2 = l___aux__Init__Notation______macroRules___xabstx___x3c_x7c_x3e___xbb__1___closed__7;
x_3 = l_term_x5b___x5d___closed__6;
x_4 = 0;
@ -28493,7 +28542,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_term_x25_x5b___x7c___x5d___closed__7;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -29813,7 +29862,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l___aux__Init__Notation______macroRules___xabstx___x3c_x7c_x3e___xbb__1___closed__6;
x_2 = l_termDepIfThenElse___closed__9;
x_2 = l_termDepIfThenElse___closed__11;
x_3 = l_Lean_Parser_Tactic_intros___closed__5;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
@ -29928,7 +29977,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_rename___closed__4;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -29974,7 +30023,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_rename___closed__8;
x_3 = l_termDepIfThenElse___closed__9;
x_3 = l_termDepIfThenElse___closed__11;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -30386,7 +30435,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_apply___closed__4;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -30460,7 +30509,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_exact___closed__4;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -30534,7 +30583,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_refine___closed__4;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -30608,7 +30657,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_refine_x27___closed__4;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -34200,7 +34249,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_config___closed__7;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -34542,7 +34591,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_change___closed__4;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -34654,7 +34703,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_changeWith___closed__5;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -34784,7 +34833,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_rwRule___closed__8;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -35405,7 +35454,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_injection___closed__4;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -35873,7 +35922,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_simpLemma___closed__5;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -36471,7 +36520,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_delta___closed__4;
x_3 = l_termDepIfThenElse___closed__9;
x_3 = l_termDepIfThenElse___closed__11;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -36559,7 +36608,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_tacticRefine__lift_____closed__4;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -37313,7 +37362,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_tacticHave_____x3a_x3d_____closed__3;
x_3 = l_termDepIfThenElse___closed__9;
x_3 = l_termDepIfThenElse___closed__11;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -37341,7 +37390,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_tacticHave_____x3a_x3d_____closed__5;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -38258,7 +38307,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_tacticShow_____closed__4;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -38989,7 +39038,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_tacticRefine__lift_x27_____closed__4;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -39679,7 +39728,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_tacticHave_x27_____x3a_x3d_____closed__4;
x_3 = l_termDepIfThenElse___closed__9;
x_3 = l_termDepIfThenElse___closed__11;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -39707,7 +39756,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_tacticHave_x27_____x3a_x3d_____closed__6;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -40273,7 +40322,7 @@ static lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_termDepIfThenElse___closed__6;
x_1 = l_termDepIfThenElse___closed__29;
x_2 = l_Lean_Parser_Tactic_inductionAlt___closed__5;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -40349,7 +40398,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_inductionAlt___closed__12;
x_3 = l_termDepIfThenElse___closed__9;
x_3 = l_termDepIfThenElse___closed__11;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -40707,7 +40756,7 @@ static lean_object* _init_l_Lean_Parser_Tactic_induction___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5;
x_1 = l_termDepIfThenElse___closed__14;
x_1 = l_termDepIfThenElse___closed__16;
x_2 = l___aux__Init__Notation______macroRules___xabstx___x3c_x7c_x3e___xbb__1___closed__7;
x_3 = l_term_x5b___x5d___closed__6;
x_4 = 0;
@ -40757,7 +40806,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_induction___closed__8;
x_3 = l_termDepIfThenElse___closed__9;
x_3 = l_termDepIfThenElse___closed__11;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -40932,8 +40981,8 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_termDepIfThenElse___closed__9;
x_3 = l_termDepIfThenElse___closed__12;
x_2 = l_termDepIfThenElse___closed__11;
x_3 = l_termDepIfThenElse___closed__14;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -40999,7 +41048,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_generalizeArg___closed__7;
x_3 = l_termDepIfThenElse___closed__9;
x_3 = l_termDepIfThenElse___closed__11;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -41143,7 +41192,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_generalizeArg___closed__5;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -41335,7 +41384,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_existsIntro___closed__4;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -41989,7 +42038,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_intro___closed__11;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -42103,7 +42152,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_specialize___closed__4;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -43196,7 +43245,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_term_u2039___u203a___closed__4;
x_3 = l_termDepIfThenElse___closed__14;
x_3 = l_termDepIfThenElse___closed__16;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -45344,6 +45393,16 @@ l_termDepIfThenElse___closed__32 = _init_l_termDepIfThenElse___closed__32();
lean_mark_persistent(l_termDepIfThenElse___closed__32);
l_termDepIfThenElse___closed__33 = _init_l_termDepIfThenElse___closed__33();
lean_mark_persistent(l_termDepIfThenElse___closed__33);
l_termDepIfThenElse___closed__34 = _init_l_termDepIfThenElse___closed__34();
lean_mark_persistent(l_termDepIfThenElse___closed__34);
l_termDepIfThenElse___closed__35 = _init_l_termDepIfThenElse___closed__35();
lean_mark_persistent(l_termDepIfThenElse___closed__35);
l_termDepIfThenElse___closed__36 = _init_l_termDepIfThenElse___closed__36();
lean_mark_persistent(l_termDepIfThenElse___closed__36);
l_termDepIfThenElse___closed__37 = _init_l_termDepIfThenElse___closed__37();
lean_mark_persistent(l_termDepIfThenElse___closed__37);
l_termDepIfThenElse___closed__38 = _init_l_termDepIfThenElse___closed__38();
lean_mark_persistent(l_termDepIfThenElse___closed__38);
l_termDepIfThenElse = _init_l_termDepIfThenElse();
lean_mark_persistent(l_termDepIfThenElse);
l___aux__Init__Notation______macroRules__termDepIfThenElse__1___closed__1 = _init_l___aux__Init__Notation______macroRules__termDepIfThenElse__1___closed__1();

6
stage0/stdlib/Lean.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean
// Imports: Init Lean.Data Lean.Compiler Lean.Environment Lean.Modifiers Lean.ProjFns Lean.Runtime Lean.ResolveName Lean.Attributes Lean.Parser Lean.ReducibilityAttrs Lean.Elab Lean.Class Lean.LocalContext Lean.MetavarContext Lean.AuxRecursor Lean.Meta Lean.Util Lean.Eval Lean.Structure Lean.PrettyPrinter Lean.CoreM Lean.InternalExceptionId Lean.Server Lean.ScopedEnvExtension Lean.DocString Lean.DeclarationRange Lean.LazyInitExtension Lean.Widget
// Imports: Init Lean.Data Lean.Compiler Lean.Environment Lean.Modifiers Lean.ProjFns Lean.Runtime Lean.ResolveName Lean.Attributes Lean.Parser Lean.ReducibilityAttrs Lean.Elab Lean.Class Lean.LocalContext Lean.MetavarContext Lean.AuxRecursor Lean.Meta Lean.Util Lean.Eval Lean.Structure Lean.PrettyPrinter Lean.CoreM Lean.InternalExceptionId Lean.Server Lean.ScopedEnvExtension Lean.DocString Lean.DeclarationRange Lean.LazyInitExtension Lean.LoadDynlib Lean.Widget
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -41,6 +41,7 @@ lean_object* initialize_Lean_ScopedEnvExtension(lean_object*);
lean_object* initialize_Lean_DocString(lean_object*);
lean_object* initialize_Lean_DeclarationRange(lean_object*);
lean_object* initialize_Lean_LazyInitExtension(lean_object*);
lean_object* initialize_Lean_LoadDynlib(lean_object*);
lean_object* initialize_Lean_Widget(lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Lean(lean_object* w) {
@ -131,6 +132,9 @@ lean_dec_ref(res);
res = initialize_Lean_LazyInitExtension(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_LoadDynlib(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Widget(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

181
stage0/stdlib/Lean/Compiler/IR/EmitC.c generated
View file

@ -576,6 +576,7 @@ static lean_object* l_Lean_IR_EmitC_emitInitFn___closed__4;
static lean_object* l_Lean_IR_EmitC_emitMainFn___lambda__2___closed__29;
LEAN_EXPORT uint8_t l_Lean_IR_EmitC_paramEqArg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_IR_EmitC_emitLn___at_Lean_IR_EmitC_emitMainFn___spec__2___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__20;
LEAN_EXPORT lean_object* l_Lean_IR_EmitC_emitCase(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_IR_EmitC_emitSSet___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_IR_EmitC_emitLns___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -2892,21 +2893,29 @@ static lean_object* _init_l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__14()
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("lean_unbox_uint32(lean_io_result_get_value(res));");
x_1 = lean_mk_string("lean_finalize_task_manager();");
return x_1;
}
}
static lean_object* _init_l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__15() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("lean_unbox_uint32(lean_io_result_get_value(res));");
return x_1;
}
}
static lean_object* _init_l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__16() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__10;
x_2 = l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__14;
x_2 = l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__15;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__16() {
static lean_object* _init_l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__17() {
_start:
{
lean_object* x_1;
@ -2914,7 +2923,7 @@ x_1 = lean_mk_string("Init.Data.Option.BasicAux");
return x_1;
}
}
static lean_object* _init_l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__17() {
static lean_object* _init_l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__18() {
_start:
{
lean_object* x_1;
@ -2922,7 +2931,7 @@ x_1 = lean_mk_string("Option.get!");
return x_1;
}
}
static lean_object* _init_l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__18() {
static lean_object* _init_l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__19() {
_start:
{
lean_object* x_1;
@ -2930,15 +2939,15 @@ x_1 = lean_mk_string("value is none");
return x_1;
}
}
static lean_object* _init_l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__19() {
static lean_object* _init_l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__20() {
_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_IR_EmitC_emitMainFn___lambda__1___closed__16;
x_2 = l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__17;
x_1 = l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__17;
x_2 = l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__18;
x_3 = lean_unsigned_to_nat(16u);
x_4 = lean_unsigned_to_nat(14u);
x_5 = l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__18;
x_5 = l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__19;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
}
@ -2980,22 +2989,22 @@ lean_ctor_set(x_23, 0, x_15);
lean_ctor_set(x_23, 1, x_22);
if (lean_obj_tag(x_11) == 0)
{
lean_object* x_64; lean_object* x_65;
x_64 = l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__19;
x_65 = l_panic___at_Lean_IR_EmitC_emitMainFn___spec__4(x_64);
x_24 = x_65;
goto block_63;
lean_object* x_68; lean_object* x_69;
x_68 = l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__20;
x_69 = l_panic___at_Lean_IR_EmitC_emitMainFn___spec__4(x_68);
x_24 = x_69;
goto block_67;
}
else
{
lean_object* x_66;
x_66 = lean_ctor_get(x_11, 0);
lean_inc(x_66);
lean_object* x_70;
x_70 = lean_ctor_get(x_11, 0);
lean_inc(x_70);
lean_dec(x_11);
x_24 = x_66;
goto block_63;
x_24 = x_70;
goto block_67;
}
block_63:
block_67:
{
lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; uint8_t x_30;
x_25 = l_Lean_ConstantInfo_type(x_24);
@ -3011,7 +3020,7 @@ x_30 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_B
lean_dec(x_28);
if (x_30 == 0)
{
lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; uint8_t x_36;
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; uint8_t x_38;
x_31 = l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__12;
x_32 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_32, 0, x_31);
@ -3020,77 +3029,85 @@ x_33 = l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__13;
x_34 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_34, 0, x_33);
lean_ctor_set(x_34, 1, x_32);
x_35 = l_List_forM___at_Lean_IR_EmitC_emitMainFn___spec__3(x_34, x_5, x_10);
lean_dec(x_34);
x_36 = !lean_is_exclusive(x_35);
if (x_36 == 0)
x_35 = l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__14;
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 = l_List_forM___at_Lean_IR_EmitC_emitMainFn___spec__3(x_36, x_5, x_10);
lean_dec(x_36);
x_38 = !lean_is_exclusive(x_37);
if (x_38 == 0)
{
lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41;
x_37 = lean_ctor_get(x_35, 1);
x_38 = lean_ctor_get(x_35, 0);
lean_dec(x_38);
x_39 = lean_string_append(x_37, x_7);
x_40 = lean_string_append(x_39, x_9);
x_41 = lean_box(0);
lean_ctor_set(x_35, 1, x_40);
lean_ctor_set(x_35, 0, x_41);
return x_35;
lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43;
x_39 = lean_ctor_get(x_37, 1);
x_40 = lean_ctor_get(x_37, 0);
lean_dec(x_40);
x_41 = lean_string_append(x_39, x_7);
x_42 = lean_string_append(x_41, x_9);
x_43 = lean_box(0);
lean_ctor_set(x_37, 1, x_42);
lean_ctor_set(x_37, 0, x_43);
return x_37;
}
else
{
lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46;
x_42 = lean_ctor_get(x_35, 1);
lean_inc(x_42);
lean_dec(x_35);
x_43 = lean_string_append(x_42, x_7);
x_44 = lean_string_append(x_43, x_9);
x_45 = lean_box(0);
x_46 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_46, 0, x_45);
lean_ctor_set(x_46, 1, x_44);
return x_46;
}
}
else
{
lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; uint8_t x_52;
x_47 = l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__15;
x_48 = lean_alloc_ctor(1, 2, 0);
lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48;
x_44 = lean_ctor_get(x_37, 1);
lean_inc(x_44);
lean_dec(x_37);
x_45 = lean_string_append(x_44, x_7);
x_46 = lean_string_append(x_45, x_9);
x_47 = lean_box(0);
x_48 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_48, 0, x_47);
lean_ctor_set(x_48, 1, x_23);
x_49 = l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__13;
lean_ctor_set(x_48, 1, x_46);
return x_48;
}
}
else
{
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; uint8_t x_56;
x_49 = l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__16;
x_50 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_50, 0, x_49);
lean_ctor_set(x_50, 1, x_48);
x_51 = l_List_forM___at_Lean_IR_EmitC_emitMainFn___spec__3(x_50, x_5, x_10);
lean_dec(x_50);
x_52 = !lean_is_exclusive(x_51);
if (x_52 == 0)
{
lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57;
x_53 = lean_ctor_get(x_51, 1);
x_54 = lean_ctor_get(x_51, 0);
lean_ctor_set(x_50, 1, x_23);
x_51 = l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__13;
x_52 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_52, 0, x_51);
lean_ctor_set(x_52, 1, x_50);
x_53 = l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__14;
x_54 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_54, 0, x_53);
lean_ctor_set(x_54, 1, x_52);
x_55 = l_List_forM___at_Lean_IR_EmitC_emitMainFn___spec__3(x_54, x_5, x_10);
lean_dec(x_54);
x_55 = lean_string_append(x_53, x_7);
x_56 = lean_string_append(x_55, x_9);
x_57 = lean_box(0);
lean_ctor_set(x_51, 1, x_56);
lean_ctor_set(x_51, 0, x_57);
return x_51;
x_56 = !lean_is_exclusive(x_55);
if (x_56 == 0)
{
lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61;
x_57 = lean_ctor_get(x_55, 1);
x_58 = lean_ctor_get(x_55, 0);
lean_dec(x_58);
x_59 = lean_string_append(x_57, x_7);
x_60 = lean_string_append(x_59, x_9);
x_61 = lean_box(0);
lean_ctor_set(x_55, 1, x_60);
lean_ctor_set(x_55, 0, x_61);
return x_55;
}
else
{
lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62;
x_58 = lean_ctor_get(x_51, 1);
lean_inc(x_58);
lean_dec(x_51);
x_59 = lean_string_append(x_58, x_7);
x_60 = lean_string_append(x_59, x_9);
x_61 = lean_box(0);
x_62 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_62, 0, x_61);
lean_ctor_set(x_62, 1, x_60);
return x_62;
lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66;
x_62 = lean_ctor_get(x_55, 1);
lean_inc(x_62);
lean_dec(x_55);
x_63 = lean_string_append(x_62, x_7);
x_64 = lean_string_append(x_63, x_9);
x_65 = lean_box(0);
x_66 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_66, 0, x_65);
lean_ctor_set(x_66, 1, x_64);
return x_66;
}
}
}
@ -13775,6 +13792,8 @@ l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__18 = _init_l_Lean_IR_EmitC_emit
lean_mark_persistent(l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__18);
l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__19 = _init_l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__19();
lean_mark_persistent(l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__19);
l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__20 = _init_l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__20();
lean_mark_persistent(l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__20);
l_Lean_IR_EmitC_emitMainFn___lambda__2___closed__1 = _init_l_Lean_IR_EmitC_emitMainFn___lambda__2___closed__1();
lean_mark_persistent(l_Lean_IR_EmitC_emitMainFn___lambda__2___closed__1);
l_Lean_IR_EmitC_emitMainFn___lambda__2___closed__2 = _init_l_Lean_IR_EmitC_emitMainFn___lambda__2___closed__2();

1733
stage0/stdlib/Lean/Data/Lsp/Extra.c generated
View file

File diff suppressed because it is too large Load diff

26
stage0/stdlib/Lean/Data/Parsec.c generated
View file

@ -69,7 +69,7 @@ LEAN_EXPORT lean_object* l_Lean_Parsec_instMonadParsec;
LEAN_EXPORT lean_object* l_Lean_Parsec_pstring(lean_object*, lean_object*);
static lean_object* l_Lean_Parsec_instMonadParsec___closed__7;
LEAN_EXPORT lean_object* l_Lean_Parsec_instInhabitedParsec___rarg(lean_object*);
uint8_t l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1514_(lean_object*, lean_object*);
uint8_t l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1554_(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parsec_many1(lean_object*);
lean_object* l_String_Iterator_next(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parsec_peek_x21(lean_object*);
@ -1144,7 +1144,7 @@ if (x_9 == 0)
lean_object* x_10; lean_object* x_11; uint8_t x_12;
x_10 = lean_ctor_get(x_4, 0);
x_11 = lean_ctor_get(x_4, 1);
x_12 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1514_(x_3, x_10);
x_12 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1554_(x_3, x_10);
if (x_12 == 0)
{
lean_dec(x_3);
@ -1170,7 +1170,7 @@ x_16 = lean_ctor_get(x_4, 1);
lean_inc(x_16);
lean_inc(x_15);
lean_dec(x_4);
x_17 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1514_(x_3, x_15);
x_17 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1554_(x_3, x_15);
if (x_17 == 0)
{
lean_object* x_18;
@ -1315,7 +1315,7 @@ if (x_10 == 0)
lean_object* x_11; lean_object* x_12; uint8_t x_13;
x_11 = lean_ctor_get(x_5, 0);
x_12 = lean_ctor_get(x_5, 1);
x_13 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1514_(x_4, x_11);
x_13 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1554_(x_4, x_11);
if (x_13 == 0)
{
lean_dec(x_4);
@ -1341,7 +1341,7 @@ x_17 = lean_ctor_get(x_5, 1);
lean_inc(x_17);
lean_inc(x_16);
lean_dec(x_5);
x_18 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1514_(x_4, x_16);
x_18 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1554_(x_4, x_16);
if (x_18 == 0)
{
lean_object* x_19;
@ -1498,7 +1498,7 @@ if (x_14 == 0)
lean_object* x_15; lean_object* x_16; uint8_t x_17;
x_15 = lean_ctor_get(x_9, 0);
x_16 = lean_ctor_get(x_9, 1);
x_17 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1514_(x_3, x_15);
x_17 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1554_(x_3, x_15);
if (x_17 == 0)
{
lean_dec(x_3);
@ -1523,7 +1523,7 @@ x_19 = lean_ctor_get(x_9, 1);
lean_inc(x_19);
lean_inc(x_18);
lean_dec(x_9);
x_20 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1514_(x_3, x_18);
x_20 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1554_(x_3, x_18);
if (x_20 == 0)
{
lean_object* x_21;
@ -1557,7 +1557,7 @@ if (x_23 == 0)
lean_object* x_24; lean_object* x_25; uint8_t x_26;
x_24 = lean_ctor_get(x_4, 0);
x_25 = lean_ctor_get(x_4, 1);
x_26 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1514_(x_3, x_24);
x_26 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1554_(x_3, x_24);
if (x_26 == 0)
{
lean_dec(x_3);
@ -1582,7 +1582,7 @@ x_28 = lean_ctor_get(x_4, 1);
lean_inc(x_28);
lean_inc(x_27);
lean_dec(x_4);
x_29 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1514_(x_3, x_27);
x_29 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1554_(x_3, x_27);
if (x_29 == 0)
{
lean_object* x_30;
@ -1757,7 +1757,7 @@ if (x_14 == 0)
lean_object* x_15; lean_object* x_16; uint8_t x_17;
x_15 = lean_ctor_get(x_9, 0);
x_16 = lean_ctor_get(x_9, 1);
x_17 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1514_(x_3, x_15);
x_17 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1554_(x_3, x_15);
if (x_17 == 0)
{
lean_dec(x_3);
@ -1782,7 +1782,7 @@ x_19 = lean_ctor_get(x_9, 1);
lean_inc(x_19);
lean_inc(x_18);
lean_dec(x_9);
x_20 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1514_(x_3, x_18);
x_20 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1554_(x_3, x_18);
if (x_20 == 0)
{
lean_object* x_21;
@ -1816,7 +1816,7 @@ if (x_23 == 0)
lean_object* x_24; lean_object* x_25; uint8_t x_26;
x_24 = lean_ctor_get(x_4, 0);
x_25 = lean_ctor_get(x_4, 1);
x_26 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1514_(x_3, x_24);
x_26 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1554_(x_3, x_24);
if (x_26 == 0)
{
lean_dec(x_3);
@ -1841,7 +1841,7 @@ x_28 = lean_ctor_get(x_4, 1);
lean_inc(x_28);
lean_inc(x_27);
lean_dec(x_4);
x_29 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1514_(x_3, x_27);
x_29 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_1554_(x_3, x_27);
if (x_29 == 0)
{
lean_object* x_30;

560
stage0/stdlib/Lean/Data/Xml/Parser.c generated
View file

File diff suppressed because it is too large Load diff

328
stage0/stdlib/Lean/Elab/Match.c generated
View file

@ -226,7 +226,6 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Term_finalizePatternDecls(lean_object*, lea
static lean_object* l_Lean_Elab_Term_isAuxDiscrName___closed__2;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_elabMatch_elabMatchDefault___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews_updateMatchType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__2;
lean_object* l_Lean_mkAppN(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_ToDepElimPattern_throwInvalidPattern___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_ToDepElimPattern_throwInvalidPattern___rarg___closed__1;
@ -234,7 +233,6 @@ static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Match_0__L
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_precheckMatch___spec__3(size_t, size_t, lean_object*);
static lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_isMatchUnit_x3f___closed__7;
LEAN_EXPORT lean_object* l_Lean_mkFreshId___at___private_Lean_Elab_Match_0__Lean_Elab_Term_ToDepElimPattern_mkLocalDeclFor___spec__2___rarg(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__1;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_finalizePatternDecls___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_withPatternVars___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -305,6 +303,7 @@ static lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_expandSimpleMa
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_finalizePatternDecls___spec__1___lambda__2___closed__2;
static lean_object* l_Lean_Elab_Term_isAuxDiscrName___closed__1;
static lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_getMatchGeneralizing_x3f___closed__11;
static lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__2;
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews_collectDeps___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_withMacroExpansion___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_forIn_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews_collectDeps___spec__5(lean_object*, lean_object*, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -325,7 +324,6 @@ lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_addTrace___at___private_Lean_Elab_Match_0__Lean_Elab_Term_findDiscrRefinementPath_goIndex___spec__3___closed__2;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltView(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkLambdaFVars(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2537____closed__2;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_expandNonAtomicDiscrs_x3f_loop___lambda__2(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_EXPORT lean_object* l_Lean_Elab_Term_ToDepElimPattern_main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabPatterns(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -371,6 +369,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatch
static lean_object* l___regBuiltin_Lean_Elab_Term_elabInaccessible_declRange___closed__2;
LEAN_EXPORT lean_object* l_Std_RBNode_revFold___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews_collectDeps___spec__3___boxed(lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_findDiscrRefinementPath_goIndex___closed__6;
static lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2554____closed__2;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews_loop___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Term_elabMVarWithIdKind_declRange___closed__4;
static lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_expandNonAtomicDiscrs_x3f_loop___closed__1;
@ -412,6 +411,7 @@ lean_object* l_Lean_MetavarContext_localDeclDependsOn(lean_object*, lean_object*
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchTypeAndDiscrs_elabDiscrsWitMatchType___spec__1___closed__3;
static lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltView___lambda__2___closed__1;
static lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___lambda__5___closed__2;
static lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2554____closed__1;
static lean_object* l___regBuiltin_Lean_Elab_Term_precheckMatch___closed__2;
static lean_object* l_Lean_Elab_Term_isAtomicDiscr_x3f___closed__2;
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Term_elabInaccessible(lean_object*);
@ -426,6 +426,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_liftMacroM___at___private_Lean_Elab_Match_0
LEAN_EXPORT lean_object* l_Lean_Elab_Term_ToDepElimPattern_State_found___default;
uint8_t l_Lean_Expr_isConst(lean_object*);
uint8_t l_Array_isEmpty___rarg(lean_object*);
static lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__5;
lean_object* l_Lean_LocalDecl_toExpr(lean_object*);
extern lean_object* l_Lean_instInhabitedSyntax;
lean_object* l_Lean_Meta_Match_instantiateAltLHSMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -434,13 +435,14 @@ LEAN_EXPORT lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatch
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews_addWildcardPatterns___spec__1(lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_Meta_isProof(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_Elab_Term_elabMatch_elabMatchDefault___spec__1___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__1;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews_addWildcardPatterns___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_expandNonAtomicDiscrs_x3f_loop___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*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__4;
lean_object* l_Lean_ResolveName_resolveGlobalName(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_ToDepElimPattern_throwInvalidPattern___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabTermEnsuringType___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_whnf(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__5;
LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at_Lean_Elab_Term_elabMatch_elabMatchDefault___spec__1(lean_object*, size_t, size_t);
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabPatterns___spec__7___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkFVar(lean_object*);
@ -455,7 +457,6 @@ static lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_expandSimpleMa
static lean_object* l_List_forIn_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___spec__7___lambda__1___closed__1;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_findDiscrRefinementPath_goIndex___closed__5;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabAtomicDiscr___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Term_elabNoMatch___closed__3;
lean_object* l_Lean_addTrace___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*);
@ -475,7 +476,6 @@ lean_object* l_Lean_LocalDecl_fvarId(lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_tryPostponeIfDiscrTypeIsMVar___spec__1___closed__2;
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchTypeAndDiscrs_elabDiscrsWitMatchType___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_findDiscrRefinementPath_goType___spec__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*);
static lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2537____closed__1;
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_tryPostponeIfDiscrTypeIsMVar___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_findDiscrRefinementPath_goType___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_EXPORT lean_object* l_Array_anyMUnsafe_any___at___private_Lean_Elab_Match_0__Lean_Elab_Term_generalize___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -483,7 +483,6 @@ static lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_getMatchGenera
LEAN_EXPORT lean_object* l_Lean_Meta_withExistingLocalDecls___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___spec__6___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_elabMatch___closed__2;
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_tryPostponeIfDiscrTypeIsMVar___spec__1___closed__1;
static lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__4;
extern lean_object* l_Lean_Elab_Term_termElabAttribute;
static lean_object* l___regBuiltin_Lean_Elab_Term_precheckMatch___closed__1;
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabPatterns___spec__7___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -568,6 +567,7 @@ static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Match_0__L
static lean_object* l___regBuiltin_Lean_Elab_Term_elabMatch___closed__3;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_expandMacrosInPatterns___spec__1(size_t, size_t, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__3;
lean_object* l_Lean_mkApp(lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_expandSimpleMatch___closed__20;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_elabInaccessible___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -592,7 +592,7 @@ static lean_object* l_Lean_addTrace___at___private_Lean_Elab_Match_0__Lean_Elab_
static lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_findDiscrRefinementPath_goIndex___closed__9;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews_collectDeps(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_findDiscrRefinementPath_goType___spec__1___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*);
static lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__3;
lean_object* l_Lean_Elab_Term_addTermInfo(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_liftMacroM___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_List_forIn_loop___at_Lean_Elab_Term_reportMatcherResultErrors___spec__1___closed__4;
lean_object* l_Lean_Elab_Term_elabTerm___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -769,9 +769,9 @@ LEAN_EXPORT lean_object* l_Lean_addTrace___at___private_Lean_Elab_Match_0__Lean_
lean_object* l_Lean_Elab_Term_isLocalIdent_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_liftMacroM___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___spec__1___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_Closure_mkBinding___spec__1(size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_12964_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2537_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_12981_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2554_(lean_object*);
lean_object* l_Lean_mkSimpleThunk(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_isAtomicDiscr_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_elabNoMatch___closed__4;
@ -1488,6 +1488,7 @@ lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_1);
return x_15;
}
else
@ -1499,8 +1500,6 @@ lean_dec(x_12);
if (lean_obj_tag(x_16) == 1)
{
lean_object* x_17; lean_object* x_18; lean_object* x_19;
lean_dec(x_3);
lean_dec(x_2);
x_17 = lean_ctor_get(x_11, 1);
lean_inc(x_17);
lean_dec(x_11);
@ -1510,141 +1509,160 @@ lean_inc(x_4);
x_19 = l_Lean_Meta_getLocalDecl(x_18, x_4, x_5, x_6, x_7, x_17);
if (lean_obj_tag(x_19) == 0)
{
uint8_t x_20;
x_20 = !lean_is_exclusive(x_19);
if (x_20 == 0)
{
lean_object* x_21; lean_object* x_22; lean_object* x_23; uint8_t x_24;
x_21 = lean_ctor_get(x_19, 0);
x_22 = lean_ctor_get(x_19, 1);
x_23 = l_Lean_LocalDecl_userName(x_21);
x_24 = l_Lean_Elab_Term_isAuxDiscrName(x_23);
if (x_24 == 0)
{
lean_dec(x_21);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_ctor_set(x_19, 0, x_16);
return x_19;
}
else
{
lean_object* x_25; lean_object* x_26;
lean_free_object(x_19);
lean_dec(x_16);
x_25 = l_Lean_LocalDecl_value(x_21);
lean_dec(x_21);
x_26 = l_Lean_Meta_instantiateMVars(x_25, x_4, x_5, x_6, x_7, x_22);
return x_26;
}
}
else
{
lean_object* x_27; lean_object* x_28; lean_object* x_29; uint8_t x_30;
x_27 = lean_ctor_get(x_19, 0);
x_28 = lean_ctor_get(x_19, 1);
lean_inc(x_28);
lean_inc(x_27);
lean_object* x_20; lean_object* x_21; lean_object* x_22; uint8_t x_23;
x_20 = lean_ctor_get(x_19, 0);
lean_inc(x_20);
x_21 = lean_ctor_get(x_19, 1);
lean_inc(x_21);
lean_dec(x_19);
x_29 = l_Lean_LocalDecl_userName(x_27);
x_30 = l_Lean_Elab_Term_isAuxDiscrName(x_29);
if (x_30 == 0)
x_22 = l_Lean_LocalDecl_userName(x_20);
x_23 = l_Lean_Elab_Term_isAuxDiscrName(x_22);
if (x_23 == 0)
{
lean_object* x_31;
lean_object* x_24; lean_object* x_25; uint8_t x_26; lean_object* x_27;
lean_dec(x_20);
x_24 = lean_box(0);
x_25 = lean_box(0);
x_26 = 0;
lean_inc(x_16);
x_27 = l_Lean_Elab_Term_addTermInfo(x_1, x_16, x_24, x_24, x_25, x_26, x_2, x_3, x_4, x_5, x_6, x_7, x_21);
if (lean_obj_tag(x_27) == 0)
{
uint8_t x_28;
x_28 = !lean_is_exclusive(x_27);
if (x_28 == 0)
{
lean_object* x_29;
x_29 = lean_ctor_get(x_27, 0);
lean_dec(x_29);
lean_ctor_set(x_27, 0, x_16);
return x_27;
}
else
{
lean_object* x_30; lean_object* x_31;
x_30 = lean_ctor_get(x_27, 1);
lean_inc(x_30);
lean_dec(x_27);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
x_31 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_31, 0, x_16);
lean_ctor_set(x_31, 1, x_28);
lean_ctor_set(x_31, 1, x_30);
return x_31;
}
}
else
{
lean_object* x_32; lean_object* x_33;
uint8_t x_32;
lean_dec(x_16);
x_32 = l_Lean_LocalDecl_value(x_27);
x_32 = !lean_is_exclusive(x_27);
if (x_32 == 0)
{
return x_27;
}
else
{
lean_object* x_33; lean_object* x_34; lean_object* x_35;
x_33 = lean_ctor_get(x_27, 0);
x_34 = lean_ctor_get(x_27, 1);
lean_inc(x_34);
lean_inc(x_33);
lean_dec(x_27);
x_33 = l_Lean_Meta_instantiateMVars(x_32, x_4, x_5, x_6, x_7, x_28);
return x_33;
x_35 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_35, 0, x_33);
lean_ctor_set(x_35, 1, x_34);
return x_35;
}
}
}
else
{
uint8_t x_34;
lean_object* x_36; lean_object* x_37;
lean_dec(x_16);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
x_34 = !lean_is_exclusive(x_19);
if (x_34 == 0)
{
return x_19;
}
else
{
lean_object* x_35; lean_object* x_36; lean_object* x_37;
x_35 = lean_ctor_get(x_19, 0);
x_36 = lean_ctor_get(x_19, 1);
lean_inc(x_36);
lean_inc(x_35);
lean_dec(x_19);
x_37 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_37, 0, x_35);
lean_ctor_set(x_37, 1, x_36);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_36 = l_Lean_LocalDecl_value(x_20);
lean_dec(x_20);
x_37 = l_Lean_Meta_instantiateMVars(x_36, x_4, x_5, x_6, x_7, x_21);
return x_37;
}
}
}
else
{
lean_object* x_38; lean_object* x_39; lean_object* x_40;
uint8_t x_38;
lean_dec(x_16);
x_38 = lean_ctor_get(x_11, 1);
lean_inc(x_38);
lean_dec(x_11);
x_39 = l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabAtomicDiscr___closed__2;
x_40 = l_Lean_throwErrorAt___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabAtomicDiscr___spec__1(x_1, x_39, x_2, x_3, x_4, x_5, x_6, x_7, x_38);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
return x_40;
}
}
}
else
{
uint8_t x_41;
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_41 = !lean_is_exclusive(x_11);
if (x_41 == 0)
lean_dec(x_1);
x_38 = !lean_is_exclusive(x_19);
if (x_38 == 0)
{
return x_19;
}
else
{
lean_object* x_39; lean_object* x_40; lean_object* x_41;
x_39 = lean_ctor_get(x_19, 0);
x_40 = lean_ctor_get(x_19, 1);
lean_inc(x_40);
lean_inc(x_39);
lean_dec(x_19);
x_41 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_41, 0, x_39);
lean_ctor_set(x_41, 1, x_40);
return x_41;
}
}
}
else
{
lean_object* x_42; lean_object* x_43; lean_object* x_44;
lean_dec(x_16);
x_42 = lean_ctor_get(x_11, 1);
lean_inc(x_42);
lean_dec(x_11);
x_43 = l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabAtomicDiscr___closed__2;
x_44 = l_Lean_throwErrorAt___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabAtomicDiscr___spec__1(x_1, x_43, x_2, x_3, x_4, x_5, x_6, x_7, x_42);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_1);
return x_44;
}
}
}
else
{
uint8_t x_45;
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_45 = !lean_is_exclusive(x_11);
if (x_45 == 0)
{
return x_11;
}
else
{
lean_object* x_42; lean_object* x_43; lean_object* x_44;
x_42 = lean_ctor_get(x_11, 0);
x_43 = lean_ctor_get(x_11, 1);
lean_inc(x_43);
lean_inc(x_42);
lean_object* x_46; lean_object* x_47; lean_object* x_48;
x_46 = lean_ctor_get(x_11, 0);
x_47 = lean_ctor_get(x_11, 1);
lean_inc(x_47);
lean_inc(x_46);
lean_dec(x_11);
x_44 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_44, 0, x_42);
lean_ctor_set(x_44, 1, x_43);
return x_44;
x_48 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_48, 0, x_46);
lean_ctor_set(x_48, 1, x_47);
return x_48;
}
}
}
@ -1662,15 +1680,6 @@ lean_dec(x_1);
return x_10;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabAtomicDiscr___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_Match_0__Lean_Elab_Term_elabAtomicDiscr(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
lean_dec(x_1);
return x_9;
}
}
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchTypeAndDiscrs_elabDiscrsWitMatchType___spec__1___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, uint8_t 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:
{
@ -3137,6 +3146,7 @@ lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_18);
x_19 = l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabAtomicDiscr(x_18, x_6, x_7, x_8, x_9, x_10, x_11, x_12);
if (lean_obj_tag(x_19) == 0)
{
@ -4696,7 +4706,7 @@ lean_dec(x_2);
return x_5;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2537____closed__1() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2554____closed__1() {
_start:
{
lean_object* x_1;
@ -4704,21 +4714,21 @@ x_1 = lean_mk_string("MVarWithIdKind");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2537____closed__2() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2554____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2537____closed__1;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2554____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2537_(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2554_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2537____closed__2;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2554____closed__2;
x_3 = l_Lean_Parser_registerBuiltinNodeKind(x_2, x_1);
return x_3;
}
@ -4803,7 +4813,7 @@ _start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_2 = l_Lean_Elab_Term_termElabAttribute;
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2537____closed__2;
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2554____closed__2;
x_4 = l___regBuiltin_Lean_Elab_Term_elabMVarWithIdKind___closed__4;
x_5 = l___regBuiltin_Lean_Elab_Term_elabMVarWithIdKind___closed__5;
x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1);
@ -25046,7 +25056,7 @@ lean_dec(x_2);
return x_9;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__1() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -25056,7 +25066,7 @@ x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__2() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__2() {
_start:
{
lean_object* x_1;
@ -25064,17 +25074,17 @@ x_1 = lean_mk_string("ignoreUnusedAlts");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__3() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__1;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__2;
x_1 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__1;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__2;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__4() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__4() {
_start:
{
lean_object* x_1;
@ -25082,13 +25092,13 @@ x_1 = lean_mk_string("if true, do not generate error if an alternative is not us
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__5() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__5() {
_start:
{
uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = 0;
x_2 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchTypeAndDiscrs_elabDiscrsWitMatchType___spec__1___closed__15;
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__4;
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__4;
x_4 = lean_box(x_1);
x_5 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_5, 0, x_4);
@ -25097,12 +25107,12 @@ lean_ctor_set(x_5, 2, x_3);
return x_5;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732_(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__3;
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__5;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__3;
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__5;
x_4 = l_Lean_Option_register___at_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_6____spec__1(x_2, x_3, x_1);
return x_4;
}
@ -25748,7 +25758,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___private_Lean_Elab_Match_0__Lean_Elab_Term_isMatchUnit_x3f___closed__4;
x_2 = l___private_Lean_Elab_Match_0__Lean_Elab_Term_isMatchUnit_x3f___closed__5;
x_3 = lean_unsigned_to_nat(756u);
x_3 = lean_unsigned_to_nat(757u);
x_4 = lean_unsigned_to_nat(2u);
x_5 = l___private_Lean_Elab_Match_0__Lean_Elab_Term_isMatchUnit_x3f___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -28322,7 +28332,7 @@ if (lean_obj_tag(x_28) == 0)
lean_object* x_30; lean_object* x_31; lean_object* x_32;
lean_dec(x_21);
x_30 = lean_array_get_size(x_22);
x_31 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__1;
x_31 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__1;
lean_inc(x_12);
lean_inc(x_11);
lean_inc(x_10);
@ -31788,7 +31798,7 @@ x_4 = l_Lean_addBuiltinDeclarationRanges(x_2, x_3, x_1);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_12964_(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_12981_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -32384,11 +32394,11 @@ l___private_Lean_Elab_Match_0__Lean_Elab_Term_getMatchGeneralizing_x3f___closed_
lean_mark_persistent(l___private_Lean_Elab_Match_0__Lean_Elab_Term_getMatchGeneralizing_x3f___closed__13);
l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Match_0__Lean_Elab_Term_getMatchAlts___spec__2___closed__1 = _init_l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Match_0__Lean_Elab_Term_getMatchAlts___spec__2___closed__1();
lean_mark_persistent(l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Match_0__Lean_Elab_Term_getMatchAlts___spec__2___closed__1);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2537____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2537____closed__1();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2537____closed__1);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2537____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2537____closed__2();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2537____closed__2);
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2537_(lean_io_mk_world());
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2554____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2554____closed__1();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2554____closed__1);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2554____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2554____closed__2();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2554____closed__2);
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_2554_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___regBuiltin_Lean_Elab_Term_elabMVarWithIdKind___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_elabMVarWithIdKind___closed__1();
@ -32597,19 +32607,19 @@ l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews_loop___closed__2
lean_mark_persistent(l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews_loop___closed__2);
l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews_loop___boxed__const__1 = _init_l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews_loop___boxed__const__1();
lean_mark_persistent(l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAltViews_loop___boxed__const__1);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__1();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__1);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__2();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__2);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__3 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__3();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__3);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__4 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__4();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__4);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__5 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__5();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732____closed__5);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__1();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__1);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__2();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__2);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__3 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__3();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__3);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__4 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__4();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__4);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__5 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__5();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749____closed__5);
l_Lean_Elab_Term_match_ignoreUnusedAlts___closed__1 = _init_l_Lean_Elab_Term_match_ignoreUnusedAlts___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_match_ignoreUnusedAlts___closed__1);
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9732_(lean_io_mk_world());
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9749_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
l_Lean_Elab_Term_match_ignoreUnusedAlts = lean_io_result_get_value(res);
lean_mark_persistent(l_Lean_Elab_Term_match_ignoreUnusedAlts);
@ -32727,7 +32737,7 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabMatch_declRange___closed_
res = l___regBuiltin_Lean_Elab_Term_elabMatch_declRange(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_Match___hyg_12964_(lean_io_mk_world());
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_12981_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_Term_elabNoMatch___closed__1 = _init_l_Lean_Elab_Term_elabNoMatch___closed__1();

36
stage0/stdlib/Lean/Elab/Term.c generated
View file

@ -134,7 +134,6 @@ LEAN_EXPORT lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_withoutMod
static lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___closed__2;
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_logUnassignedUsingErrorInfos___spec__5(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_termElabAttribute___closed__12;
static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15198____closed__2;
static lean_object* l_Lean_Elab_Term_throwErrorIfErrors___closed__1;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_commitIfNoErrors_x3f___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_getConstInfo___at_Lean_Elab_Term_mkConst___spec__1___closed__1;
@ -154,6 +153,7 @@ uint8_t l_Lean_Elab_isValidAutoBoundImplicitName(lean_object*);
static lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___lambda__3___closed__5;
lean_object* l_Std_HashMapImp_find_x3f___at_Lean_Meta_ToHide_visitVisibleExpr_visit___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_resolveLocalName_loop___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15195____closed__2;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFnsAux___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_commitIfDidNotPostpone___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_autoBoundImplicitLocal;
@ -335,11 +335,11 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Term_instMonadMacroAdapterTermElabM___lambd
uint8_t lean_usize_dec_lt(size_t, size_t);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_instInhabitedMVarErrorInfo;
LEAN_EXPORT lean_object* l_List_mapTRAux___at_Lean_Elab_Term_resolveId_x3f___spec__3(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15195____closed__1;
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Term_throwTypeMismatchError___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFns(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_addAutoBoundImplicits___spec__1___closed__2;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_mkCoe___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*);
static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15198____closed__1;
lean_object* l_Lean_Meta_mkAppOptM(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_mkExplicitBinder___closed__8;
static lean_object* l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___lambda__2___closed__1;
@ -668,8 +668,8 @@ LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Term_synthesizeInstMVa
static lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___lambda__3___closed__1;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_getMainModule(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_replace___at___private_Lean_Elab_Term_0__Lean_Elab_Term_throwStuckAtUniverseCnstr___spec__9(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15195____closed__3;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_mkTermElabAttribute(lean_object*);
static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15198____closed__3;
LEAN_EXPORT lean_object* l_Lean_Elab_withInfoContext_x27___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFnsAux___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_pure___at_Lean_Elab_liftMacroM___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_printTraces___at_Lean_Core_instMetaEvalCoreM___spec__1(lean_object*, lean_object*, lean_object*);
@ -1128,7 +1128,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Term_applyResult___rarg(lean_object*, lean_
lean_object* l_IO_println___at_Lean_instEval___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ReaderT_pure___at_Lean_Elab_Term_addTermInfo___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_throwErrorIfErrors(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15198_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15195_(lean_object*);
static lean_object* l_Lean_Elab_Term_termElabAttribute___closed__10;
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Term_evalExpr___spec__13(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_addAutoBoundImplicits(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -52722,7 +52722,7 @@ x_3 = lean_alloc_closure((void*)(l_Lean_Elab_withoutModifyingStateWithInfoAndMes
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15198____closed__1() {
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15195____closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -52732,7 +52732,7 @@ x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15198____closed__2() {
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15195____closed__2() {
_start:
{
lean_object* x_1;
@ -52740,17 +52740,17 @@ x_1 = lean_mk_string("debug");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15198____closed__3() {
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15195____closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Term_MVarErrorInfo_logError___closed__11;
x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15198____closed__2;
x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15195____closed__2;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15198_(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15195_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -52762,7 +52762,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
lean_dec(x_3);
x_5 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15198____closed__1;
x_5 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15195____closed__1;
x_6 = l_Lean_registerTraceClass(x_5, x_4);
if (lean_obj_tag(x_6) == 0)
{
@ -52770,7 +52770,7 @@ lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_ctor_get(x_6, 1);
lean_inc(x_7);
lean_dec(x_6);
x_8 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15198____closed__3;
x_8 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15195____closed__3;
x_9 = l_Lean_registerTraceClass(x_8, x_7);
return x_9;
}
@ -53752,13 +53752,13 @@ l___private_Lean_Elab_Term_0__Lean_Elab_Term_throwStuckAtUniverseCnstr___closed_
lean_mark_persistent(l___private_Lean_Elab_Term_0__Lean_Elab_Term_throwStuckAtUniverseCnstr___closed__1);
l___private_Lean_Elab_Term_0__Lean_Elab_Term_throwStuckAtUniverseCnstr___closed__2 = _init_l___private_Lean_Elab_Term_0__Lean_Elab_Term_throwStuckAtUniverseCnstr___closed__2();
lean_mark_persistent(l___private_Lean_Elab_Term_0__Lean_Elab_Term_throwStuckAtUniverseCnstr___closed__2);
l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15198____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15198____closed__1();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15198____closed__1);
l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15198____closed__2 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15198____closed__2();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15198____closed__2);
l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15198____closed__3 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15198____closed__3();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15198____closed__3);
res = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15198_(lean_io_mk_world());
l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15195____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15195____closed__1();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15195____closed__1);
l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15195____closed__2 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15195____closed__2();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15195____closed__2);
l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15195____closed__3 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15195____closed__3();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15195____closed__3);
res = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_15195_(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));

40
stage0/stdlib/Lean/LoadDynlib.c generated Normal file
View file

@ -0,0 +1,40 @@
// Lean compiler output
// Module: Lean.LoadDynlib
// Imports: Init
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
#ifdef __cplusplus
extern "C" {
#endif
lean_object* lean_load_dynlib(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_loadDynlib___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_loadDynlib___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_load_dynlib(x_1, x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* initialize_Init(lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Lean_LoadDynlib(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init(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));
}
#ifdef __cplusplus
}
#endif

818
stage0/stdlib/Lean/Parser/Basic.c generated
View file

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

458
stage0/stdlib/Lean/Parser/Term.c generated
View file

File diff suppressed because it is too large Load diff

1967
stage0/stdlib/Lean/Server/FileWorker.c generated
View file

File diff suppressed because it is too large Load diff

1843
stage0/stdlib/Lean/Server/FileWorker/RequestHandling.c generated
View file

File diff suppressed because it is too large Load diff

4
stage0/stdlib/Lean/Server/FileWorker/Utils.c generated
View file

@ -24,7 +24,7 @@ uint8_t lean_usize_dec_eq(size_t, size_t);
LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_instMonadRpcSession___rarg(lean_object*, lean_object*);
static lean_object* l_Lean_Server_FileWorker_logSnapContent___closed__2;
LEAN_EXPORT lean_object* l_Lean_Server_FileWorker_instMonadRpcSession___rarg___lambda__6___boxed(lean_object*, lean_object*);
uint64_t l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_hashRpcRef____x40_Lean_Data_Lsp_Extra___hyg_820_(size_t);
uint64_t l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_hashRpcRef____x40_Lean_Data_Lsp_Extra___hyg_954_(size_t);
size_t lean_usize_sub(size_t, size_t);
static lean_object* l_Lean_Server_FileWorker_logSnapContent___closed__1;
static lean_object* l_Lean_Server_FileWorker_instInhabitedEditableDocument___closed__13;
@ -953,7 +953,7 @@ lean_object* x_3; uint64_t x_4; size_t x_5; uint8_t x_6;
x_3 = lean_ctor_get(x_1, 0);
lean_inc(x_3);
lean_dec(x_1);
x_4 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_hashRpcRef____x40_Lean_Data_Lsp_Extra___hyg_820_(x_2);
x_4 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_hashRpcRef____x40_Lean_Data_Lsp_Extra___hyg_954_(x_2);
x_5 = lean_uint64_to_usize(x_4);
x_6 = l_Std_PersistentHashMap_containsAux___at_Lean_Server_FileWorker_RpcSession_release___spec__2(x_3, x_5, x_2);
return x_6;

32
stage0/stdlib/Lean/Server/FileWorker/WidgetRequests.c generated
View file

@ -46,6 +46,7 @@ static lean_object* l___private_Lean_Widget_InteractiveDiagnostic_0__Lean_Widget
LEAN_EXPORT lean_object* l___private_Lean_Widget_InteractiveDiagnostic_0__Lean_Widget_Lean_MessageData_decodeUnsafe____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_246____spec__4___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_MsgToInteractive_instRpcEncodingMsgToInteractiveRpcEncodingPacket___lambda__5(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_8950____spec__35(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1143____spec__1___lambda__2(lean_object*, uint64_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Info_type_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__11___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -56,6 +57,7 @@ LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPop
static lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___closed__3;
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_MsgToInteractive_instFromJsonRpcEncodingPacket;
LEAN_EXPORT lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_246____spec__1___lambda__6(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_liftExcept___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_8950____spec__36___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_Lean_Widget_InfoPopup_toJsonRpcEncodingPacket____x40_Lean_Server_FileWorker_WidgetRequests___hyg_433____closed__5;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__2___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_Lean_Widget_MsgToInteractive_fromJsonRpcEncodingPacket____x40_Lean_Server_FileWorker_WidgetRequests___hyg_57_(lean_object*);
@ -95,7 +97,6 @@ lean_object* l_Lean_FileMap_lspPosToUtf8Pos(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_MsgToInteractive_instRpcEncodingMsgToInteractiveRpcEncodingPacket___spec__2(lean_object*);
lean_object* l_Std_RBNode_find___at_Lean_Server_registerRpcCallHandler___spec__1(lean_object*, uint64_t);
LEAN_EXPORT lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_246____spec__14(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_8924____spec__35(lean_object*);
lean_object* l_IO_AsyncList_waitAll___at_Lean_Server_FileWorker_handleReferences___spec__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_613____spec__1___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__9(lean_object*);
@ -118,7 +119,6 @@ LEAN_EXPORT lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_i
LEAN_EXPORT lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_toJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_948_(lean_object*);
static lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_246____spec__1___lambda__4___closed__1;
LEAN_EXPORT lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_fromJsonGetInteractiveDiagnosticsParams____x40_Lean_Server_FileWorker_WidgetRequests___hyg_913____boxed(lean_object*);
lean_object* l_liftExcept___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_8924____spec__36___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_854____spec__1___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instFromJsonRpcEncodingPacket;
LEAN_EXPORT lean_object* l_Lean_Server_parseRequestParams___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_1143____spec__2(lean_object*);
@ -145,9 +145,10 @@ LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Widget_getInteracti
lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_Diagnostics_0__Lean_Lsp_toJsonDiagnosticWith____x40_Lean_Data_Lsp_Diagnostics___hyg_883____spec__5(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___lambda__8(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonLineRange____x40_Lean_Data_Lsp_Extra___hyg_1666_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonLineRange____x40_Lean_Data_Lsp_Extra___hyg_1800_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_854____spec__1___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_854____spec__3___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_liftExcept___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_8950____spec__33___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_MsgToInteractive_instRpcEncodingMsgToInteractiveRpcEncodingPacket;
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___lambda__9(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_parseRequestParams___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_613____spec__2(lean_object*);
@ -220,7 +221,7 @@ LEAN_EXPORT lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_Widg
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__20(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_getInteractiveDiagnostics___lambda__1___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_MsgToInteractive_instRpcEncodingMsgToInteractiveRpcEncodingPacket___lambda__5___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_883_(size_t);
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_1017_(size_t);
LEAN_EXPORT lean_object* l___private_Lean_Widget_InteractiveDiagnostic_0__Lean_Widget_Lean_MessageData_decodeUnsafe____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_246____spec__4(size_t, lean_object*);
static lean_object* l___private_Lean_Widget_TaggedText_0__Lean_Widget_toJsonTaggedText____x40_Lean_Widget_TaggedText___hyg_578____at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_246____spec__16___closed__1;
LEAN_EXPORT lean_object* l_Lean_Server_WithRpcRef_encodeUnsafe___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_246____spec__13(lean_object*, lean_object*, lean_object*);
@ -251,6 +252,7 @@ extern lean_object* l_Task_Priority_default;
static lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___lambda__10___closed__1;
LEAN_EXPORT lean_object* l_Lean_Widget_getInteractiveDiagnostics(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_854____closed__4;
lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_8950____spec__32(lean_object*);
size_t lean_usize_of_nat(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Widget_TaggedText_0__Lean_Widget_toJsonTaggedText____x40_Lean_Widget_TaggedText___hyg_578____at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_246____spec__16(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_323____spec__1(lean_object*, lean_object*);
@ -300,7 +302,6 @@ LEAN_EXPORT lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_Lean_Wid
LEAN_EXPORT lean_object* l_Lean_Widget_getInteractiveDiagnostics___lambda__3___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_613____spec__1___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__5(lean_object*);
lean_object* l_liftExcept___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_8924____spec__33___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_613____spec__1___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___lambda__3___closed__1;
LEAN_EXPORT lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_854____spec__1___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -331,8 +332,7 @@ static lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__7(lean_object*);
lean_object* l_Lean_Json_mkObj(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_MsgToInteractive_instToJsonRpcEncodingPacket;
lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_8924____spec__32(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_848_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_982_(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Widget_InteractiveCode_0__Lean_Widget_Lean_Widget_InfoWithCtx_decodeUnsafe____x40_Lean_Widget_InteractiveCode___hyg_5____at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_613____spec__4___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__17(lean_object*);
static lean_object* l___private_Lean_Widget_InteractiveDiagnostic_0__Lean_Widget_Lean_MessageData_decodeUnsafe____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_246____spec__4___closed__3;
@ -414,7 +414,7 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_Inf
static lean_object* l___private_Lean_Widget_InteractiveDiagnostic_0__Lean_Widget_Lean_MessageData_decodeUnsafe____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_246____spec__4___closed__4;
static lean_object* l_Lean_Server_WithRpcRef_decodeUnsafeAs___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_246____spec__5___rarg___closed__6;
static lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_246____spec__1___lambda__1___closed__1;
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonLineRange____x40_Lean_Data_Lsp_Extra___hyg_1614_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonLineRange____x40_Lean_Data_Lsp_Extra___hyg_1748_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_WithRpcRef_decodeUnsafeAs___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_246____spec__5(lean_object*);
static lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___closed__1;
LEAN_EXPORT lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_613____spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -594,7 +594,7 @@ x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_4 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_883_(x_3);
x_4 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_1017_(x_3);
x_5 = l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_Lean_Widget_MsgToInteractive_fromJsonRpcEncodingPacket____x40_Lean_Server_FileWorker_WidgetRequests___hyg_57____closed__1;
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_5);
@ -6046,7 +6046,7 @@ _start:
{
lean_object* x_2;
lean_inc(x_1);
x_2 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_848_(x_1);
x_2 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_982_(x_1);
if (lean_obj_tag(x_2) == 0)
{
uint8_t x_3;
@ -8157,8 +8157,8 @@ lean_inc(x_12);
x_13 = lean_ctor_get(x_11, 1);
lean_inc(x_13);
lean_dec(x_11);
x_14 = l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_8924____spec__32(x_3);
x_15 = lean_alloc_closure((void*)(l_liftExcept___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_8924____spec__33___boxed), 3, 1);
x_14 = l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_8950____spec__32(x_3);
x_15 = lean_alloc_closure((void*)(l_liftExcept___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_8950____spec__33___boxed), 3, 1);
lean_closure_set(x_15, 0, x_14);
x_16 = l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_854____spec__1___lambda__3___closed__1;
x_17 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Server_FileWorker_handleDocumentSymbol___spec__2___rarg), 4, 2);
@ -8525,8 +8525,8 @@ lean_inc(x_12);
x_13 = lean_ctor_get(x_11, 1);
lean_inc(x_13);
lean_dec(x_11);
x_14 = l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_8924____spec__35(x_3);
x_15 = lean_alloc_closure((void*)(l_liftExcept___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_8924____spec__36___boxed), 3, 1);
x_14 = l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_8950____spec__35(x_3);
x_15 = lean_alloc_closure((void*)(l_liftExcept___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_8950____spec__36___boxed), 3, 1);
lean_closure_set(x_15, 0, x_14);
x_16 = l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_854____spec__1___lambda__3___closed__1;
x_17 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Server_FileWorker_handleDocumentSymbol___spec__2___rarg), 4, 2);
@ -8932,7 +8932,7 @@ return x_4;
else
{
lean_object* x_5;
x_5 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonLineRange____x40_Lean_Data_Lsp_Extra___hyg_1614_(x_3);
x_5 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonLineRange____x40_Lean_Data_Lsp_Extra___hyg_1748_(x_3);
lean_dec(x_3);
if (lean_obj_tag(x_5) == 0)
{
@ -9087,7 +9087,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_obj
x_4 = lean_ctor_get(x_2, 0);
lean_inc(x_4);
lean_dec(x_2);
x_5 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonLineRange____x40_Lean_Data_Lsp_Extra___hyg_1666_(x_4);
x_5 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonLineRange____x40_Lean_Data_Lsp_Extra___hyg_1800_(x_4);
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_1);
lean_ctor_set(x_6, 1, x_5);

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

@ -120,7 +120,7 @@ LEAN_EXPORT lean_object* l_Lean_Server_registerRpcCallHandler___lambda__5___boxe
LEAN_EXPORT lean_object* l_Lean_Server_registerLspRequestHandler___at_Lean_Server_initFn____x40_Lean_Server_Rpc_RequestHandling___hyg_153____spec__1___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_usize_to_nat(size_t);
static lean_object* l_Lean_Server_registerRpcCallHandler___lambda__1___closed__5;
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonRpcCallParams____x40_Lean_Data_Lsp_Extra___hyg_1108_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonRpcCallParams____x40_Lean_Data_Lsp_Extra___hyg_1242_(lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_containsAtAux___at_Lean_Server_registerRpcCallHandler___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_parseRequestParams___rarg(lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
@ -334,7 +334,7 @@ _start:
{
lean_object* x_2;
lean_inc(x_1);
x_2 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonRpcCallParams____x40_Lean_Data_Lsp_Extra___hyg_1108_(x_1);
x_2 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonRpcCallParams____x40_Lean_Data_Lsp_Extra___hyg_1242_(x_1);
if (lean_obj_tag(x_2) == 0)
{
uint8_t x_3;

359
stage0/stdlib/Lean/Server/Utils.c generated
View file

@ -13,7 +13,6 @@
#ifdef __cplusplus
extern "C" {
#endif
static lean_object* l_panic___at_Lean_Server_foldDocumentChanges___spec__2___closed__1;
LEAN_EXPORT lean_object* l_IO_FS_Stream_chainLeft___elambda__3___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
size_t lean_usize_add(size_t, size_t);
LEAN_EXPORT uint8_t l_Lean_Server_toFileUri___lambda__1(uint32_t);
@ -24,7 +23,7 @@ LEAN_EXPORT lean_object* l_IO_FS_Stream_chainRight___elambda__6(lean_object*, le
LEAN_EXPORT lean_object* l_IO_FS_Stream_writeLspNotification___at_Lean_Server_publishDiagnostics___spec__1(lean_object*, lean_object*, lean_object*);
uint8_t lean_usize_dec_eq(size_t, size_t);
lean_object* lean_array_uget(lean_object*, size_t);
LEAN_EXPORT lean_object* l_Lean_Server_publishProgressAtPos___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_publishProgressAtPos___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_publishProgress(lean_object*, lean_object*, lean_object*, lean_object*);
extern uint8_t l_System_FilePath_isCaseInsensitive;
LEAN_EXPORT lean_object* l_String_Range_toLspRange___boxed(lean_object*, lean_object*);
@ -35,11 +34,10 @@ static lean_object* l_Lean_Server_toFileUri___closed__1;
LEAN_EXPORT lean_object* l_IO_FS_Stream_chainRight___lambda__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_publishProgressDone(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_FS_Stream_chainLeft___elambda__6(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Server_foldDocumentChanges___spec__1(lean_object*, lean_object*, size_t, size_t, lean_object*);
extern lean_object* l_instInhabitedNat;
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Server_foldDocumentChanges___spec__1(lean_object*, size_t, size_t, lean_object*);
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_publishProgressAtPos(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_publishProgressAtPos(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
LEAN_EXPORT lean_object* l_IO_FS_Stream_withPrefix___elambda__5(lean_object*, lean_object*);
lean_object* lean_string_append(lean_object*, lean_object*);
lean_object* lean_string_utf8_set(lean_object*, lean_object*, uint32_t);
@ -49,7 +47,6 @@ LEAN_EXPORT lean_object* l_IO_throwServerError___rarg(lean_object*, lean_object*
lean_object* l_String_dropWhile(lean_object*, lean_object*);
lean_object* lean_string_utf8_byte_size(lean_object*);
static lean_object* l_Lean_Server_publishDiagnostics___closed__1;
static lean_object* l_Lean_Server_foldDocumentChanges___closed__3;
lean_object* l_Lean_FileMap_utf8PosToLspPos(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_FS_Stream_chainLeft___elambda__5(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_instInhabitedDocumentMeta;
@ -65,6 +62,7 @@ LEAN_EXPORT lean_object* l_String_Range_toLspRange(lean_object*, lean_object*);
static lean_object* l_Lean_Server_toFileUri___closed__2;
LEAN_EXPORT lean_object* l_IO_FS_Stream_chainRight___lambda__2(lean_object*, uint8_t, lean_object*, lean_object*);
static lean_object* l_Lean_Server_publishProgressAtPos___closed__1;
LEAN_EXPORT lean_object* l_Lean_Server_applyDocumentChange___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_FS_Stream_chainLeft(lean_object*, lean_object*, uint8_t);
LEAN_EXPORT lean_object* l_IO_FS_Stream_chainRight___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_FS_Stream_chainLeft___elambda__2(lean_object*, lean_object*);
@ -75,13 +73,10 @@ LEAN_EXPORT lean_object* l_IO_FS_Stream_chainRight___lambda__1___boxed(lean_obje
LEAN_EXPORT lean_object* l_Lean_Json_toStructured_x3f___at_Lean_Server_publishDiagnostics___spec__2(lean_object*);
lean_object* lean_stream_of_handle(lean_object*);
lean_object* l_IO_FS_Handle_mk(lean_object*, uint8_t, uint8_t, lean_object*);
LEAN_EXPORT lean_object* l_panic___at_Lean_Server_foldDocumentChanges___spec__2(lean_object*);
static lean_object* l_Lean_Json_toStructured_x3f___at_Lean_Server_publishDiagnostics___spec__2___closed__1;
uint32_t lean_string_utf8_get(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_FS_Stream_chainLeft___elambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Server_publishProgress___closed__1;
lean_object* l___private_Init_Util_0__mkPanicMessageWithDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Array_isEmpty___rarg(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Diagnostics_0__Lean_Lsp_toJsonPublishDiagnosticsParams____x40_Lean_Data_Lsp_Diagnostics___hyg_1263_(lean_object*);
lean_object* l_Lean_FileMap_ofString(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Json_toStructured_x3f___at_Lean_Server_publishProgress___spec__2(lean_object*);
@ -107,21 +102,18 @@ LEAN_EXPORT lean_object* l_IO_FS_Stream_chainLeft___elambda__3___lambda__1___box
LEAN_EXPORT lean_object* l_Lean_Server_toFileUri___lambda__1___boxed(lean_object*);
static lean_object* l_Lean_Server_instInhabitedDocumentMeta___closed__3;
LEAN_EXPORT lean_object* l_IO_FS_Stream_chainRight(lean_object*, lean_object*, uint8_t);
lean_object* lean_panic_fn(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonLeanFileProgressParams____x40_Lean_Data_Lsp_Extra___hyg_287_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonLeanFileProgressParams____x40_Lean_Data_Lsp_Extra___hyg_421_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_toFileUri(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_foldDocumentChanges(lean_object*, lean_object*);
static lean_object* l_Lean_Server_foldDocumentChanges___closed__1;
LEAN_EXPORT lean_object* l_Lean_Server_foldDocumentChanges___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_FS_Stream_withPrefix___elambda__6(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_FS_Stream_withPrefix(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_FS_Stream_chainRight___elambda__4___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_FS_Stream_chainRight___elambda__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Server_foldDocumentChanges___closed__2;
static lean_object* l_Lean_Server_foldDocumentChanges___closed__4;
LEAN_EXPORT lean_object* l_Lean_Server_maybeTee(lean_object*, uint8_t, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_FS_Stream_withPrefix___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_min(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_FS_Stream_chainLeft___elambda__4(lean_object*, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_applyDocumentChange(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_FS_Stream_chainRight___elambda__5(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_FS_Stream_withPrefix___elambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_FS_Stream_chainRight___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -130,8 +122,7 @@ uint8_t lean_string_utf8_at_end(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_FS_Stream_chainLeft___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_to_int(lean_object*);
LEAN_EXPORT lean_object* l_IO_FS_Stream_chainRight___elambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_instInhabitedFileMap;
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Server_foldDocumentChanges___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Server_foldDocumentChanges___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_String_mapAux___at_Lean_Server_toFileUri___spec__1(lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_throwServerError___rarg(lean_object* x_1, lean_object* x_2) {
@ -1587,248 +1578,117 @@ x_4 = lean_box(x_3);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Server_foldDocumentChanges___spec__1(lean_object* x_1, lean_object* x_2, size_t x_3, size_t x_4, lean_object* x_5) {
LEAN_EXPORT lean_object* l_Lean_Server_applyDocumentChange(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_6;
x_6 = lean_usize_dec_eq(x_3, x_4);
if (x_6 == 0)
{
lean_object* x_7; size_t x_8; size_t x_9;
x_7 = lean_array_uget(x_2, x_3);
x_8 = 1;
x_9 = lean_usize_add(x_3, x_8);
if (lean_obj_tag(x_7) == 0)
{
uint8_t x_10;
x_10 = !lean_is_exclusive(x_5);
if (x_10 == 0)
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18;
x_11 = lean_ctor_get(x_5, 0);
x_12 = lean_ctor_get(x_5, 1);
x_13 = lean_ctor_get(x_7, 0);
lean_inc(x_13);
x_14 = lean_ctor_get(x_7, 1);
lean_inc(x_14);
lean_dec(x_7);
x_15 = lean_ctor_get(x_13, 0);
lean_inc(x_15);
x_16 = l_Lean_FileMap_lspPosToUtf8Pos(x_1, x_15);
x_17 = l_Lean_Server_replaceLspRange(x_11, x_13, x_14);
lean_dec(x_14);
lean_dec(x_11);
x_18 = l_Nat_min(x_12, x_16);
lean_dec(x_16);
lean_dec(x_12);
lean_ctor_set(x_5, 1, x_18);
lean_ctor_set(x_5, 0, x_17);
x_3 = x_9;
goto _start;
}
else
{
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;
x_20 = lean_ctor_get(x_5, 0);
x_21 = lean_ctor_get(x_5, 1);
lean_inc(x_21);
lean_inc(x_20);
lean_dec(x_5);
x_22 = lean_ctor_get(x_7, 0);
lean_inc(x_22);
x_23 = lean_ctor_get(x_7, 1);
lean_inc(x_23);
lean_dec(x_7);
x_24 = lean_ctor_get(x_22, 0);
lean_inc(x_24);
x_25 = l_Lean_FileMap_lspPosToUtf8Pos(x_1, x_24);
x_26 = l_Lean_Server_replaceLspRange(x_20, x_22, x_23);
lean_dec(x_23);
lean_dec(x_20);
x_27 = l_Nat_min(x_21, x_25);
lean_dec(x_25);
lean_dec(x_21);
x_28 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_28, 0, x_26);
lean_ctor_set(x_28, 1, x_27);
x_3 = x_9;
x_5 = x_28;
goto _start;
}
}
else
{
uint8_t x_30;
x_30 = !lean_is_exclusive(x_5);
if (x_30 == 0)
{
lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35;
x_31 = lean_ctor_get(x_5, 1);
lean_dec(x_31);
x_32 = lean_ctor_get(x_5, 0);
lean_dec(x_32);
x_33 = lean_ctor_get(x_7, 0);
lean_inc(x_33);
lean_dec(x_7);
x_34 = l_Lean_FileMap_ofString(x_33);
x_35 = lean_unsigned_to_nat(0u);
lean_ctor_set(x_5, 1, x_35);
lean_ctor_set(x_5, 0, x_34);
x_3 = x_9;
goto _start;
}
else
{
lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40;
lean_dec(x_5);
x_37 = lean_ctor_get(x_7, 0);
lean_inc(x_37);
lean_dec(x_7);
x_38 = l_Lean_FileMap_ofString(x_37);
x_39 = lean_unsigned_to_nat(0u);
x_40 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_40, 0, x_38);
lean_ctor_set(x_40, 1, x_39);
x_3 = x_9;
x_5 = x_40;
goto _start;
}
}
}
else
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
x_4 = lean_ctor_get(x_2, 1);
lean_inc(x_4);
lean_dec(x_2);
x_5 = l_Lean_Server_replaceLspRange(x_1, x_3, x_4);
lean_dec(x_4);
return x_5;
}
else
{
lean_object* x_6; lean_object* x_7;
x_6 = lean_ctor_get(x_2, 0);
lean_inc(x_6);
lean_dec(x_2);
x_7 = l_Lean_FileMap_ofString(x_6);
return x_7;
}
}
static lean_object* _init_l_panic___at_Lean_Server_foldDocumentChanges___spec__2___closed__1() {
}
LEAN_EXPORT lean_object* l_Lean_Server_applyDocumentChange___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_instInhabitedFileMap;
x_2 = l_instInhabitedNat;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
lean_object* x_3;
x_3 = l_Lean_Server_applyDocumentChange(x_1, x_2);
lean_dec(x_1);
return x_3;
}
}
LEAN_EXPORT lean_object* l_panic___at_Lean_Server_foldDocumentChanges___spec__2(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Server_foldDocumentChanges___spec__1(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_panic___at_Lean_Server_foldDocumentChanges___spec__2___closed__1;
x_3 = lean_panic_fn(x_2, x_1);
return x_3;
}
}
static lean_object* _init_l_Lean_Server_foldDocumentChanges___closed__1() {
_start:
uint8_t x_5;
x_5 = lean_usize_dec_eq(x_2, x_3);
if (x_5 == 0)
{
lean_object* x_1;
x_1 = lean_mk_string("Lean.Server.Utils");
return x_1;
lean_object* x_6; lean_object* x_7; size_t x_8; size_t x_9;
x_6 = lean_array_uget(x_1, x_2);
x_7 = l_Lean_Server_applyDocumentChange(x_4, x_6);
lean_dec(x_4);
x_8 = 1;
x_9 = lean_usize_add(x_2, x_8);
x_2 = x_9;
x_4 = x_7;
goto _start;
}
}
static lean_object* _init_l_Lean_Server_foldDocumentChanges___closed__2() {
_start:
else
{
lean_object* x_1;
x_1 = lean_mk_string("Lean.Server.foldDocumentChanges");
return x_1;
return x_4;
}
}
static lean_object* _init_l_Lean_Server_foldDocumentChanges___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Lean.Server.foldDocumentChanges: empty change array");
return x_1;
}
}
static lean_object* _init_l_Lean_Server_foldDocumentChanges___closed__4() {
_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_Server_foldDocumentChanges___closed__1;
x_2 = l_Lean_Server_foldDocumentChanges___closed__2;
x_3 = lean_unsigned_to_nat(112u);
x_4 = lean_unsigned_to_nat(26u);
x_5 = l_Lean_Server_foldDocumentChanges___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Lean_Server_foldDocumentChanges(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3;
x_3 = l_Array_isEmpty___rarg(x_1);
if (x_3 == 0)
lean_object* x_3; lean_object* x_4; uint8_t x_5;
x_3 = lean_array_get_size(x_1);
x_4 = lean_unsigned_to_nat(0u);
x_5 = lean_nat_dec_lt(x_4, x_3);
if (x_5 == 0)
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8;
x_4 = lean_unsigned_to_nat(4294967295u);
lean_inc(x_2);
x_5 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_5, 0, x_2);
lean_ctor_set(x_5, 1, x_4);
x_6 = lean_array_get_size(x_1);
x_7 = lean_unsigned_to_nat(0u);
x_8 = lean_nat_dec_lt(x_7, x_6);
if (x_8 == 0)
{
lean_dec(x_6);
lean_dec(x_2);
lean_dec(x_1);
return x_5;
lean_dec(x_3);
return x_2;
}
else
{
uint8_t x_9;
x_9 = lean_nat_dec_le(x_6, x_6);
if (x_9 == 0)
uint8_t x_6;
x_6 = lean_nat_dec_le(x_3, x_3);
if (x_6 == 0)
{
lean_dec(x_6);
lean_dec(x_2);
lean_dec(x_1);
return x_5;
lean_dec(x_3);
return x_2;
}
else
{
size_t x_10; size_t x_11; lean_object* x_12;
x_10 = 0;
x_11 = lean_usize_of_nat(x_6);
lean_dec(x_6);
x_12 = l_Array_foldlMUnsafe_fold___at_Lean_Server_foldDocumentChanges___spec__1(x_2, x_1, x_10, x_11, x_5);
lean_dec(x_1);
lean_dec(x_2);
return x_12;
size_t x_7; size_t x_8; lean_object* x_9;
x_7 = 0;
x_8 = lean_usize_of_nat(x_3);
lean_dec(x_3);
x_9 = l_Array_foldlMUnsafe_fold___at_Lean_Server_foldDocumentChanges___spec__1(x_1, x_7, x_8, x_2);
return x_9;
}
}
}
else
{
lean_object* x_13; lean_object* x_14;
lean_dec(x_2);
lean_dec(x_1);
x_13 = l_Lean_Server_foldDocumentChanges___closed__4;
x_14 = l_panic___at_Lean_Server_foldDocumentChanges___spec__2(x_13);
return x_14;
}
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Server_foldDocumentChanges___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Server_foldDocumentChanges___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
size_t x_6; size_t x_7; lean_object* x_8;
size_t x_5; size_t x_6; lean_object* x_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 = lean_unbox_usize(x_4);
lean_dec(x_4);
x_8 = l_Array_foldlMUnsafe_fold___at_Lean_Server_foldDocumentChanges___spec__1(x_1, x_2, x_6, x_7, x_5);
lean_dec(x_2);
x_7 = l_Array_foldlMUnsafe_fold___at_Lean_Server_foldDocumentChanges___spec__1(x_1, x_5, x_6, x_4);
lean_dec(x_1);
return x_8;
return x_7;
}
}
LEAN_EXPORT lean_object* l_Lean_Server_foldDocumentChanges___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_Server_foldDocumentChanges(x_1, x_2);
lean_dec(x_1);
return x_3;
}
}
static lean_object* _init_l_Lean_Json_toStructured_x3f___at_Lean_Server_publishDiagnostics___spec__2___closed__1() {
@ -1921,7 +1781,7 @@ LEAN_EXPORT lean_object* l_Lean_Json_toStructured_x3f___at_Lean_Server_publishPr
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonLeanFileProgressParams____x40_Lean_Data_Lsp_Extra___hyg_287_(x_1);
x_2 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonLeanFileProgressParams____x40_Lean_Data_Lsp_Extra___hyg_421_(x_1);
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
lean_dec(x_2);
@ -1997,36 +1857,41 @@ x_2 = lean_mk_empty_array_with_capacity(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Lean_Server_publishProgressAtPos(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
LEAN_EXPORT lean_object* l_Lean_Server_publishProgressAtPos(lean_object* x_1, lean_object* x_2, lean_object* x_3, uint8_t x_4, lean_object* x_5) {
_start:
{
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;
x_5 = lean_ctor_get(x_1, 2);
lean_inc(x_5);
x_6 = l_Lean_FileMap_utf8PosToLspPos(x_5, x_2);
x_7 = lean_ctor_get(x_5, 0);
lean_inc(x_7);
x_8 = lean_string_utf8_byte_size(x_7);
lean_dec(x_7);
x_9 = l_Lean_FileMap_utf8PosToLspPos(x_5, x_8);
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;
x_6 = lean_ctor_get(x_1, 2);
lean_inc(x_6);
x_7 = l_Lean_FileMap_utf8PosToLspPos(x_6, x_2);
x_8 = lean_ctor_get(x_6, 0);
lean_inc(x_8);
x_9 = lean_string_utf8_byte_size(x_8);
lean_dec(x_8);
lean_dec(x_5);
x_10 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_10, 0, x_6);
lean_ctor_set(x_10, 1, x_9);
x_11 = l_Lean_Server_publishProgressAtPos___closed__1;
x_12 = lean_array_push(x_11, x_10);
x_13 = l_Lean_Server_publishProgress(x_1, x_12, x_3, x_4);
return x_13;
x_10 = l_Lean_FileMap_utf8PosToLspPos(x_6, x_9);
lean_dec(x_9);
lean_dec(x_6);
x_11 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_11, 0, x_7);
lean_ctor_set(x_11, 1, x_10);
x_12 = lean_alloc_ctor(0, 1, 1);
lean_ctor_set(x_12, 0, x_11);
lean_ctor_set_uint8(x_12, sizeof(void*)*1, x_4);
x_13 = l_Lean_Server_publishProgressAtPos___closed__1;
x_14 = lean_array_push(x_13, x_12);
x_15 = l_Lean_Server_publishProgress(x_1, x_14, x_3, x_5);
return x_15;
}
}
LEAN_EXPORT lean_object* l_Lean_Server_publishProgressAtPos___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
LEAN_EXPORT lean_object* l_Lean_Server_publishProgressAtPos___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_5;
x_5 = l_Lean_Server_publishProgressAtPos(x_1, x_2, x_3, x_4);
uint8_t x_6; lean_object* x_7;
x_6 = lean_unbox(x_4);
lean_dec(x_4);
x_7 = l_Lean_Server_publishProgressAtPos(x_1, x_2, x_3, x_6, x_5);
lean_dec(x_2);
return x_5;
return x_7;
}
}
LEAN_EXPORT lean_object* l_Lean_Server_publishProgressDone(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
@ -2103,16 +1968,6 @@ l_Lean_Server_toFileUri___closed__1 = _init_l_Lean_Server_toFileUri___closed__1(
lean_mark_persistent(l_Lean_Server_toFileUri___closed__1);
l_Lean_Server_toFileUri___closed__2 = _init_l_Lean_Server_toFileUri___closed__2();
lean_mark_persistent(l_Lean_Server_toFileUri___closed__2);
l_panic___at_Lean_Server_foldDocumentChanges___spec__2___closed__1 = _init_l_panic___at_Lean_Server_foldDocumentChanges___spec__2___closed__1();
lean_mark_persistent(l_panic___at_Lean_Server_foldDocumentChanges___spec__2___closed__1);
l_Lean_Server_foldDocumentChanges___closed__1 = _init_l_Lean_Server_foldDocumentChanges___closed__1();
lean_mark_persistent(l_Lean_Server_foldDocumentChanges___closed__1);
l_Lean_Server_foldDocumentChanges___closed__2 = _init_l_Lean_Server_foldDocumentChanges___closed__2();
lean_mark_persistent(l_Lean_Server_foldDocumentChanges___closed__2);
l_Lean_Server_foldDocumentChanges___closed__3 = _init_l_Lean_Server_foldDocumentChanges___closed__3();
lean_mark_persistent(l_Lean_Server_foldDocumentChanges___closed__3);
l_Lean_Server_foldDocumentChanges___closed__4 = _init_l_Lean_Server_foldDocumentChanges___closed__4();
lean_mark_persistent(l_Lean_Server_foldDocumentChanges___closed__4);
l_Lean_Json_toStructured_x3f___at_Lean_Server_publishDiagnostics___spec__2___closed__1 = _init_l_Lean_Json_toStructured_x3f___at_Lean_Server_publishDiagnostics___spec__2___closed__1();
lean_mark_persistent(l_Lean_Json_toStructured_x3f___at_Lean_Server_publishDiagnostics___spec__2___closed__1);
l_Lean_Json_toStructured_x3f___at_Lean_Server_publishDiagnostics___spec__2___closed__2 = _init_l_Lean_Json_toStructured_x3f___at_Lean_Server_publishDiagnostics___spec__2___closed__2();

1109
stage0/stdlib/Lean/Server/Watchdog.c generated
View file

File diff suppressed because it is too large Load diff

8
stage0/stdlib/Lean/Widget/InteractiveCode.c generated
View file

@ -79,7 +79,7 @@ LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_CodeToken_instRpcEncodingCode
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_InfoWithCtx_instRpcEncodingWithRpcRefInfoWithCtxRpcRef___lambda__2(lean_object*, lean_object*, lean_object*, size_t);
LEAN_EXPORT lean_object* l_Lean_Widget_exprToInteractiveExplicit(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Widget_formatExplicitInfos___closed__5;
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_883_(size_t);
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_1017_(size_t);
LEAN_EXPORT lean_object* l_Lean_Widget_exprToInteractive(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static uint32_t l_Lean_Widget_instInhabitedInfoWithCtx___closed__7;
LEAN_EXPORT lean_object* l_Lean_Widget_CodeWithInfos_pretty(lean_object*);
@ -111,7 +111,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Widget_InteractiveCode_0__Lean_Widget_
LEAN_EXPORT lean_object* l_Std_RBMap_ofList___at_Lean_Widget_formatExplicitInfos___spec__1(lean_object*);
static lean_object* l_Lean_Widget_formatExplicitInfos___closed__3;
lean_object* l_Lean_Json_mkObj(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_848_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_982_(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Widget_InteractiveCode_0__Lean_Widget_Lean_Widget_InfoWithCtx_encodeUnsafe____x40_Lean_Widget_InteractiveCode___hyg_5_(lean_object*);
static lean_object* l___private_Lean_Widget_InteractiveCode_0__Lean_Widget_Lean_Widget_InfoWithCtx_decode____x40_Lean_Widget_InteractiveCode___hyg_5____rarg___closed__2;
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_CodeToken_instRpcEncodingCodeTokenRpcEncodingPacket___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -666,7 +666,7 @@ _start:
{
lean_object* x_3; lean_object* x_4;
x_3 = l_Lean_Json_getObjValD(x_1, x_2);
x_4 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_848_(x_3);
x_4 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_982_(x_3);
return x_4;
}
}
@ -763,7 +763,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Widget_InteractiveCode_0__Lean_Widget_
_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;
x_2 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_883_(x_1);
x_2 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_1017_(x_1);
x_3 = l___private_Lean_Widget_InteractiveCode_0__Lean_Widget_Lean_Widget_CodeToken_fromJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveCode___hyg_181____closed__1;
x_4 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_4, 0, x_3);

14
stage0/stdlib/Lean/Widget/InteractiveDiagnostic.c generated
View file

@ -336,7 +336,7 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_MsgEmbed_instRp
LEAN_EXPORT lean_object* l_Lean_Widget_MsgEmbed_instRpcEncodingMsgEmbedRpcEncodingPacket___lambda__10___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_dbg_to_string(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_MessageData_instRpcEncodingWithRpcRefMessageDataRpcRef___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_883_(size_t);
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_1017_(size_t);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_InteractiveDiagnostic_instRpcEncodingInteractiveDiagnosticRpcEncodingPacket___spec__3___rarg___lambda__1(size_t, lean_object*, lean_object*, size_t, lean_object*);
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_MsgEmbed_instRpcEncodingMsgEmbedRpcEncodingPacket___spec__17(lean_object*);
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_InteractiveDiagnostic_instRpcEncodingInteractiveDiagnosticRpcEncodingPacket___spec__47(lean_object*);
@ -476,7 +476,7 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_InteractiveDiag
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_InteractiveDiagnostic_instRpcEncodingInteractiveDiagnosticRpcEncodingPacket___spec__2___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_MsgEmbed_instRpcEncodingMsgEmbedRpcEncodingPacket___spec__7___rarg(lean_object*, lean_object*, size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_MsgEmbed_instRpcEncodingMsgEmbedRpcEncodingPacket___spec__19(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_848_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_982_(lean_object*);
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_InteractiveDiagnostic_instRpcEncodingInteractiveDiagnosticRpcEncodingPacket___spec__30(lean_object*);
static lean_object* l___private_Lean_Widget_TaggedText_0__Lean_Widget_fromJsonTaggedText____x40_Lean_Widget_TaggedText___hyg_400____at___private_Lean_Widget_InteractiveDiagnostic_0__Lean_Widget_MsgEmbed_fromJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveDiagnostic___hyg_257____spec__1___lambda__3___closed__1;
LEAN_EXPORT lean_object* l_Lean_Widget_MsgEmbed_instInhabitedRpcEncodingPacket;
@ -1702,7 +1702,7 @@ lean_dec(x_43);
x_53 = lean_unsigned_to_nat(2u);
x_54 = lean_array_get(x_15, x_14, x_53);
lean_dec(x_14);
x_55 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_848_(x_54);
x_55 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_982_(x_54);
if (lean_obj_tag(x_55) == 0)
{
uint8_t x_56;
@ -1774,7 +1774,7 @@ lean_dec(x_28);
x_73 = lean_unsigned_to_nat(2u);
x_74 = lean_array_get(x_15, x_14, x_73);
lean_dec(x_14);
x_75 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_848_(x_74);
x_75 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_982_(x_74);
if (lean_obj_tag(x_75) == 0)
{
uint8_t x_76;
@ -1881,7 +1881,7 @@ lean_dec(x_100);
x_111 = lean_unsigned_to_nat(2u);
x_112 = lean_array_get(x_15, x_14, x_111);
lean_dec(x_14);
x_113 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_848_(x_112);
x_113 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_982_(x_112);
if (lean_obj_tag(x_113) == 0)
{
lean_object* x_114; lean_object* x_115; lean_object* x_116; lean_object* x_117; lean_object* x_118;
@ -1942,7 +1942,7 @@ lean_dec(x_28);
x_125 = lean_unsigned_to_nat(2u);
x_126 = lean_array_get(x_15, x_14, x_125);
lean_dec(x_14);
x_127 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_848_(x_126);
x_127 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_982_(x_126);
if (lean_obj_tag(x_127) == 0)
{
lean_object* x_128; lean_object* x_129; lean_object* x_130; lean_object* x_131; lean_object* x_132;
@ -2472,7 +2472,7 @@ x_23 = lean_alloc_ctor(3, 1, 0);
lean_ctor_set(x_23, 0, x_22);
x_24 = lean_unbox_usize(x_18);
lean_dec(x_18);
x_25 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_883_(x_24);
x_25 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_1017_(x_24);
x_26 = l___private_Lean_Widget_InteractiveDiagnostic_0__Lean_Widget_MsgEmbed_toJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveDiagnostic___hyg_431____closed__1;
x_27 = lean_array_push(x_26, x_20);
x_28 = lean_array_push(x_27, x_23);

8
stage0/stdlib/Lean/Widget/InteractiveGoal.c generated
View file

@ -289,6 +289,7 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_Int
LEAN_EXPORT lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_Lean_Widget_InteractiveGoal_instRpcEncodingInteractiveGoalRpcEncodingPacket___spec__12___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InteractiveGoals_instRpcEncodingInteractiveGoalsRpcEncodingPacket___spec__14___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonPlainGoal____x40_Lean_Data_Lsp_Extra___hyg_584____spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_Lean_Widget_InteractiveGoal_instRpcEncodingInteractiveGoalRpcEncodingPacket___spec__4___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Widget_goalToInteractive___spec__6(uint8_t, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InteractiveHypothesis_instRpcEncodingInteractiveHypothesisRpcEncodingPacket___spec__10___rarg___lambda__1(size_t, lean_object*, lean_object*, lean_object*, size_t, lean_object*);
@ -336,7 +337,6 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_Int
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_InteractiveHypothesis_instRpcEncodingInteractiveHypothesisRpcEncodingPacket___lambda__17(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_Lean_Widget_InteractiveHypothesis_instRpcEncodingInteractiveHypothesisRpcEncodingPacket___lambda__12(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InteractiveTermGoal_instRpcEncodingInteractiveTermGoalRpcEncodingPacket___spec__13___rarg(lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonPlainGoal____x40_Lean_Data_Lsp_Extra___hyg_502____spec__1(size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_InteractiveTermGoal_toInteractiveGoal(lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InteractiveGoal_instRpcEncodingInteractiveGoalRpcEncodingPacket___spec__13___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InteractiveHypothesis_instRpcEncodingInteractiveHypothesisRpcEncodingPacket___spec__12___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -647,7 +647,6 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_Int
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InteractiveGoals_instRpcEncodingInteractiveGoalsRpcEncodingPacket___spec__30___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_instantiateMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InteractiveHypothesis_instRpcEncodingInteractiveHypothesisRpcEncodingPacket___spec__5___rarg___lambda__1(size_t, lean_object*, lean_object*, lean_object*, size_t, lean_object*);
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonPlainGoal____x40_Lean_Data_Lsp_Extra___hyg_450____spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InteractiveGoal_instRpcEncodingInteractiveGoalRpcEncodingPacket___spec__9___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Widget_InteractiveGoal_pretty___closed__1;
LEAN_EXPORT lean_object* l_Lean_Widget_goalToInteractive_ppVars___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -722,6 +721,7 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_Int
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InteractiveTermGoal_instRpcEncodingInteractiveTermGoalRpcEncodingPacket___spec__29___rarg(lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l_Std_instInhabitedPersistentArrayNode(lean_object*);
LEAN_EXPORT lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlMAux___at_Lean_Widget_goalToInteractive___spec__12(uint8_t, 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___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonPlainGoal____x40_Lean_Data_Lsp_Extra___hyg_636____spec__1(size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Widget_TaggedText_0__Lean_Widget_fromJsonTaggedText____x40_Lean_Widget_TaggedText___hyg_400____at___private_Lean_Widget_InteractiveGoal_0__Lean_Widget_Lean_Widget_InteractiveHypothesis_fromJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveGoal___hyg_114____spec__2___lambda__3___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Widget_InteractiveGoal_0__Lean_Widget_Lean_Widget_InteractiveHypothesis_fromJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveGoal___hyg_114____spec__3(size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_Lean_Widget_InteractiveGoals_instRpcEncodingInteractiveGoalsRpcEncodingPacket___spec__7___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, size_t);
@ -1566,7 +1566,7 @@ _start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l___private_Lean_Widget_InteractiveGoal_0__Lean_Widget_Lean_Widget_InteractiveHypothesis_fromJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveGoal___hyg_114____closed__1;
x_3 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonPlainGoal____x40_Lean_Data_Lsp_Extra___hyg_450____spec__1(x_1, x_2);
x_3 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonPlainGoal____x40_Lean_Data_Lsp_Extra___hyg_584____spec__1(x_1, x_2);
if (lean_obj_tag(x_3) == 0)
{
uint8_t x_4;
@ -2001,7 +2001,7 @@ x_4 = lean_usize_of_nat(x_3);
lean_dec(x_3);
x_5 = 0;
x_6 = x_2;
x_7 = l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonPlainGoal____x40_Lean_Data_Lsp_Extra___hyg_502____spec__1(x_4, x_5, x_6);
x_7 = l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonPlainGoal____x40_Lean_Data_Lsp_Extra___hyg_636____spec__1(x_4, x_5, x_6);
x_8 = x_7;
x_9 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_9, 0, x_8);