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:
Leonardo de Moura 2020-02-13 18:27:58 -08:00
parent 0cf226220c
commit c30c14ec84
32 changed files with 21254 additions and 14825 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
stage0/src/Init/Lean/Elab/App.lean
View file

@ -98,10 +98,6 @@ structure ElabAppArgsCtx :=
(typeMVars : Array MVarId := #[]) -- metavariables for implicit arguments of the form `{α : Sort u}` that have already been processed
(foundExplicit : Bool := false) -- true if an explicit argument has already been processed
private def isAutoOrOptParam (type : Expr) : Bool :=
-- TODO: add auto param
type.getOptParamDefault?.isSome
/- Auxiliary function for retrieving the resulting type of a function application.
See `propagateExpectedType`. -/
private partial def getForallBody : Nat → Array NamedArg → Expr → Option Expr
@ -113,7 +109,7 @@ private partial def getForallBody : Nat → Array NamedArg → Expr → Option E
getForallBody i namedArgs b
else if i > 0 then
getForallBody (i-1) namedArgs b
else if isAutoOrOptParam d then
else if d.isAutoParam || d.isOptParam then
getForallBody i namedArgs b
else
some type
@ -227,10 +223,25 @@ private partial def elabAppArgsAux : ElabAppArgsCtx → Expr → Expr → TermEl
if h : ctx.argIdx < ctx.args.size then do
argElab ← elabArg ctx.ref e (ctx.args.get ⟨ctx.argIdx, h⟩) d;
elabAppArgsAux { argIdx := ctx.argIdx + 1, .. ctx } (mkApp e argElab) (b.instantiate1 argElab)
else match ctx.explicit, d.getOptParamDefault? with
| false, some defVal => elabAppArgsAux ctx (mkApp e defVal) (b.instantiate1 defVal)
| _, _ =>
-- TODO: tactic auto param
else match ctx.explicit, d.getOptParamDefault?, d.getAutoParamTactic? with
| false, some defVal, _ => elabAppArgsAux ctx (mkApp e defVal) (b.instantiate1 defVal)
| false, _, some (Expr.const tacticDecl _ _) => do
env ← getEnv;
match evalSyntaxConstant env tacticDecl with
| Except.error err => throwError ctx.ref err
| Except.ok tacticSyntax => do
tacticBlock ← `(begin $(tacticSyntax.getArgs)* end);
-- tacticBlock does not have any position information
-- use ctx.ref.getHeadInfo if available
let tacticBlock := match ctx.ref.getHeadInfo with
| some info => tacticBlock.replaceInfo info
| _ => tacticBlock;
let d := d.getArg! 0; -- `autoParam type := by tactic` ==> `type`
argElab ← elabArg ctx.ref e (Arg.stx tacticBlock) d;
elabAppArgsAux ctx (mkApp e argElab) (b.instantiate1 argElab)
| false, _, some _ =>
throwError ctx.ref "invalid autoParam, argument must be a constant"
| _, _, _ =>
if ctx.namedArgs.isEmpty then
finalize ()
else

52
stage0/src/Init/Lean/Elab/Binders.lean
View file

@ -5,6 +5,7 @@ Authors: Leonardo de Moura
-/
prelude
import Init.Lean.Elab.Term
import Init.Lean.Elab.Quotation
namespace Lean
namespace Elab
@ -37,11 +38,40 @@ else
structure BinderView :=
(id : Syntax) (type : Syntax) (bi : BinderInfo)
partial def quoteAutoTactic : Syntax → TermElabM Syntax
| stx@(Syntax.ident _ _ _ _) => throwError stx "invalic auto tactic, identifier is not allowed"
| stx@(Syntax.node k args) =>
if Quotation.isAntiquot stx then
throwError stx "invalic auto tactic, antiquotation is not allowed"
else do
empty ← `(Array.empty);
args ← args.foldlM (fun args arg =>
if k == nullKind && Quotation.isAntiquotSplice arg then
throwError arg "invalic auto tactic, antiquotation is not allowed"
else do
arg ← quoteAutoTactic arg;
`(Array.push $args $arg)) empty;
`(Syntax.node $(quote k) $args)
| Syntax.atom info val => `(Syntax.atom none $(quote val))
| Syntax.missing => unreachable!
def declareTacticSyntax (tactic : Syntax) : TermElabM Name :=
withFreshMacroScope $ do
name ← MonadQuotation.addMacroScope `_auto;
let type := Lean.mkConst `Lean.Syntax;
tactic ← quoteAutoTactic tactic;
val ← elabTerm tactic type;
val ← instantiateMVars tactic val;
trace `Elab.autoParam tactic $ fun _ => val;
let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false };
addDecl tactic decl;
compileDecl tactic decl;
pure name
/-
Expand `optional (binderDefault <|> binderTactic)`
Expand `optional (binderTactic <|> binderDefault)`
def binderTactic := parser! " := " >> " by " >> tacticParser
def binderDefault := parser! " := " >> termParser
def binderTactic := parser! " . " >> termParser
-/
private def expandBinderModifier (type : Syntax) (optBinderModifier : Syntax) : TermElabM Syntax :=
if optBinderModifier.isNone then pure type
@ -52,7 +82,9 @@ else
let defaultVal := modifier.getArg 1;
`(optParam $type $defaultVal)
else if kind == `Lean.Parser.Term.binderTactic then do
throwError modifier "not implemented yet"
let tac := modifier.getArg 2;
name ← declareTacticSyntax tac;
`(autoParam $type $(mkTermIdFrom tac name))
else
throwUnsupportedSyntax
@ -249,6 +281,13 @@ structure State :=
(expectedType? : Option Expr := none)
(explicit : Bool := false)
private def checkNoOptAutoParam (ref : Syntax) (type : Expr) : TermElabM Unit := do
type ← instantiateMVars ref type;
when type.isOptParam $
throwError ref "optParam is not allowed at 'fun/λ' binders";
when type.isAutoParam $
throwError ref "autoParam is not allowed at 'fun/λ' binders"
private def propagateExpectedType (ref : Syntax) (fvar : Expr) (fvarType : Expr) (s : State) : TermElabM State := do
match s.expectedType? with
| none => pure s
@ -257,6 +296,7 @@ match s.expectedType? with
match expectedType with
| Expr.forallE _ d b _ => do
isDefEq ref fvarType d;
checkNoOptAutoParam ref fvarType;
let b := b.instantiate1 fvar;
pure { expectedType? := some b, .. s }
| _ => pure { expectedType? := none, .. s }
@ -269,6 +309,7 @@ private partial def elabFunBinderViews (binderViews : Array BinderView) : Nat
/- As soon as we find an explicit binder, we switch to `explict := true` mode. -/
let s := if binderView.bi.isExplicit then { explicit := true, .. s } else s;
type ← elabType binderView.type;
checkNoOptAutoParam binderView.type type;
fvarId ← mkFreshFVarId;
let fvar := mkFVar fvarId;
let s := { fvars := s.fvars.push fvar, .. s };
@ -283,6 +324,11 @@ private partial def elabFunBinderViews (binderViews : Array BinderView) : Nat
};
if s.explicit then do
-- dbgTrace (toString binderView.id.getId ++ " : " ++ toString type);
/-
We do **not** want to support default and auto arguments in lambda abstractions.
Example: `fun (x : Nat := 10) => x+1`.
We do not believe this is an useful feature, and it would complicate the logic here.
-/
let lctx := s.lctx.mkLocalDecl fvarId binderView.id.getId type binderView.bi;
s ← propagateExpectedType binderView.id fvar type s;
continue { lctx := lctx, .. s }

21
stage0/src/Init/Lean/Elab/Command.lean
View file

@ -263,14 +263,17 @@ match result with
instance CommandElabM.inhabited {α} : Inhabited (CommandElabM α) :=
⟨throw $ arbitrary _⟩
@[inline] def runTermElabM {α} (declName? : Option Name) (elab : Array Expr → TermElabM α) : CommandElabM α := do
@[inline] def liftTermElabM {α} (declName? : Option Name) (x : TermElabM α) : CommandElabM α := do
ctx ← read;
s ← get;
match (Term.elabBinders (getVarDecls s) elab (mkTermContext ctx s declName?)).run (mkTermState s) with
match (x $ mkTermContext ctx s declName?).run (mkTermState s) with
| EStateM.Result.ok a newS => do modify $ fun s => { env := newS.env, messages := newS.messages, .. s }; pure a
| EStateM.Result.error (Term.Exception.ex ex) newS => do modify $ fun s => { env := newS.env, messages := newS.messages, .. s }; throw ex
| EStateM.Result.error Term.Exception.postpone newS => unreachable!
@[inline] def runTermElabM {α} (declName? : Option Name) (elab : Array Expr → TermElabM α) : CommandElabM α := do
s ← get; liftTermElabM declName? (Term.elabBinders (getVarDecls s) elab)
@[inline] def withLogging (x : CommandElabM Unit) : CommandElabM Unit :=
catch x (fun ex => match ex with
| Exception.error ex => do logMessage ex; pure ()
@ -643,18 +646,8 @@ let remaining := usedParams.filter (fun levelParam => !explicitParams.elem level
let remaining := remaining.qsort Name.lt;
result ++ remaining.toList
def addDecl (ref : Syntax) (decl : Declaration) : CommandElabM Unit := do
env ← getEnv;
match env.addDecl decl with
| Except.ok env => setEnv env
| Except.error kex => do opts ← getOptions; throwError ref (kex.toMessageData opts)
def compileDecl (ref : Syntax) (decl : Declaration) : CommandElabM Unit := do
env ← getEnv;
opts ← getOptions;
match env.compileDecl opts decl with
| Except.ok env => setEnv env
| Except.error kex => throwError ref (kex.toMessageData opts)
def addDecl (ref : Syntax) (decl : Declaration) : CommandElabM Unit := liftTermElabM none $ Term.addDecl ref decl
def compileDecl (ref : Syntax) (decl : Declaration) : CommandElabM Unit := liftTermElabM none $ Term.compileDecl ref decl
end Command
end Elab

21
stage0/src/Init/Lean/Elab/Term.lean
View file

@ -114,6 +114,8 @@ def getMCtx : TermElabM MetavarContext := do s ← get; pure s.mctx
def getLCtx : TermElabM LocalContext := do ctx ← read; pure ctx.lctx
def getLocalInsts : TermElabM LocalInstances := do ctx ← read; pure ctx.localInstances
def getOptions : TermElabM Options := do ctx ← read; pure ctx.config.opts
def setEnv (newEnv : Environment) : TermElabM Unit :=
modify $ fun s => { env := newEnv, .. s }
def addContext (msg : MessageData) : TermElabM MessageData := do
env ← getEnv; mctx ← getMCtx; lctx ← getLCtx; opts ← getOptions;
@ -876,6 +878,19 @@ u ← mkFreshLevelMVar stx;
type ← elabTerm stx (mkSort u);
ensureType stx type
def addDecl (ref : Syntax) (decl : Declaration) : TermElabM Unit := do
env ← getEnv;
match env.addDecl decl with
| Except.ok env => setEnv env
| Except.error kex => do opts ← getOptions; throwError ref (kex.toMessageData opts)
def compileDecl (ref : Syntax) (decl : Declaration) : TermElabM Unit := do
env ← getEnv;
opts ← getOptions;
match env.compileDecl opts decl with
| Except.ok env => setEnv env
| Except.error kex => throwError ref (kex.toMessageData opts)
/- =======================================
Builtin elaboration functions
======================================= -/
@ -909,6 +924,12 @@ fun stx expectedType? =>
| some expectedType => mkTacticMVar stx expectedType (stx.getArg 1)
| none => throwError stx ("invalid tactic block, expected type has not been provided")
@[builtinTermElab byTactic] def elabByTactic : TermElab :=
fun stx expectedType? =>
match expectedType? with
| some expectedType => mkTacticMVar stx expectedType (stx.getArg 1)
| none => throwError stx ("invalid 'by' tactic, expected type has not been provided")
/-- Main loop for `mkPairs`. -/
private partial def mkPairsAux (elems : Array Syntax) : Nat → Syntax → MacroM Syntax
| i, acc =>

14
stage0/src/Init/Lean/Elab/Util.lean
View file

@ -107,7 +107,7 @@ pure { table := table }
private def throwUnexpectedElabType {γ} (typeName : Name) (constName : Name) : ExceptT String Id γ :=
throw ("unexpected elaborator type at '" ++ toString constName ++ "', `" ++ toString typeName ++ "` expected")
private unsafe def mkElabFnOfConstantUnsafe (γ) (env : Environment) (typeName : Name) (constName : Name) : ExceptT String Id γ :=
private unsafe def evalConstantUnsafe (γ) (env : Environment) (typeName : Name) (constName : Name) : ExceptT String Id γ :=
match env.find? constName with
| none => throw ("unknow constant '" ++ toString constName ++ "'")
| some info =>
@ -117,8 +117,12 @@ match env.find? constName with
else env.evalConst γ constName
| _ => throwUnexpectedElabType typeName constName
@[implementedBy mkElabFnOfConstantUnsafe]
constant mkElabFnOfConstant (γ : Type) (env : Environment) (typeName : Name) (constName : Name) : ExceptT String Id γ := throw ""
-- We mark `evalConstant` as private because it is only safe if `mkConst typeName` is definitionally equal to `γ`.
@[implementedBy evalConstantUnsafe]
private constant evalConstant (γ : Type) (env : Environment) (typeName : Name) (constName : Name) : ExceptT String Id γ := throw ""
def evalSyntaxConstant (env : Environment) (constName : Name) : ExceptT String Id Syntax :=
evalConstant Syntax env `Lean.Syntax constName
private def ElabAttribute.addImportedParsers {γ} (typeName : Name) (builtinTableRef : IO.Ref (ElabFnTable γ))
(env : Environment) (es : Array (Array ElabAttributeOLeanEntry)) : IO (ElabAttributeExtensionState γ) := do
@ -127,7 +131,7 @@ table ← es.foldlM
(fun table entries =>
entries.foldlM
(fun (table : ElabFnTable γ) entry =>
match mkElabFnOfConstant γ env typeName entry.constName with
match evalConstant γ env typeName entry.constName with
| Except.ok f => pure $ table.insert entry.kind f
| Except.error ex => throw (IO.userError ex))
table)
@ -139,7 +143,7 @@ private def ElabAttribute.addExtensionEntry {γ} (s : ElabAttributeExtensionStat
private def ElabAttribute.add {γ} (parserNamespace : Name) (typeName : Name) (ext : ElabAttributeExtension γ)
(env : Environment) (constName : Name) (arg : Syntax) (persistent : Bool) : IO Environment := do
match mkElabFnOfConstant γ env typeName constName with
match evalConstant γ env typeName constName with
| Except.error ex => throw (IO.userError ex)
| Except.ok f => do
kind ← IO.ofExcept $ syntaxNodeKindOfAttrParam env parserNamespace arg;

12
stage0/src/Init/Lean/Expr.lean
View file

@ -733,6 +733,18 @@ if e.isAppOfArity `optParam 2 then
else
none
def getAutoParamTactic? (e : Expr) : Option Expr :=
if e.isAppOfArity `autoParam 2 then
some e.appArg!
else
none
def isOptParam (e : Expr) : Bool :=
e.isAppOfArity `optParam 2
def isAutoParam (e : Expr) : Bool :=
e.isAppOfArity `autoParam 2
@[specialize] private partial def hasAnyFVarAux (p : FVarId → Bool) : Expr → Bool
| e => if !e.hasFVar then false else
match e with

27
stage0/src/Init/Lean/Parser/Tactic.lean
View file

@ -8,17 +8,6 @@ import Init.Lean.Parser.Term
namespace Lean
namespace Parser
@[init] def regBuiltinTacticParserAttr : IO Unit :=
let leadingIdentAsSymbol := true;
registerBuiltinParserAttribute `builtinTacticParser `tactic leadingIdentAsSymbol
@[init] def regTacticParserAttribute : IO Unit :=
registerBuiltinDynamicParserAttribute `tacticParser `tactic
@[inline] def tacticParser (rbp : Nat := 0) : Parser :=
categoryParser `tactic rbp
namespace Tactic
def underscoreFn : ParserFn :=
@ -34,12 +23,6 @@ fun c s =>
def ident' : Parser := ident <|> underscore
/-
We must not use the `parser! t` macro here it because it expands into `mkAntiquot ... <|> t`,
but a tactic parser may start with an antiquotation. -/
def seq : Parser := node `Lean.Parser.Tactic.seq $ sepBy tacticParser "; " true
def nonEmptySeq : Parser := node `Lean.Parser.Tactic.seq $ sepBy1 tacticParser "; " true
@[builtinTacticParser] def «intro» := parser! nonReservedSymbol "intro " >> optional ident'
@[builtinTacticParser] def «intros» := parser! nonReservedSymbol "intros " >> many ident'
@[builtinTacticParser] def «revert» := parser! nonReservedSymbol "revert " >> many1 ident
@ -60,15 +43,5 @@ def nonEmptySeq : Parser := node `Lean.Parser.Tactic.seq $ sepBy1 tacticParser "
@[builtinTacticParser] def orelse := tparser! " <|> " >> tacticParser 1
end Tactic
namespace Term
@[builtinTermParser] def tacticBlock := parser! symbol "begin " appPrec >> Tactic.seq >> "end"
@[builtinTermParser] def byTactic := parser! symbol "by " leadPrec >> Tactic.nonEmptySeq
-- Use `unboxSingleton` trick similar to the one used at Command.lean for `Term.stxQuot`
@[builtinTermParser] def tacticStxQuot : Parser := node `Lean.Parser.Term.stxQuot $ symbol "`(tactic|" appPrec >> sepBy1 tacticParser "; " true true >> ")"
end Term
end Parser
end Lean

22
stage0/src/Init/Lean/Parser/Term.lean
View file

@ -10,6 +10,19 @@ import Init.Lean.Parser.Level
namespace Lean
namespace Parser
@[init] def regBuiltinTacticParserAttr : IO Unit :=
let leadingIdentAsSymbol := true;
registerBuiltinParserAttribute `builtinTacticParser `tactic leadingIdentAsSymbol
@[init] def regTacticParserAttribute : IO Unit :=
registerBuiltinDynamicParserAttribute `tacticParser `tactic
@[inline] def tacticParser (rbp : Nat := 0) : Parser :=
categoryParser `tactic rbp
def Tactic.seq : Parser := node `Lean.Parser.Tactic.seq $ sepBy tacticParser "; " true
def Tactic.nonEmptySeq : Parser := node `Lean.Parser.Tactic.seq $ sepBy1 tacticParser "; " true
def darrow : Parser := unicodeSymbol "⇒" "=>"
namespace Term
@ -73,9 +86,9 @@ def optType : Parser := optional typeSpec
@[builtinTermParser] def inaccessible := parser! symbol ".(" appPrec >> termParser >> ")"
def binderIdent : Parser := ident <|> hole
def binderType (requireType := false) : Parser := if requireType then group (" : " >> termParser) else optional (" : " >> termParser)
def binderTactic := parser! try (" := " >> " by ") >> Tactic.nonEmptySeq
def binderDefault := parser! " := " >> termParser
def binderTactic := parser! " . " >> termParser
def explicitBinder (requireType := false) := parser! "(" >> many1 binderIdent >> binderType requireType >> optional (binderDefault <|> binderTactic) >> ")"
def explicitBinder (requireType := false) := parser! "(" >> many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault) >> ")"
def implicitBinder (requireType := false) := parser! "{" >> many1 binderIdent >> binderType requireType >> "}"
def instBinder := parser! "[" >> optIdent >> termParser >> "]"
def bracktedBinder (requireType := false) := explicitBinder requireType <|> implicitBinder requireType <|> instBinder
@ -189,6 +202,11 @@ def checkIsSort := checkStackTop (fun stx => stx.isOfKind `Lean.Parser.Term.type
@[builtinTermParser] def mapConst := tparser! infixR " <$ " 100
@[builtinTermParser] def mapConstRev := tparser! infixR " $> " 100
@[builtinTermParser] def tacticBlock := parser! symbol "begin " appPrec >> Tactic.seq >> "end"
@[builtinTermParser] def byTactic := parser! symbol "by " leadPrec >> Tactic.nonEmptySeq
-- Use `unboxSingleton` trick similar to the one used at Command.lean for `Term.stxQuot`
@[builtinTermParser] def tacticStxQuot : Parser := node `Lean.Parser.Term.stxQuot $ symbol "`(tactic|" appPrec >> sepBy1 tacticParser "; " true true >> ")"
end Term
end Parser
end Lean

30
stage0/src/Init/Lean/Syntax.lean
View file

@ -229,6 +229,36 @@ match stx.getTailInfo with
| none => stx
| some info => stx.setTailInfo info.truncateTrailing
@[specialize] private partial def updateFirst {α} [Inhabited α] (a : Array α) (f : α → Option α) : Nat → Option (Array α)
| i =>
if h : i < a.size then
let v := a.get ⟨i, h⟩;
match f v with
| some v => some $ a.set ⟨i, h⟩ v
| none => updateFirst (i+1)
else
none
partial def setHeadInfoAux (info : Option SourceInfo) : Syntax → Option Syntax
| atom _ val => some $ atom info val
| ident _ rawVal val pre => some $ ident info rawVal val pre
| node k args =>
match updateFirst args setHeadInfoAux args.size with
| some args => some $ node k args
| noxne => none
| stx => none
def setHeadInfo (stx : Syntax) (info : Option SourceInfo) : Syntax :=
match setHeadInfoAux info stx with
| some stx => stx
| none => stx
partial def replaceInfo (info : SourceInfo) : Syntax → Syntax
| atom _ val => atom info val
| ident _ rawVal val pre => ident info rawVal val pre
| node k args => node k $ args.map replaceInfo
| stx => stx
private def reprintLeaf : Option SourceInfo → String → String
-- no source info => add gracious amounts of whitespace to definitely separate tokens
-- Note that the proper pretty printer does not use this function.

16
stage0/src/Init/LeanInit.lean
View file

@ -132,13 +132,6 @@ mkNameNum g.namePrefix g.idx
end NameGenerator
/--
Gadget for automatic parameter support. This is similar to the `optParam` gadget, but it uses
the tactic declaration name `tacName` to synthesize the argument.
Like `optParam`, this gadget only affects elaboration.
For example, the tactic will *not* be invoked during type class resolution. -/
abbrev autoParam.{u} (α : Sort u) (tacName : Name) : Sort u := α
/-
Small DSL for describing parsers. We implement an interpreter for it
at `Parser.lean` -/
@ -175,6 +168,8 @@ structure SourceInfo :=
(pos : String.Pos)
(trailing : Substring)
instance SourceInfo.inhabited : Inhabited SourceInfo := ⟨⟨"".toSubstring, arbitrary _, "".toSubstring⟩⟩
abbrev SyntaxNodeKind := Name
/- Syntax AST -/
@ -814,3 +809,10 @@ def mapSepElems (a : Array Syntax) (f : Syntax → Syntax) : Array Syntax :=
Id.run $ a.mapSepElemsM f
end Array
/--
Gadget for automatic parameter support. This is similar to the `optParam` gadget, but it uses
the given tactic.
Like `optParam`, this gadget only affects elaboration.
For example, the tactic will *not* be invoked during type class resolution. -/
abbrev autoParam.{u} (α : Sort u) (tactic : Lean.Syntax) : Sort u := α

1
stage0/src/library/compiler/csimp.cpp
View file

@ -330,7 +330,6 @@ class csimp_fn {
};
void collect_cases_info(expr e, cases_info_result & result) {
lean_assert(m_before_erasure);
while (true) {
if (is_lambda(e))
e = binding_body(e);

11513
stage0/stdlib/Init/Lean/Elab/App.c
View file

File diff suppressed because it is too large Load diff

6327
stage0/stdlib/Init/Lean/Elab/Binders.c
View file

File diff suppressed because it is too large Load diff

74
stage0/stdlib/Init/Lean/Elab/BuiltinNotation.c
View file

@ -34,7 +34,6 @@ extern lean_object* l_Lean_Parser_Term_andthen___elambda__1___closed__1;
lean_object* l___regBuiltinMacro_Lean_Elab_Term_elabGE(lean_object*);
lean_object* l_Lean_Elab_Term_elabBAnd___closed__1;
lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__13;
extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__34;
extern lean_object* l_Lean_Expr_eq_x3f___closed__2;
lean_object* l___regBuiltinMacro_Lean_Elab_Term_elabNe(lean_object*);
lean_object* l___regBuiltinMacro_Lean_Elab_Term_elabEq___closed__1;
@ -214,6 +213,7 @@ extern lean_object* l_Lean_Parser_Term_mul___elambda__1___closed__2;
lean_object* l___regBuiltinMacro_Lean_Elab_Term_elabOrElse(lean_object*);
extern lean_object* l_Lean_Parser_Term_div___elambda__1___closed__1;
extern lean_object* l_Lean_Parser_Term_tparser_x21___elambda__1___closed__2;
extern lean_object* l_Lean_Parser_Tactic_seq___elambda__1___closed__3;
extern lean_object* l_Lean_Parser_Term_ge___elambda__1___closed__2;
lean_object* l_Lean_Elab_Term_elabseq___closed__3;
extern lean_object* l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___closed__2;
@ -223,7 +223,6 @@ lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, lean
lean_object* l_Lean_Elab_Term_expandIf___closed__4;
extern lean_object* l_Lean_Parser_Term_sub___elambda__1___closed__1;
lean_object* l___regBuiltinMacro_Lean_Elab_Term_elabseq(lean_object*);
extern lean_object* l_Lean_Parser_Term_seq___elambda__1___closed__2;
lean_object* l_Lean_Elab_Term_elabTParserMacro___lambda__1___closed__10;
lean_object* l_Lean_Elab_Term_elabLE___closed__1;
lean_object* l_Lean_Elab_Term_ElabFComp___closed__4;
@ -285,7 +284,6 @@ extern lean_object* l_Lean_Parser_Term_iff___elambda__1___closed__2;
lean_object* l_Lean_Elab_Term_elabAnonymousCtor___closed__9;
lean_object* l_Lean_Elab_Term_elabLE(lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__31;
extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
lean_object* l_Lean_Elab_Term_expandShow(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabOr___closed__1;
lean_object* l_Lean_Elab_Term_elabAnonymousCtor___closed__3;
@ -362,7 +360,6 @@ lean_object* l___regBuiltinMacro_Lean_Elab_Term_elabMod___closed__1;
lean_object* l_Lean_Elab_Term_elabMap___closed__2;
lean_object* l_Lean_Elab_Term_expandSubtype___closed__3;
lean_object* l_Lean_Elab_Term_expandHave(lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
extern lean_object* l_Lean_Parser_Term_le___elambda__1___closed__2;
extern lean_object* l_Lean_Parser_Term_str___elambda__1___closed__2;
lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__20;
@ -397,7 +394,6 @@ lean_object* l_Lean_Elab_Term_expandIf___closed__8;
lean_object* l___regBuiltinMacro_Lean_Elab_Term_elabBNe___closed__1;
extern lean_object* l___private_Init_Util_1__mkPanicMessage___closed__2;
extern lean_object* l_Lean_Parser_Term_append___elambda__1___closed__2;
extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__32;
lean_object* l_Lean_Elab_Term_elabGE___closed__1;
lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__10;
lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__32;
@ -424,6 +420,7 @@ lean_object* l_Lean_Elab_Term_elabParserMacro___closed__1;
lean_object* l_Lean_Elab_Term_ElabFComp___closed__3;
lean_object* l_Lean_Elab_Term_elabAndThen___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_mkAppStx___closed__9;
extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__42;
extern lean_object* l_Lean_Parser_Term_and___elambda__1___closed__2;
lean_object* l_Lean_Elab_Term_elabAnonymousCtor___closed__13;
extern lean_object* l_Lean_Parser_Term_mapRev___elambda__1___closed__1;
@ -471,10 +468,12 @@ lean_object* l_Lean_Elab_Term_elabCons(lean_object*, lean_object*, lean_object*)
extern lean_object* l___private_Init_Lean_Elab_Term_5__expandCDot___main___closed__4;
lean_object* l_Lean_Elab_Term_elabMod(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabAnonymousCtor___closed__7;
extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__30;
extern lean_object* l_Lean_Parser_Term_map___elambda__1___closed__2;
lean_object* l___regBuiltinMacro_Lean_Elab_Term_elabBOr(lean_object*);
extern lean_object* l_Lean_Parser_Term_orelse___elambda__1___closed__2;
lean_object* l___regBuiltinMacro_Lean_Elab_Term_elabMapConst___closed__1;
extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
lean_object* l___regBuiltinMacro_Lean_Elab_Term_elabLT(lean_object*);
lean_object* l_Lean_Elab_Term_elabBEq___closed__2;
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabTParserMacro(lean_object*);
@ -492,6 +491,7 @@ extern lean_object* l_Lean_Parser_Term_bne___elambda__1___closed__1;
lean_object* l___regBuiltinMacro_Lean_Elab_Term_elabAndM(lean_object*);
lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__25;
lean_object* l___regBuiltinMacro_Lean_Elab_Term_elabAnd___closed__1;
extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__33;
extern lean_object* l_Lean_Parser_Term_map___elambda__1___closed__1;
lean_object* l_Lean_Elab_Term_elabAndThen(lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinMacro_Lean_Elab_Term_elabGT___closed__1;
@ -1135,9 +1135,9 @@ x_91 = lean_array_push(x_90, x_72);
x_92 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_92, 0, x_45);
lean_ctor_set(x_92, 1, x_91);
x_93 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_93 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__42;
x_94 = lean_array_push(x_93, x_92);
x_95 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_95 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
x_96 = lean_array_push(x_94, x_95);
x_97 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___closed__2;
x_98 = lean_alloc_ctor(1, 2, 0);
@ -1453,9 +1453,9 @@ x_39 = l_Lean_nullKind___closed__2;
x_40 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_40, 0, x_39);
lean_ctor_set(x_40, 1, x_38);
x_41 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_41 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__42;
x_42 = lean_array_push(x_41, x_40);
x_43 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_43 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
x_44 = lean_array_push(x_42, x_43);
x_45 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___closed__2;
x_46 = lean_alloc_ctor(1, 2, 0);
@ -1623,9 +1623,9 @@ x_112 = lean_array_push(x_105, x_111);
x_113 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_113, 0, x_69);
lean_ctor_set(x_113, 1, x_112);
x_114 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_114 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__42;
x_115 = lean_array_push(x_114, x_113);
x_116 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_116 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
x_117 = lean_array_push(x_115, x_116);
x_118 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___closed__2;
x_119 = lean_alloc_ctor(1, 2, 0);
@ -2454,9 +2454,9 @@ x_28 = lean_array_push(x_20, x_27);
x_29 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_29, 0, x_26);
lean_ctor_set(x_29, 1, x_28);
x_30 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_30 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__42;
x_31 = lean_array_push(x_30, x_29);
x_32 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_32 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
x_33 = lean_array_push(x_31, x_32);
x_34 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___closed__2;
x_35 = lean_alloc_ctor(1, 2, 0);
@ -2695,9 +2695,9 @@ x_41 = lean_array_push(x_33, x_40);
x_42 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_42, 0, x_39);
lean_ctor_set(x_42, 1, x_41);
x_43 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_43 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__42;
x_44 = lean_array_push(x_43, x_42);
x_45 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_45 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
x_46 = lean_array_push(x_44, x_45);
x_47 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___closed__2;
x_48 = lean_alloc_ctor(1, 2, 0);
@ -2803,9 +2803,9 @@ x_97 = lean_array_push(x_89, x_96);
x_98 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_98, 0, x_95);
lean_ctor_set(x_98, 1, x_97);
x_99 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_99 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__42;
x_100 = lean_array_push(x_99, x_98);
x_101 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_101 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
x_102 = lean_array_push(x_100, x_101);
x_103 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___closed__2;
x_104 = lean_alloc_ctor(1, 2, 0);
@ -2949,9 +2949,9 @@ x_165 = lean_array_push(x_158, x_164);
x_166 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_166, 0, x_135);
lean_ctor_set(x_166, 1, x_165);
x_167 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_167 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__42;
x_168 = lean_array_push(x_167, x_166);
x_169 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_169 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
x_170 = lean_array_push(x_168, x_169);
x_171 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___closed__2;
x_172 = lean_alloc_ctor(1, 2, 0);
@ -3052,9 +3052,9 @@ x_218 = lean_array_push(x_211, x_217);
x_219 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_219, 0, x_135);
lean_ctor_set(x_219, 1, x_218);
x_220 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_220 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__42;
x_221 = lean_array_push(x_220, x_219);
x_222 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_222 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
x_223 = lean_array_push(x_221, x_222);
x_224 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___closed__2;
x_225 = lean_alloc_ctor(1, 2, 0);
@ -3856,10 +3856,10 @@ lean_ctor_set(x_76, 0, x_43);
lean_ctor_set(x_76, 1, x_75);
x_77 = lean_array_push(x_39, x_76);
x_78 = lean_array_push(x_39, x_26);
x_79 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__32;
x_79 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__31;
x_80 = l_Lean_addMacroScope(x_59, x_79, x_55);
x_81 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__31;
x_82 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__34;
x_81 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__30;
x_82 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__33;
x_83 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_83, 0, x_21);
lean_ctor_set(x_83, 1, x_81);
@ -3883,9 +3883,9 @@ x_92 = lean_array_push(x_91, x_41);
x_93 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_93, 0, x_48);
lean_ctor_set(x_93, 1, x_92);
x_94 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_94 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__42;
x_95 = lean_array_push(x_94, x_93);
x_96 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_96 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
x_97 = lean_array_push(x_95, x_96);
x_98 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___closed__2;
x_99 = lean_alloc_ctor(1, 2, 0);
@ -3946,10 +3946,10 @@ lean_ctor_set(x_123, 0, x_43);
lean_ctor_set(x_123, 1, x_122);
x_124 = lean_array_push(x_39, x_123);
x_125 = lean_array_push(x_39, x_26);
x_126 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__32;
x_126 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__31;
x_127 = l_Lean_addMacroScope(x_105, x_126, x_55);
x_128 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__31;
x_129 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__34;
x_128 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__30;
x_129 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__33;
x_130 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_130, 0, x_21);
lean_ctor_set(x_130, 1, x_128);
@ -3973,9 +3973,9 @@ x_139 = lean_array_push(x_138, x_41);
x_140 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_140, 0, x_48);
lean_ctor_set(x_140, 1, x_139);
x_141 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_141 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__42;
x_142 = lean_array_push(x_141, x_140);
x_143 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_143 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
x_144 = lean_array_push(x_142, x_143);
x_145 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___closed__2;
x_146 = lean_alloc_ctor(1, 2, 0);
@ -4074,9 +4074,9 @@ x_191 = lean_array_push(x_190, x_41);
x_192 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_192, 0, x_48);
lean_ctor_set(x_192, 1, x_191);
x_193 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_193 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__42;
x_194 = lean_array_push(x_193, x_192);
x_195 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_195 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
x_196 = lean_array_push(x_194, x_195);
x_197 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___closed__2;
x_198 = lean_alloc_ctor(1, 2, 0);
@ -4182,9 +4182,9 @@ x_248 = lean_array_push(x_247, x_41);
x_249 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_249, 0, x_48);
lean_ctor_set(x_249, 1, x_248);
x_250 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_250 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__42;
x_251 = lean_array_push(x_250, x_249);
x_252 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_252 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
x_253 = lean_array_push(x_251, x_252);
x_254 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___closed__2;
x_255 = lean_alloc_ctor(1, 2, 0);
@ -6277,7 +6277,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Term_elabseq___closed__2;
x_2 = l_Lean_Parser_Term_seq___elambda__1___closed__1;
x_2 = l_Lean_Parser_Tactic_seq___elambda__1___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -6313,7 +6313,7 @@ lean_object* l___regBuiltinMacro_Lean_Elab_Term_elabseq(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = l_Lean_Parser_Term_seq___elambda__1___closed__2;
x_2 = l_Lean_Parser_Term_seq___elambda__1___closed__1;
x_3 = l___regBuiltinMacro_Lean_Elab_Term_elabseq___closed__1;
x_4 = l_Lean_Elab_addBuiltinMacro(x_2, x_3, x_1);
return x_4;

4688
stage0/stdlib/Init/Lean/Elab/Command.c
View file

File diff suppressed because it is too large Load diff

2225
stage0/stdlib/Init/Lean/Elab/Declaration.c
View file

File diff suppressed because it is too large Load diff

2354
stage0/stdlib/Init/Lean/Elab/Definition.c
View file

File diff suppressed because it is too large Load diff

26
stage0/stdlib/Init/Lean/Elab/DoNotation.c
View file

@ -47,6 +47,7 @@ lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
uint8_t l___private_Init_Lean_Elab_DoNotation_4__hasLiftMethod(lean_object*);
lean_object* l_Lean_Expr_getAppFn___main(lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__1;
extern lean_object* l___private_Init_Lean_Elab_Term_5__expandCDot___main___closed__2;
lean_object* l_Lean_Elab_Term_synthesizeInst(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_DoNotation_3__getDoElems___boxed(lean_object*);
@ -76,7 +77,6 @@ lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, lean
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_DoNotation_12__processDoElems(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__6;
extern lean_object* l_Lean_Elab_Term_elabLetDecl___closed__4;
extern lean_object* l_Lean_Parser_Term_doId___elambda__1___closed__2;
lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__6;
@ -120,6 +120,7 @@ lean_object* l___private_Init_Lean_Elab_DoNotation_10__mkBind(lean_object*, lean
extern lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__7;
lean_object* lean_environment_main_module(lean_object*);
uint8_t l_Lean_Expr_isMVar(lean_object*);
extern lean_object* l_Lean_Elab_Term_elabLetDecl___closed__2;
extern lean_object* l_Lean_Parser_Term_match___elambda__1___closed__2;
lean_object* l_Lean_mkApp(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_bracketedDoSeq___elambda__1___closed__2;
@ -162,7 +163,6 @@ lean_object* l___private_Init_Lean_Elab_DoNotation_11__processDoElemsAux___main_
lean_object* l___private_Init_Lean_Elab_DoNotation_9__extractTypeFormerAppArg___closed__3;
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_mkAppN___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__1;
lean_object* l___private_Init_Lean_Elab_DoNotation_7__expandDoElemsAux___main___closed__1;
lean_object* l___private_Init_Lean_Elab_DoNotation_7__expandDoElemsAux___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkAppB(lean_object*, lean_object*, lean_object*);
@ -2112,7 +2112,7 @@ x_82 = lean_box(0);
x_83 = l_Lean_Meta_AbstractMVars_abstractExprMVars___main___closed__2;
x_84 = l_Lean_addMacroScope(x_81, x_83, x_80);
x_85 = lean_box(0);
x_86 = l_Lean_Elab_Term_elabLetDecl___closed__4;
x_86 = l_Lean_Elab_Term_elabLetDecl___closed__2;
x_87 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_87, 0, x_82);
lean_ctor_set(x_87, 1, x_86);
@ -2218,7 +2218,7 @@ lean_dec(x_121);
x_146 = l_Lean_Meta_AbstractMVars_abstractExprMVars___main___closed__2;
x_147 = l_Lean_addMacroScope(x_128, x_146, x_60);
x_148 = lean_box(0);
x_149 = l_Lean_Elab_Term_elabLetDecl___closed__4;
x_149 = l_Lean_Elab_Term_elabLetDecl___closed__2;
x_150 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_150, 0, x_129);
lean_ctor_set(x_150, 1, x_149);
@ -2306,7 +2306,7 @@ lean_dec(x_121);
x_199 = l_Lean_Meta_AbstractMVars_abstractExprMVars___main___closed__2;
x_200 = l_Lean_addMacroScope(x_128, x_199, x_60);
x_201 = lean_box(0);
x_202 = l_Lean_Elab_Term_elabLetDecl___closed__4;
x_202 = l_Lean_Elab_Term_elabLetDecl___closed__2;
x_203 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_203, 0, x_129);
lean_ctor_set(x_203, 1, x_202);
@ -2402,7 +2402,7 @@ x_253 = lean_box(0);
x_254 = l_Lean_Meta_AbstractMVars_abstractExprMVars___main___closed__2;
x_255 = l_Lean_addMacroScope(x_250, x_254, x_60);
x_256 = lean_box(0);
x_257 = l_Lean_Elab_Term_elabLetDecl___closed__4;
x_257 = l_Lean_Elab_Term_elabLetDecl___closed__2;
x_258 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_258, 0, x_253);
lean_ctor_set(x_258, 1, x_257);
@ -2495,7 +2495,7 @@ x_311 = lean_box(0);
x_312 = l_Lean_Meta_AbstractMVars_abstractExprMVars___main___closed__2;
x_313 = l_Lean_addMacroScope(x_250, x_312, x_60);
x_314 = lean_box(0);
x_315 = l_Lean_Elab_Term_elabLetDecl___closed__4;
x_315 = l_Lean_Elab_Term_elabLetDecl___closed__2;
x_316 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_316, 0, x_311);
lean_ctor_set(x_316, 1, x_315);
@ -2805,7 +2805,7 @@ x_463 = lean_box(0);
x_464 = l_Lean_Meta_AbstractMVars_abstractExprMVars___main___closed__2;
x_465 = l_Lean_addMacroScope(x_462, x_464, x_461);
x_466 = lean_box(0);
x_467 = l_Lean_Elab_Term_elabLetDecl___closed__4;
x_467 = l_Lean_Elab_Term_elabLetDecl___closed__2;
x_468 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_468, 0, x_463);
lean_ctor_set(x_468, 1, x_467);
@ -2911,7 +2911,7 @@ lean_dec(x_502);
x_527 = l_Lean_Meta_AbstractMVars_abstractExprMVars___main___closed__2;
x_528 = l_Lean_addMacroScope(x_509, x_527, x_442);
x_529 = lean_box(0);
x_530 = l_Lean_Elab_Term_elabLetDecl___closed__4;
x_530 = l_Lean_Elab_Term_elabLetDecl___closed__2;
x_531 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_531, 0, x_510);
lean_ctor_set(x_531, 1, x_530);
@ -2999,7 +2999,7 @@ lean_dec(x_502);
x_580 = l_Lean_Meta_AbstractMVars_abstractExprMVars___main___closed__2;
x_581 = l_Lean_addMacroScope(x_509, x_580, x_442);
x_582 = lean_box(0);
x_583 = l_Lean_Elab_Term_elabLetDecl___closed__4;
x_583 = l_Lean_Elab_Term_elabLetDecl___closed__2;
x_584 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_584, 0, x_510);
lean_ctor_set(x_584, 1, x_583);
@ -3095,7 +3095,7 @@ x_634 = lean_box(0);
x_635 = l_Lean_Meta_AbstractMVars_abstractExprMVars___main___closed__2;
x_636 = l_Lean_addMacroScope(x_631, x_635, x_442);
x_637 = lean_box(0);
x_638 = l_Lean_Elab_Term_elabLetDecl___closed__4;
x_638 = l_Lean_Elab_Term_elabLetDecl___closed__2;
x_639 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_639, 0, x_634);
lean_ctor_set(x_639, 1, x_638);
@ -3188,7 +3188,7 @@ x_692 = lean_box(0);
x_693 = l_Lean_Meta_AbstractMVars_abstractExprMVars___main___closed__2;
x_694 = l_Lean_addMacroScope(x_631, x_693, x_442);
x_695 = lean_box(0);
x_696 = l_Lean_Elab_Term_elabLetDecl___closed__4;
x_696 = l_Lean_Elab_Term_elabLetDecl___closed__2;
x_697 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_697, 0, x_692);
lean_ctor_set(x_697, 1, x_696);
@ -4991,7 +4991,7 @@ lean_object* _init_l_Lean_Elab_Term_elabDo___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__1;
x_1 = l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__1;
x_2 = l_Lean_Parser_Term_do___elambda__1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;

6
stage0/stdlib/Init/Lean/Elab/Frontend.c
View file

@ -23,7 +23,6 @@ lean_object* l_Lean_Elab_IO_processCommands(lean_object*, lean_object*, lean_obj
lean_object* l_Lean_Elab_runFrontend(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Frontend_processCommandsAux___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Frontend_liftIOCore_x21(lean_object*);
extern lean_object* l_Lean_Elab_Command_runTermElabM___rarg___closed__1;
lean_object* lean_io_mk_ref(lean_object*, lean_object*);
lean_object* lean_io_ref_get(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Frontend_runCommandElabM___closed__1;
@ -77,6 +76,7 @@ uint8_t l_PersistentArray_anyM___at_Lean_MessageLog_hasErrors___spec__1(lean_obj
extern lean_object* l_Nat_Inhabited;
lean_object* l_Lean_Elab_Frontend_getParserState___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_process(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Command_liftTermElabM___rarg___closed__1;
lean_object* l_Lean_Elab_Frontend_processCommands___boxed(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Command_3__setState(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Frontend_processCommands(lean_object*, lean_object*);
@ -597,7 +597,7 @@ lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68;
x_65 = lean_ctor_get(x_16, 1);
lean_inc(x_65);
lean_dec(x_16);
x_66 = l_Lean_Elab_Command_runTermElabM___rarg___closed__1;
x_66 = l_Lean_Elab_Command_liftTermElabM___rarg___closed__1;
x_67 = l_unreachable_x21___rarg(x_66);
x_68 = lean_apply_2(x_67, x_15, x_65);
if (lean_obj_tag(x_68) == 0)
@ -905,7 +905,7 @@ lean_object* x_142; lean_object* x_143; lean_object* x_144; lean_object* x_145;
x_142 = lean_ctor_get(x_93, 1);
lean_inc(x_142);
lean_dec(x_93);
x_143 = l_Lean_Elab_Command_runTermElabM___rarg___closed__1;
x_143 = l_Lean_Elab_Command_liftTermElabM___rarg___closed__1;
x_144 = l_unreachable_x21___rarg(x_143);
x_145 = lean_apply_2(x_144, x_92, x_142);
if (lean_obj_tag(x_145) == 0)

430
stage0/stdlib/Init/Lean/Elab/Quotation.c
View file

File diff suppressed because it is too large Load diff

850
stage0/stdlib/Init/Lean/Elab/Syntax.c
View file

File diff suppressed because it is too large Load diff

8
stage0/stdlib/Init/Lean/Elab/SyntheticMVars.c
View file

@ -36,6 +36,7 @@ lean_object* l_List_find_x3f___main___rarg(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_SyntheticMVars_11__synthesizeSyntheticMVarsAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppFn___main(lean_object*);
lean_object* l_PersistentArray_push___rarg(lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__1;
lean_object* l_Lean_Elab_Term_synthesizeSyntheticMVars(uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_assignExprMVar(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
@ -134,7 +135,6 @@ lean_object* l_List_filterAuxM___main___at___private_Init_Lean_Elab_SyntheticMVa
lean_object* l_Lean_MetavarContext_instantiateMVarDeclMVars(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_SyntheticMVars_10__getSomeSynthethicMVarsRef___rarg(lean_object*);
uint8_t l_List_isEmpty___rarg(lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__1;
lean_object* l___private_Init_Lean_Elab_SyntheticMVars_10__getSomeSynthethicMVarsRef___rarg___closed__1;
lean_object* l_Lean_indentExpr(lean_object*);
extern lean_object* l_Lean_Format_repr___main___closed__16;
@ -2775,7 +2775,7 @@ lean_object* _init_l___private_Init_Lean_Elab_SyntheticMVars_7__synthesizeSynthe
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__1;
x_1 = l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__1;
x_2 = l___private_Init_Lean_Elab_SyntheticMVars_7__synthesizeSyntheticMVarsStep___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -2934,7 +2934,7 @@ x_9 = l_List_lengthAux___main___rarg(x_7, x_8);
x_10 = lean_box(0);
lean_ctor_set(x_5, 1, x_10);
x_11 = l_List_reverse___rarg(x_7);
x_12 = l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__1;
x_12 = l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__1;
x_13 = l_List_filterAuxM___main___at___private_Init_Lean_Elab_SyntheticMVars_7__synthesizeSyntheticMVarsStep___spec__2(x_1, x_2, x_12, x_11, x_10, x_3, x_5);
if (lean_obj_tag(x_13) == 0)
{
@ -3149,7 +3149,7 @@ lean_ctor_set(x_73, 3, x_67);
lean_ctor_set(x_73, 4, x_68);
lean_ctor_set(x_73, 5, x_69);
x_74 = l_List_reverse___rarg(x_65);
x_75 = l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__1;
x_75 = l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__1;
x_76 = l_List_filterAuxM___main___at___private_Init_Lean_Elab_SyntheticMVars_7__synthesizeSyntheticMVarsStep___spec__2(x_1, x_2, x_75, x_74, x_72, x_3, x_73);
if (lean_obj_tag(x_76) == 0)
{

26
stage0/stdlib/Init/Lean/Elab/Tactic/Basic.c
View file

@ -41,6 +41,7 @@ extern lean_object* l_Lean_Elab_Term_elabTermAux___main___closed__6;
lean_object* l_List_map___main___at_Lean_Elab_goalsToMessageData___spec__1(lean_object*);
lean_object* l_Lean_Elab_Tactic_mkTacticAttribute(lean_object*);
lean_object* l_Lean_Elab_Tactic_evalSkip___boxed(lean_object*, lean_object*);
lean_object* l_IO_ofExcept___at___private_Init_Lean_Elab_Util_7__ElabAttribute_add___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_getMCtx___rarg(lean_object*);
lean_object* l_Lean_Elab_Tactic_monadQuotation___closed__4;
extern lean_object* l_Lean_Parser_Tactic_seq___elambda__1___closed__2;
@ -116,10 +117,12 @@ extern lean_object* l_Lean_Parser_Tactic_assumption___elambda__1___closed__2;
lean_object* l_Lean_Elab_Tactic_withFreshMacroScope(lean_object*);
lean_object* l_Lean_MetavarContext_renameMVar(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_reportUnsolvedGoals___closed__3;
extern lean_object* l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__1;
lean_object* l_AssocList_find___main___at_Lean_Elab_Tactic_evalTactic___main___spec__6___boxed(lean_object*, lean_object*);
lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalNestedTacticBlock___closed__2;
size_t l_USize_shiftRight(size_t, size_t);
lean_object* l_Lean_Elab_Tactic_resettingSynthInstanceCacheWhen___rarg(uint8_t, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__3;
uint8_t l_PersistentHashMap_containsAux___main___at_Lean_Elab_Tactic_addBuiltinTactic___spec__5(lean_object*, size_t, lean_object*);
lean_object* l_Lean_Elab_Tactic_getLocalInsts(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_monadLog___closed__10;
@ -182,7 +185,6 @@ lean_object* l_Lean_Elab_Term_isExprMVarAssigned___boxed(lean_object*, lean_obje
lean_object* l_Lean_Name_append___main(lean_object*, lean_object*);
lean_object* l_PersistentHashMap_findAux___main___at_Lean_Elab_Tactic_evalTactic___main___spec__3___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_dbgTrace___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Tactic_seq___elambda__1___closed__3;
lean_object* l_Lean_Elab_Tactic_Lean_Elab_MonadMacroAdapter___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_addContext(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalClear___closed__1;
@ -382,6 +384,7 @@ lean_object* l_Lean_Elab_Tactic_addBuiltinTactic___boxed(lean_object*, lean_obje
lean_object* l_Lean_SMap_empty___at_Lean_Elab_Tactic_mkBuiltinTacticTable___spec__1___closed__1;
lean_object* l_Lean_Elab_Tactic_addBuiltinTactic___closed__1;
lean_object* l_Lean_Elab_Tactic_assignExprMVar(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Tactic_seq___elambda__1___closed__4;
lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalParen___closed__1;
lean_object* l_Lean_Elab_Tactic_ensureHasNoMVars(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_erase___main___at_Lean_Elab_Tactic_evalCase___spec__2___boxed(lean_object*, lean_object*);
@ -458,7 +461,6 @@ lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalAssumption___closed__3;
lean_object* l_Array_iterateMAux___main___at_Lean_mkAppN___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_dbgTrace(lean_object*);
lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__1;
lean_object* l_Lean_Elab_Tactic_monadLog___lambda__3___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_EStateM_Backtrackable___closed__3;
lean_object* lean_usize_to_nat(size_t);
@ -475,7 +477,6 @@ lean_object* l_Lean_indentExpr(lean_object*);
lean_object* l_Lean_Elab_Tactic_getMainModule___boxed(lean_object*);
extern lean_object* l_Lean_Parser_Tactic_traceState___elambda__1___closed__2;
lean_object* l_Lean_Elab_Tactic_monadQuotation___closed__3;
lean_object* l_IO_ofExcept___at___private_Init_Lean_Elab_Util_6__ElabAttribute_add___spec__1(lean_object*, lean_object*);
lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalSkip(lean_object*);
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalIntros___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -510,7 +511,6 @@ uint8_t lean_string_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalIntros___lambda__2___boxed(lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalSkip___rarg(lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__3;
lean_object* l_Lean_Elab_Tactic_withIncRecDepth(lean_object*);
lean_object* l_List_map___main___at_Lean_Elab_goalsToMessageData___spec__1(lean_object* x_1) {
_start:
@ -3610,7 +3610,7 @@ lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_8 = l_Lean_Parser_Tactic_seq___elambda__1___closed__2;
lean_inc(x_1);
x_9 = l_Lean_Elab_syntaxNodeKindOfAttrParam(x_1, x_8, x_3);
x_10 = l_IO_ofExcept___at___private_Init_Lean_Elab_Util_6__ElabAttribute_add___spec__1(x_9, x_5);
x_10 = l_IO_ofExcept___at___private_Init_Lean_Elab_Util_7__ElabAttribute_add___spec__1(x_9, x_5);
lean_dec(x_9);
if (lean_obj_tag(x_10) == 0)
{
@ -6252,7 +6252,7 @@ lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27;
lean_inc(x_1);
x_24 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalTactic___main___lambda__1___boxed), 2, 1);
lean_closure_set(x_24, 0, x_1);
x_25 = l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__3;
x_25 = l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__3;
lean_inc(x_1);
x_26 = lean_alloc_closure((void*)(l_Lean_Elab_Term_trace___boxed), 5, 3);
lean_closure_set(x_26, 0, x_25);
@ -6421,7 +6421,7 @@ lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77;
lean_inc(x_1);
x_74 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalTactic___main___lambda__1___boxed), 2, 1);
lean_closure_set(x_74, 0, x_1);
x_75 = l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__3;
x_75 = l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__3;
lean_inc(x_1);
x_76 = lean_alloc_closure((void*)(l_Lean_Elab_Term_trace___boxed), 5, 3);
lean_closure_set(x_76, 0, x_75);
@ -6615,7 +6615,7 @@ lean_object* x_128; lean_object* x_129; lean_object* x_130; lean_object* x_131;
lean_inc(x_1);
x_128 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalTactic___main___lambda__1___boxed), 2, 1);
lean_closure_set(x_128, 0, x_1);
x_129 = l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__3;
x_129 = l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__3;
lean_inc(x_1);
x_130 = lean_alloc_closure((void*)(l_Lean_Elab_Term_trace___boxed), 5, 3);
lean_closure_set(x_130, 0, x_129);
@ -6841,7 +6841,7 @@ lean_object* x_191; lean_object* x_192; lean_object* x_193; lean_object* x_194;
lean_inc(x_1);
x_191 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalTactic___main___lambda__1___boxed), 2, 1);
lean_closure_set(x_191, 0, x_1);
x_192 = l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__3;
x_192 = l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__3;
lean_inc(x_1);
x_193 = lean_alloc_closure((void*)(l_Lean_Elab_Term_trace___boxed), 5, 3);
lean_closure_set(x_193, 0, x_192);
@ -7114,7 +7114,7 @@ lean_object* x_267; lean_object* x_268; lean_object* x_269; lean_object* x_270;
lean_inc(x_1);
x_267 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalTactic___main___lambda__1___boxed), 2, 1);
lean_closure_set(x_267, 0, x_1);
x_268 = l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__3;
x_268 = l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__3;
lean_inc(x_1);
x_269 = lean_alloc_closure((void*)(l_Lean_Elab_Term_trace___boxed), 5, 3);
lean_closure_set(x_269, 0, x_268);
@ -7414,7 +7414,7 @@ lean_object* x_347; lean_object* x_348; lean_object* x_349; lean_object* x_350;
lean_inc(x_1);
x_347 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalTactic___main___lambda__1___boxed), 2, 1);
lean_closure_set(x_347, 0, x_1);
x_348 = l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__3;
x_348 = l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__3;
lean_inc(x_1);
x_349 = lean_alloc_closure((void*)(l_Lean_Elab_Term_trace___boxed), 5, 3);
lean_closure_set(x_349, 0, x_348);
@ -13297,7 +13297,7 @@ lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalSeq(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_Parser_Tactic_seq___elambda__1___closed__3;
x_2 = l_Lean_Parser_Tactic_seq___elambda__1___closed__4;
x_3 = l___regBuiltinTactic_Lean_Elab_Tactic_evalSeq___closed__2;
x_4 = l___regBuiltinTactic_Lean_Elab_Tactic_evalSeq___closed__3;
x_5 = l_Lean_Elab_Tactic_addBuiltinTactic(x_2, x_3, x_4, x_1);
@ -16606,7 +16606,7 @@ lean_object* _init_l___private_Init_Lean_Elab_Tactic_Basic_4__regTraceClasses___
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__1;
x_1 = l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__1;
x_2 = l_Lean_Parser_regBuiltinTacticParserAttr___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;

365
stage0/stdlib/Init/Lean/Elab/Term.c
View file

@ -55,6 +55,7 @@ extern lean_object* l_Lean_Parser_declareBuiltinParser___closed__8;
lean_object* l_Lean_Elab_Term_State_inhabited;
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabChar(lean_object*);
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabByTactic___closed__3;
lean_object* l_Lean_mkSort(lean_object*);
lean_object* l_Lean_Elab_Term_instantiateMVars(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___closed__9;
@ -68,6 +69,7 @@ lean_object* l_Lean_Meta_whnfForall(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_umapMAux___main___at___private_Init_Lean_Elab_Term_5__expandCDot___main___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabTermAux___main___closed__6;
lean_object* l_Lean_Elab_Term_monadLog___lambda__3___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_IO_ofExcept___at___private_Init_Lean_Elab_Util_7__ElabAttribute_add___spec__1(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Term_8__exceptionToSorry___closed__1;
extern lean_object* l_Lean_MessageData_ofList___closed__3;
lean_object* l_Lean_Elab_Term_declareBuiltinTermElab___closed__2;
@ -156,6 +158,7 @@ lean_object* l_Lean_Elab_Term_withoutPostponing(lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabRawNumLit___closed__3;
lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___closed__13;
lean_object* l_Lean_Elab_Term_decLevel(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_compileDecl(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabRawStrLit___closed__2;
lean_object* l_Lean_Elab_Term_elabParen___closed__3;
lean_object* l___private_Init_Lean_Elab_Term_18__mkFreshLevelMVars___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -164,6 +167,7 @@ lean_object* l_Lean_Elab_Term_getMVarDecl(lean_object*, lean_object*, lean_objec
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabListLit___closed__1;
lean_object* l_Lean_Elab_Term_mkLambda(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_instantiate1(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_compileDecl___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Literal_type___closed__3;
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
@ -197,6 +201,7 @@ lean_object* l_Lean_Elab_Term_withIncRecDepth(lean_object*);
lean_object* l_List_foldlM___main___at___private_Init_Lean_Elab_Term_19__mkConsts___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_WHNF_unfoldDefinitionAux___at_Lean_Meta_unfoldDefinition_x3f___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Term_16__resolveLocalNameAux___main(lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__1;
extern lean_object* l_List_repr___rarg___closed__3;
extern lean_object* l_Lean_Parser_Term_typeAscription___elambda__1___closed__2;
lean_object* l_PersistentHashMap_findAtAux___main___at_Lean_Elab_Term_elabTermAux___main___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -208,6 +213,7 @@ size_t l_USize_shiftRight(size_t, size_t);
lean_object* l___private_Init_Lean_Elab_Term_5__expandCDot___main___closed__2;
lean_object* l_Lean_Elab_Term_withLCtx___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_synthesizeInst(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__3;
lean_object* l_Lean_Elab_Term_elabArrayLit___closed__6;
lean_object* l_Lean_Elab_Term_monadLog___closed__10;
lean_object* l_Lean_Elab_Term_resolveName___closed__6;
@ -263,6 +269,7 @@ lean_object* l_Lean_Elab_Term_elabArrayLit(lean_object*, lean_object*, lean_obje
lean_object* l_Lean_Elab_Term_getOptions(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_monadLog___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabParen___closed__1;
lean_object* l_Lean_Elab_Term_addDecl(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabListLit___closed__1;
extern lean_object* l_Lean_mkTermIdFromIdent___closed__2;
extern lean_object* l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
@ -270,11 +277,13 @@ lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_Term_elabParen___spec__
lean_object* l_Lean_Elab_Term_liftMetaM(lean_object*);
uint8_t l___private_Init_Lean_Elab_Term_11__isExplicit___closed__1;
extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__1;
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabByTactic___closed__2;
uint8_t lean_metavar_ctx_is_expr_assigned(lean_object*, lean_object*);
lean_object* l_Lean_Meta_isClass(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_SMap_contains___at_Lean_Elab_Term_addBuiltinTermElab___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_withTransparency(lean_object*);
lean_object* l_HashMapImp_find_x3f___at_Lean_Elab_Term_elabTermAux___main___spec__5___boxed(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_byTactic___elambda__1___closed__2;
lean_object* l_Lean_Elab_Term_withIncRecDepth___rarg___closed__1;
lean_object* l_Lean_Elab_Term_elabListLit___closed__2;
lean_object* l_Lean_Elab_Term_Lean_Elab_MonadMacroAdapter___lambda__2(lean_object*, lean_object*, lean_object*);
@ -291,6 +300,7 @@ lean_object* l_Lean_Elab_Term_tryCoe(lean_object*, lean_object*, lean_object*, l
lean_object* l___private_Init_Lean_Elab_Term_10__elabTermUsing___main___closed__3;
lean_object* l_Lean_Elab_Term_tryPostponeIfNoneOrMVar(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Term_2__fromMetaException___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabByTactic___closed__1;
lean_object* l_Lean_Elab_Term_elabParen___closed__4;
lean_object* l_Lean_Elab_Term_withIncRecDepth___rarg___closed__2;
lean_object* l_Lean_Elab_Term_elabLevel(lean_object*, lean_object*, lean_object*);
@ -313,6 +323,7 @@ lean_object* l___private_Init_Lean_Elab_Term_17__resolveLocalName(lean_object*,
lean_object* l_Lean_Elab_Term_termElabAttribute___closed__4;
lean_object* l_Lean_Elab_Term_addContext___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_levelMVarToParam(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabByTactic(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_observing(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_mkLet___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_withoutMacroStackAtErr(lean_object*);
@ -351,8 +362,10 @@ lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___closed__3;
lean_object* l_Lean_Elab_mkMessageCore(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
extern lean_object* l_Lean_Parser_Term_quotedName___elambda__1___closed__2;
lean_object* l_Lean_Elab_Term_withMacroExpansion___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabByTactic___closed__2;
lean_object* l_Lean_Elab_Term_mkExplicitBinder___closed__3;
lean_object* l___private_Init_Lean_Elab_Term_10__elabTermUsing(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_KernelException_toMessageData(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_levelMVarToParam___closed__2;
lean_object* l_Lean_Elab_Term_elabStr___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabParen(lean_object*);
@ -360,6 +373,7 @@ lean_object* l_Lean_Elab_Term_mkConst___closed__2;
lean_object* l_Lean_Elab_Term_isType(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___closed__2;
lean_object* l_List_foldlM___main___at___private_Init_Lean_Elab_Term_19__mkConsts___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_setEnv___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabQuotedName(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_TermElabM_inhabited(lean_object*, lean_object*);
@ -392,6 +406,7 @@ lean_object* l_Lean_Elab_Term_monadLog___closed__6;
extern lean_object* l_Lean_strLitKind___closed__2;
lean_object* l_Lean_Elab_Term_withFreshMacroScope(lean_object*);
lean_object* l_Lean_Elab_Term_resolveName___closed__7;
lean_object* l_Lean_Elab_Term_addDecl___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
size_t l_Lean_Name_hash(lean_object*);
lean_object* l_Lean_Elab_Term_elabTermAux___main(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_termElabAttribute___closed__3;
@ -668,6 +683,7 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabParen___closed__2;
lean_object* l_Lean_Elab_Term_resettingSynthInstanceCacheWhen___rarg(uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_logAt___at_Lean_Elab_Term_logTrace___spec__2(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Term_8__exceptionToSorry___closed__3;
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabByTactic(lean_object*);
lean_object* l___private_Init_Lean_Elab_Term_14__mkPairsAux___main___closed__8;
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabQuotedName___closed__1;
lean_object* l___private_Init_Lean_Elab_Term_3__fromMetaState___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -740,6 +756,7 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabStr(lean_object*);
lean_object* l_Lean_Elab_Term_elabImplicitLambda___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
lean_object* l_Lean_PersistentEnvExtension_getState___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabByTactic___closed__3;
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabHole___closed__3;
lean_object* l_Lean_Elab_Term_withLetDecl___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabTacticBlock___closed__2;
@ -767,6 +784,7 @@ lean_object* l_Lean_Elab_Term_decLevel___boxed(lean_object*, lean_object*, lean_
lean_object* l_Lean_Elab_Term_getLCtx___boxed(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Term_13__tryCoeSort(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_mkFreshLevelMVar___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabByTactic___closed__1;
lean_object* l_Lean_Elab_Term_ppGoal(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_setTraceState(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_tryPostpone(lean_object*, lean_object*);
@ -775,6 +793,7 @@ lean_object* l_Lean_Elab_Term_monadLog___lambda__3(lean_object*, lean_object*, l
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Term_3__fromMetaState___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_monadQuotation___closed__3;
lean_object* l_Lean_Elab_Term_tryCoeAndLift___closed__3;
lean_object* l_Lean_Elab_Term_setEnv(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkFreshLevelMVar___rarg(lean_object*);
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
extern lean_object* l_Lean_MetavarContext_Inhabited___closed__1;
@ -795,6 +814,7 @@ uint8_t l_Lean_LocalInstance_beq(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_registerBuiltinTermElabAttr___closed__4;
lean_object* l___private_Init_Lean_Elab_Term_5__expandCDot___main___closed__4;
lean_object* l_Lean_Elab_Term_tryCoeAndLift___closed__1;
lean_object* lean_compile_decl(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_resettingSynthInstanceCache___rarg___closed__1;
lean_object* l_Lean_Elab_Term_elabRawCharLit___closed__1;
lean_object* l_Lean_MetavarContext_getDecl(lean_object*, lean_object*);
@ -817,7 +837,6 @@ lean_object* l_Array_iterateMAux___main___at_Lean_mkAppN___spec__1(lean_object*,
lean_object* l_Lean_Elab_Term_getMCtx___boxed(lean_object*);
lean_object* l_Lean_Elab_Term_applyResult(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__1;
lean_object* l_Lean_Meta_isTypeFormer(lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabHole___closed__1;
lean_object* l_Lean_SMap_empty___at_Lean_Elab_Term_mkBuiltinTermElabTable___spec__1;
@ -845,7 +864,6 @@ lean_object* l_Lean_Elab_Term_registerBuiltinTermElabAttr___closed__1;
lean_object* l_Lean_Elab_Term_resolveName___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_resolveName___closed__1;
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabHole___closed__2;
lean_object* l_IO_ofExcept___at___private_Init_Lean_Elab_Util_6__ElabAttribute_add___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_resettingSynthInstanceCache(lean_object*);
lean_object* l___private_Init_Lean_Elab_Term_13__tryCoeSort___closed__7;
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
@ -906,7 +924,7 @@ uint8_t lean_string_dec_eq(lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Lean_Elab_MonadMacroAdapter___closed__6;
lean_object* l_Lean_Elab_Term_decLevel___closed__6;
extern lean_object* l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__3;
lean_object* lean_add_decl(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_tryCoe___closed__3;
lean_object* _init_l_Lean_Elab_Term_State_inhabited___closed__1() {
_start:
@ -1379,6 +1397,130 @@ lean_dec(x_1);
return x_3;
}
}
lean_object* l_Lean_Elab_Term_setEnv(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4;
x_4 = !lean_is_exclusive(x_3);
if (x_4 == 0)
{
lean_object* x_5; uint8_t x_6;
x_5 = lean_ctor_get(x_3, 0);
x_6 = !lean_is_exclusive(x_5);
if (x_6 == 0)
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_ctor_get(x_5, 0);
lean_dec(x_7);
lean_ctor_set(x_5, 0, x_1);
x_8 = lean_box(0);
x_9 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_9, 0, x_8);
lean_ctor_set(x_9, 1, x_3);
return x_9;
}
else
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_10 = lean_ctor_get(x_5, 1);
x_11 = lean_ctor_get(x_5, 2);
x_12 = lean_ctor_get(x_5, 3);
x_13 = lean_ctor_get(x_5, 4);
x_14 = lean_ctor_get(x_5, 5);
lean_inc(x_14);
lean_inc(x_13);
lean_inc(x_12);
lean_inc(x_11);
lean_inc(x_10);
lean_dec(x_5);
x_15 = lean_alloc_ctor(0, 6, 0);
lean_ctor_set(x_15, 0, x_1);
lean_ctor_set(x_15, 1, x_10);
lean_ctor_set(x_15, 2, x_11);
lean_ctor_set(x_15, 3, x_12);
lean_ctor_set(x_15, 4, x_13);
lean_ctor_set(x_15, 5, x_14);
lean_ctor_set(x_3, 0, x_15);
x_16 = lean_box(0);
x_17 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set(x_17, 1, x_3);
return x_17;
}
}
else
{
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33;
x_18 = lean_ctor_get(x_3, 0);
x_19 = lean_ctor_get(x_3, 1);
x_20 = lean_ctor_get(x_3, 2);
x_21 = lean_ctor_get(x_3, 3);
x_22 = lean_ctor_get(x_3, 4);
x_23 = lean_ctor_get(x_3, 5);
lean_inc(x_23);
lean_inc(x_22);
lean_inc(x_21);
lean_inc(x_20);
lean_inc(x_19);
lean_inc(x_18);
lean_dec(x_3);
x_24 = lean_ctor_get(x_18, 1);
lean_inc(x_24);
x_25 = lean_ctor_get(x_18, 2);
lean_inc(x_25);
x_26 = lean_ctor_get(x_18, 3);
lean_inc(x_26);
x_27 = lean_ctor_get(x_18, 4);
lean_inc(x_27);
x_28 = lean_ctor_get(x_18, 5);
lean_inc(x_28);
if (lean_is_exclusive(x_18)) {
lean_ctor_release(x_18, 0);
lean_ctor_release(x_18, 1);
lean_ctor_release(x_18, 2);
lean_ctor_release(x_18, 3);
lean_ctor_release(x_18, 4);
lean_ctor_release(x_18, 5);
x_29 = x_18;
} else {
lean_dec_ref(x_18);
x_29 = lean_box(0);
}
if (lean_is_scalar(x_29)) {
x_30 = lean_alloc_ctor(0, 6, 0);
} else {
x_30 = x_29;
}
lean_ctor_set(x_30, 0, x_1);
lean_ctor_set(x_30, 1, x_24);
lean_ctor_set(x_30, 2, x_25);
lean_ctor_set(x_30, 3, x_26);
lean_ctor_set(x_30, 4, x_27);
lean_ctor_set(x_30, 5, x_28);
x_31 = lean_alloc_ctor(0, 6, 0);
lean_ctor_set(x_31, 0, x_30);
lean_ctor_set(x_31, 1, x_19);
lean_ctor_set(x_31, 2, x_20);
lean_ctor_set(x_31, 3, x_21);
lean_ctor_set(x_31, 4, x_22);
lean_ctor_set(x_31, 5, x_23);
x_32 = lean_box(0);
x_33 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_33, 0, x_32);
lean_ctor_set(x_33, 1, x_31);
return x_33;
}
}
}
lean_object* l_Lean_Elab_Term_setEnv___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Lean_Elab_Term_setEnv(x_1, x_2, x_3);
lean_dec(x_2);
return x_4;
}
}
lean_object* l_Lean_Elab_Term_addContext(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -3291,7 +3433,7 @@ lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_8 = l_Lean_mkAppStx___closed__6;
lean_inc(x_1);
x_9 = l_Lean_Elab_syntaxNodeKindOfAttrParam(x_1, x_8, x_3);
x_10 = l_IO_ofExcept___at___private_Init_Lean_Elab_Util_6__ElabAttribute_add___spec__1(x_9, x_5);
x_10 = l_IO_ofExcept___at___private_Init_Lean_Elab_Util_7__ElabAttribute_add___spec__1(x_9, x_5);
lean_dec(x_9);
if (lean_obj_tag(x_10) == 0)
{
@ -16571,7 +16713,7 @@ lean_object* _init_l___private_Init_Lean_Elab_Term_9__postponeElabTerm___closed_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__1;
x_1 = l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__1;
x_2 = l___private_Init_Lean_Elab_Term_9__postponeElabTerm___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -17507,7 +17649,7 @@ lean_inc(x_105);
x_106 = lean_ctor_get(x_104, 1);
lean_inc(x_106);
lean_dec(x_104);
x_107 = l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__3;
x_107 = l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__3;
x_108 = l_Lean_checkTraceOption(x_105, x_107);
lean_dec(x_105);
if (x_108 == 0)
@ -17889,7 +18031,7 @@ lean_inc(x_196);
x_197 = lean_ctor_get(x_195, 1);
lean_inc(x_197);
lean_dec(x_195);
x_198 = l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__3;
x_198 = l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__3;
x_199 = l_Lean_checkTraceOption(x_196, x_198);
lean_dec(x_196);
if (x_199 == 0)
@ -18370,7 +18512,7 @@ lean_inc(x_312);
x_313 = lean_ctor_get(x_311, 1);
lean_inc(x_313);
lean_dec(x_311);
x_314 = l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__3;
x_314 = l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__3;
x_315 = l_Lean_checkTraceOption(x_312, x_314);
lean_dec(x_312);
if (x_315 == 0)
@ -18892,7 +19034,7 @@ lean_inc(x_438);
x_439 = lean_ctor_get(x_437, 1);
lean_inc(x_439);
lean_dec(x_437);
x_440 = l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__3;
x_440 = l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__3;
x_441 = l_Lean_checkTraceOption(x_438, x_440);
lean_dec(x_438);
if (x_441 == 0)
@ -19708,7 +19850,7 @@ lean_object* _init_l_Lean_Elab_Term_elabImplicitLambdaAux___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__1;
x_1 = l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__1;
x_2 = l_Lean_Elab_Term_elabImplicitLambdaAux___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -23717,6 +23859,105 @@ return x_17;
}
}
}
lean_object* l_Lean_Elab_Term_addDecl(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_5 = l_Lean_Elab_Term_getEnv___rarg(x_4);
x_6 = lean_ctor_get(x_5, 0);
lean_inc(x_6);
x_7 = lean_ctor_get(x_5, 1);
lean_inc(x_7);
lean_dec(x_5);
x_8 = lean_add_decl(x_6, x_2);
if (lean_obj_tag(x_8) == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_9 = lean_ctor_get(x_8, 0);
lean_inc(x_9);
lean_dec(x_8);
x_10 = l_Lean_Elab_Term_getOptions(x_3, x_7);
x_11 = lean_ctor_get(x_10, 0);
lean_inc(x_11);
x_12 = lean_ctor_get(x_10, 1);
lean_inc(x_12);
lean_dec(x_10);
x_13 = l_Lean_KernelException_toMessageData(x_9, x_11);
x_14 = l_Lean_Elab_Term_throwError___rarg(x_1, x_13, x_3, x_12);
return x_14;
}
else
{
lean_object* x_15; lean_object* x_16;
x_15 = lean_ctor_get(x_8, 0);
lean_inc(x_15);
lean_dec(x_8);
x_16 = l_Lean_Elab_Term_setEnv(x_15, x_3, x_7);
lean_dec(x_3);
return x_16;
}
}
}
lean_object* l_Lean_Elab_Term_addDecl___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_Lean_Elab_Term_addDecl(x_1, x_2, x_3, x_4);
lean_dec(x_2);
lean_dec(x_1);
return x_5;
}
}
lean_object* l_Lean_Elab_Term_compileDecl(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_5 = l_Lean_Elab_Term_getEnv___rarg(x_4);
x_6 = lean_ctor_get(x_5, 0);
lean_inc(x_6);
x_7 = lean_ctor_get(x_5, 1);
lean_inc(x_7);
lean_dec(x_5);
x_8 = l_Lean_Elab_Term_getOptions(x_3, x_7);
x_9 = lean_ctor_get(x_8, 0);
lean_inc(x_9);
x_10 = lean_ctor_get(x_8, 1);
lean_inc(x_10);
lean_dec(x_8);
x_11 = lean_compile_decl(x_6, x_9, x_2);
if (lean_obj_tag(x_11) == 0)
{
lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_12 = lean_ctor_get(x_11, 0);
lean_inc(x_12);
lean_dec(x_11);
x_13 = l_Lean_KernelException_toMessageData(x_12, x_9);
x_14 = l_Lean_Elab_Term_throwError___rarg(x_1, x_13, x_3, x_10);
return x_14;
}
else
{
lean_object* x_15; lean_object* x_16;
lean_dec(x_9);
x_15 = lean_ctor_get(x_11, 0);
lean_inc(x_15);
lean_dec(x_11);
x_16 = l_Lean_Elab_Term_setEnv(x_15, x_3, x_10);
lean_dec(x_3);
return x_16;
}
}
}
lean_object* l_Lean_Elab_Term_compileDecl___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_Lean_Elab_Term_compileDecl(x_1, x_2, x_3, x_4);
lean_dec(x_2);
lean_dec(x_1);
return x_5;
}
}
lean_object* l_Lean_Elab_Term_elabProp___rarg(lean_object* x_1) {
_start:
{
@ -24189,6 +24430,95 @@ x_5 = l_Lean_Elab_Term_addBuiltinTermElab(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* _init_l_Lean_Elab_Term_elabByTactic___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("invalid 'by' tactic, expected type has not been provided");
return x_1;
}
}
lean_object* _init_l_Lean_Elab_Term_elabByTactic___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_elabByTactic___closed__1;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Elab_Term_elabByTactic___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_elabByTactic___closed__2;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* l_Lean_Elab_Term_elabByTactic(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_5; lean_object* x_6;
x_5 = l_Lean_Elab_Term_elabByTactic___closed__3;
x_6 = l_Lean_Elab_Term_throwError___rarg(x_1, x_5, x_3, x_4);
lean_dec(x_1);
return x_6;
}
else
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_7 = lean_ctor_get(x_2, 0);
lean_inc(x_7);
lean_dec(x_2);
x_8 = lean_unsigned_to_nat(1u);
x_9 = l_Lean_Syntax_getArg(x_1, x_8);
x_10 = l_Lean_Elab_Term_mkTacticMVar(x_1, x_7, x_9, x_3, x_4);
return x_10;
}
}
}
lean_object* _init_l___regBuiltinTermElab_Lean_Elab_Term_elabByTactic___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("elabByTactic");
return x_1;
}
}
lean_object* _init_l___regBuiltinTermElab_Lean_Elab_Term_elabByTactic___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Term_declareBuiltinTermElab___closed__3;
x_2 = l___regBuiltinTermElab_Lean_Elab_Term_elabByTactic___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l___regBuiltinTermElab_Lean_Elab_Term_elabByTactic___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabByTactic), 4, 0);
return x_1;
}
}
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabByTactic(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_Parser_Term_byTactic___elambda__1___closed__2;
x_3 = l___regBuiltinTermElab_Lean_Elab_Term_elabByTactic___closed__2;
x_4 = l___regBuiltinTermElab_Lean_Elab_Term_elabByTactic___closed__3;
x_5 = l_Lean_Elab_Term_addBuiltinTermElab(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* _init_l___private_Init_Lean_Elab_Term_14__mkPairsAux___main___closed__1() {
_start:
{
@ -28335,6 +28665,21 @@ lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_elabTacticBlock___clo
res = l___regBuiltinTermElab_Lean_Elab_Term_elabTacticBlock(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_Term_elabByTactic___closed__1 = _init_l_Lean_Elab_Term_elabByTactic___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_elabByTactic___closed__1);
l_Lean_Elab_Term_elabByTactic___closed__2 = _init_l_Lean_Elab_Term_elabByTactic___closed__2();
lean_mark_persistent(l_Lean_Elab_Term_elabByTactic___closed__2);
l_Lean_Elab_Term_elabByTactic___closed__3 = _init_l_Lean_Elab_Term_elabByTactic___closed__3();
lean_mark_persistent(l_Lean_Elab_Term_elabByTactic___closed__3);
l___regBuiltinTermElab_Lean_Elab_Term_elabByTactic___closed__1 = _init_l___regBuiltinTermElab_Lean_Elab_Term_elabByTactic___closed__1();
lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_elabByTactic___closed__1);
l___regBuiltinTermElab_Lean_Elab_Term_elabByTactic___closed__2 = _init_l___regBuiltinTermElab_Lean_Elab_Term_elabByTactic___closed__2();
lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_elabByTactic___closed__2);
l___regBuiltinTermElab_Lean_Elab_Term_elabByTactic___closed__3 = _init_l___regBuiltinTermElab_Lean_Elab_Term_elabByTactic___closed__3();
lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_elabByTactic___closed__3);
res = l___regBuiltinTermElab_Lean_Elab_Term_elabByTactic(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___private_Init_Lean_Elab_Term_14__mkPairsAux___main___closed__1 = _init_l___private_Init_Lean_Elab_Term_14__mkPairsAux___main___closed__1();
lean_mark_persistent(l___private_Init_Lean_Elab_Term_14__mkPairsAux___main___closed__1);
l___private_Init_Lean_Elab_Term_14__mkPairsAux___main___closed__2 = _init_l___private_Init_Lean_Elab_Term_14__mkPairsAux___main___closed__2();

196
stage0/stdlib/Init/Lean/Elab/Util.c
View file

@ -21,7 +21,6 @@ size_t l_USize_add(size_t, size_t);
lean_object* l_AssocList_replace___main___at_Lean_Elab_ElabFnTable_insert___spec__30(lean_object*);
lean_object* l_AssocList_foldlM___main___at_Lean_Elab_ElabFnTable_insert___spec__29(lean_object*);
lean_object* l_Lean_registerTraceClass(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_6__ElabAttribute_add___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Environment_8__persistentEnvExtensionsRef;
lean_object* l_AssocList_contains___main___at_Lean_Elab_ElabFnTable_insert___spec__26___rarg___boxed(lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Parser_Parser_27__BuiltinParserAttribute_add___closed__2;
@ -34,6 +33,7 @@ lean_object* l_Lean_Elab_macroAttribute___closed__2;
lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MacroScopesView_format___boxed(lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_ElabFnTable_insert___spec__24___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_IO_ofExcept___at___private_Init_Lean_Elab_Util_7__ElabAttribute_add___spec__1(lean_object*, lean_object*);
lean_object* l_String_toFormat(lean_object*);
extern lean_object* l_Lean_MessageData_ofList___closed__3;
lean_object* l_PersistentHashMap_insertAux___main___at_Lean_Elab_ElabFnTable_insert___spec__22(lean_object*);
@ -53,7 +53,6 @@ uint8_t l_AssocList_contains___main___at_Lean_Elab_ElabFnTable_insert___spec__26
lean_object* l_Lean_MacroScopesView_format(lean_object*, lean_object*);
size_t l_USize_sub(size_t, size_t);
lean_object* l_HashMapImp_insert___at_Lean_Elab_ElabFnTable_insert___spec__25(lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Array_empty___closed__1;
lean_object* lean_environment_find(lean_object*, lean_object*);
lean_object* l_HashMapImp_insert___at_Lean_Elab_ElabFnTable_insert___spec__14___rarg(lean_object*, lean_object*, lean_object*);
@ -66,15 +65,14 @@ lean_object* l_HashMapImp_moveEntries___main___at_Lean_Elab_ElabFnTable_insert__
lean_object* l_Lean_Elab_liftMacroM___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_io_ref_get(lean_object*, lean_object*);
lean_object* l_PersistentHashMap_find_x3f___at_Lean_Elab_ElabFnTable_insert___spec__2(lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_8__regTraceClasses(lean_object*);
lean_object* lean_get_namespaces(lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_9__regTraceClasses(lean_object*);
lean_object* l_HashMapImp_find_x3f___at_Lean_Elab_ElabFnTable_insert___spec__7(lean_object*);
lean_object* l_Lean_Syntax_reprint___main(lean_object*);
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
lean_object* l_List_find_x3f___main___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_registerBuiltinMacroAttr___lambda__1___closed__2;
lean_object* l___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers(lean_object*);
lean_object* lean_string_append(lean_object*, lean_object*);
lean_object* l_AssocList_find___main___at_Lean_Elab_ElabFnTable_insert___spec__6___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -85,15 +83,17 @@ extern lean_object* l_String_splitAux___main___closed__1;
lean_object* l_PersistentHashMap_find_x3f___at_Lean_Elab_ElabFnTable_insert___spec__2___rarg___boxed(lean_object*, lean_object*);
lean_object* l_PersistentHashMap_insertAux___main___at_Lean_Elab_ElabFnTable_insert___spec__11(lean_object*);
lean_object* l_Lean_Elab_mkElabAttributeAux___rarg___closed__3;
lean_object* l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__1;
lean_object* l___private_Init_Lean_Elab_Util_2__throwUnexpectedElabType___rarg(lean_object*, lean_object*);
size_t l_USize_shiftRight(size_t, size_t);
lean_object* l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__3;
lean_object* l_Lean_SMap_insert___at_Lean_Elab_ElabFnTable_insert___spec__20(lean_object*);
lean_object* l_IO_ofExcept___at___private_Init_Lean_Elab_Util_7__ElabAttribute_add___spec__1___boxed(lean_object*, lean_object*);
extern lean_object* l_Lean_mkAttributeImplOfConstantUnsafe___closed__3;
lean_object* l_AssocList_replace___main___at_Lean_Elab_ElabFnTable_insert___spec__19(lean_object*);
lean_object* l_PersistentHashMap_findAtAux___main___at_Lean_Elab_getMacros___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_LocalContext_Inhabited___closed__1;
lean_object* l_Lean_Syntax_truncateTrailing(lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__2;
lean_object* l_Lean_Elab_macroAttribute___closed__3;
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_ElabFnTable_insert___spec__24___rarg(size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_AttributeImpl_inhabited___closed__2;
@ -102,26 +102,29 @@ lean_object* l_Lean_Elab_checkSyntaxNodeKindAtNamespaces___main(lean_object*, le
lean_object* l_Lean_SMap_empty___at_Lean_Elab_mkElabAttributeAux___spec__4___closed__2;
lean_object* l_Lean_Elab_registerBuiltinMacroAttr___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_AssocList_foldlM___main___at_Lean_Elab_ElabFnTable_insert___spec__29___rarg(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_8__expandMacroFns___main(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_HashMapImp_insert___at_Lean_Elab_ElabFnTable_insert___spec__14(lean_object*);
lean_object* l_Lean_Elab_mkElabAttributeAux___rarg___lambda__1(lean_object*);
lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_Elab_mkElabAttributeAux___spec__3___rarg___closed__3;
lean_object* l_IO_ofExcept___at___private_Init_Lean_Elab_Util_6__ElabAttribute_add___spec__1___boxed(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_6__ElabAttribute_addExtensionEntry(lean_object*);
lean_object* l_Lean_Elab_addBuiltinMacro(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_ElabAttribute_inhabited___closed__6;
lean_object* l_List_foldl___main___at_Lean_Elab_addMacroStack___spec__1___closed__1;
extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__1;
lean_object* l_Lean_Elab_evalSyntaxConstant___closed__1;
extern lean_object* l_Lean_mkAttributeImplOfConstant___closed__1;
lean_object* l___private_Init_Lean_Elab_Util_5__ElabAttribute_addImportedParsers___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_7__ElabAttribute_add___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_macroAttribute___closed__5;
lean_object* l_Lean_Elab_checkSyntaxNodeKind___closed__2;
lean_object* l___private_Init_Lean_Elab_Util_3__mkElabFnOfConstantUnsafe___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_ElabAttribute_inhabited___closed__5;
lean_object* l___private_Init_Lean_Elab_Util_5__ElabAttribute_addExtensionEntry(lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_7__ElabAttribute_add(lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_4__evalConstant(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_Elab_checkSyntaxNodeKindAtNamespaces(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_SMap_empty___at_Lean_Elab_ElabAttributeExtensionState_inhabited___spec__1(lean_object*);
lean_object* l_Lean_Elab_declareBuiltinMacro___closed__7;
lean_object* l___private_Init_Lean_Elab_Util_6__ElabAttribute_add(lean_object*);
uint8_t l_Lean_Elab_getBetterRef___lambda__1(lean_object*, lean_object*);
lean_object* l_PersistentHashMap_empty___at_Lean_Elab_ElabAttributeExtensionState_inhabited___spec__3(lean_object*);
extern lean_object* l_Lean_EnvExtension_Inhabited___rarg___closed__1;
@ -132,7 +135,6 @@ lean_object* l_Lean_SMap_empty___at_Lean_Elab_mkElabAttributeAux___spec__4___clo
lean_object* l_HashMapImp_expand___at_Lean_Elab_ElabFnTable_insert___spec__16(lean_object*);
lean_object* l_Lean_SMap_find_x3f___at_Lean_Elab_getMacros___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Elab_syntaxNodeKindOfAttrParam___closed__2;
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___spec__1(lean_object*);
lean_object* l_HashMapImp_expand___at_Lean_Elab_ElabFnTable_insert___spec__16___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_registerBuiltinMacroAttr___lambda__1___closed__1;
lean_object* l_Lean_Name_append___main(lean_object*, lean_object*);
@ -144,22 +146,23 @@ lean_object* l_Lean_Elab_ElabAttributeExtensionState_inhabited___closed__1;
lean_object* l_Lean_Elab_liftMacroM___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_checkSyntaxNodeKindAtNamespaces___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_Elab_mkElabAttributeAux___spec__3(lean_object*);
extern lean_object* l_Lean_Parser_Syntax_paren___elambda__1___closed__1;
lean_object* l_PersistentHashMap_find_x3f___at_Lean_Elab_getMacros___spec__2___boxed(lean_object*, lean_object*);
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
uint8_t l_AssocList_contains___main___at_Lean_Elab_ElabFnTable_insert___spec__15___rarg(lean_object*, lean_object*);
lean_object* l_List_foldl___main___at_Lean_Elab_addMacroStack___spec__1___closed__3;
lean_object* l_PersistentHashMap_insertAux___main___at_Lean_Elab_ElabFnTable_insert___spec__22___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_HashMapImp_find_x3f___at_Lean_Elab_getMacros___spec__5___boxed(lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_5__ElabAttribute_addImportedParsers___spec__2(lean_object*);
lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
lean_object* l_List_lengthAux___main___rarg(lean_object*, lean_object*);
lean_object* l_Lean_SMap_find_x3f___at_Lean_Elab_ElabFnTable_insert___spec__1___rarg___boxed(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_4__evalConstant___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_HashMapImp_find_x3f___at_Lean_Elab_ElabFnTable_insert___spec__5___rarg(lean_object*, lean_object*);
lean_object* l_PersistentHashMap_find_x3f___at_Lean_Elab_ElabFnTable_insert___spec__2___rarg(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_3__mkElabFnOfConstantUnsafe(lean_object*);
lean_object* l_Lean_Elab_registerBuiltinMacroAttr(lean_object*);
size_t l_Lean_Name_hash(lean_object*);
lean_object* l_Nat_repr(lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Char_HasRepr___closed__1;
lean_object* l_Lean_Elab_registerBuiltinMacroAttr___lambda__1___closed__4;
lean_object* l_Lean_Elab_getMacros(lean_object*, lean_object*, lean_object*, lean_object*);
@ -171,8 +174,10 @@ lean_object* l_AssocList_find___main___at_Lean_Elab_ElabFnTable_insert___spec__6
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_SMap_empty___at_Lean_Elab_mkElabAttributeAux___spec__4___closed__3;
lean_object* l_PersistentHashMap_findAtAux___main___at_Lean_Elab_getMacros___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__2;
lean_object* l_Lean_Elab_mkElabAttributeAux___rarg___lambda__2(lean_object*);
lean_object* l_List_foldl___main___at_Lean_Elab_addMacroStack___spec__1___closed__2;
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_5__ElabAttribute_addImportedParsers___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_eval_const(lean_object*, lean_object*);
lean_object* l_Lean_Elab_registerBuiltinMacroAttr___lambda__1___closed__3;
lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_Elab_mkElabAttributeAux___spec__3___rarg___closed__2;
@ -192,7 +197,6 @@ lean_object* l_AssocList_contains___main___at_Lean_Elab_ElabFnTable_insert___spe
lean_object* l_PersistentHashMap_insert___at_Lean_Elab_ElabFnTable_insert___spec__21(lean_object*);
size_t lean_usize_modn(size_t, lean_object*);
extern lean_object* l___private_Init_Lean_Environment_5__envExtensionsRef;
lean_object* l_Lean_Elab_mkElabFnOfConstant(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_registerBuiltinAttribute(lean_object*, lean_object*);
lean_object* l_mkHashMap___at_Lean_Elab_ElabAttribute_inhabited___spec__2(lean_object*);
lean_object* l_mkHashMap___at_Lean_Elab_mkElabAttributeAux___spec__5(lean_object*);
@ -205,12 +209,13 @@ lean_object* l_List_redLength___main___rarg(lean_object*);
lean_object* l_Lean_Elab_liftMacroM(lean_object*, lean_object*);
lean_object* l_Lean_Elab_addMacroStack___closed__1;
lean_object* l_mkHashMapImp___rarg(lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_6__ElabAttribute_addExtensionEntry___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_syntaxNodeKindOfAttrParam___closed__3;
lean_object* l_mkHashMap___at_Lean_Elab_ElabAttributeExtensionState_inhabited___spec__2(lean_object*);
lean_object* l_Lean_Elab_getBetterRef___lambda__1___boxed(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_5__ElabAttribute_addExtensionEntry___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_ElabFnTable_insert(lean_object*);
lean_object* l_AssocList_find___main___at_Lean_Elab_ElabFnTable_insert___spec__8(lean_object*);
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_5__ElabAttribute_addImportedParsers___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_declareBuiltinMacro(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__3;
lean_object* l_Lean_ConstantInfo_type(lean_object*);
@ -231,8 +236,8 @@ lean_object* l_Lean_Elab_mkElabAttributeAux___rarg___lambda__2___boxed(lean_obje
lean_object* l_Lean_Elab_declareBuiltinMacro___closed__4;
lean_object* l_Lean_SMap_find_x3f___at_Lean_Elab_ElabFnTable_insert___spec__1___rarg(lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_mkElabAttributeAux___rarg___closed__2;
lean_object* l___private_Init_Lean_Elab_Util_3__evalConstantUnsafe___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_2__throwUnexpectedElabType___rarg___closed__2;
lean_object* l_Lean_Elab_syntaxNodeKindOfAttrParam___closed__1;
lean_object* l___private_Init_Lean_Elab_Util_1__ElabAttribute_mkInitial(lean_object*);
@ -240,6 +245,7 @@ lean_object* l_Lean_Elab_registerBuiltinMacroAttr___closed__1;
lean_object* l_AssocList_find___main___at_Lean_Elab_ElabFnTable_insert___spec__8___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_syntaxNodeKindOfAttrParam___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_5__ElabAttribute_addImportedParsers___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_PersistentHashMap_find_x3f___at_Lean_Elab_getMacros___spec__2(lean_object*, lean_object*);
lean_object* l_Lean_Elab_registerBuiltinMacroAttr___closed__2;
lean_object* l_Lean_Elab_getMacros___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -247,9 +253,7 @@ lean_object* l_PersistentHashMap_insertAux___main___at_Lean_Elab_ElabFnTable_ins
lean_object* l_Lean_Elab_ElabAttribute_inhabited___closed__3;
lean_object* l_Lean_Elab_macroAttribute;
lean_object* lean_environment_main_module(lean_object*);
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___spec__2(lean_object*);
extern lean_object* l_Lean_registerSimplePersistentEnvExtension___rarg___lambda__4___closed__2;
lean_object* l___private_Init_Lean_Elab_Util_6__ElabAttribute_add___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
lean_object* l_HashMapImp_find_x3f___at_Lean_Elab_ElabFnTable_insert___spec__7___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_checkSyntaxNodeKind___closed__1;
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
@ -257,8 +261,6 @@ uint8_t l_USize_decLe(size_t, size_t);
lean_object* l_HashMapImp_insert___at_Lean_Elab_ElabFnTable_insert___spec__25___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_mkElabAttribute(lean_object*);
lean_object* l_AssocList_foldlM___main___at_Lean_Elab_ElabFnTable_insert___spec__18___rarg(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_7__expandMacroFns___main(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_nameToExprAux___main(lean_object*);
lean_object* l_Lean_SMap_empty___at_Lean_Elab_mkBuiltinMacroFnTable___spec__1___closed__2;
lean_object* l_Lean_Environment_addAndCompile(lean_object*, lean_object*, lean_object*);
@ -279,6 +281,7 @@ lean_object* l_Lean_Elab_declareBuiltinMacro___closed__2;
lean_object* l_HashMapImp_find_x3f___at_Lean_Elab_ElabFnTable_insert___spec__5___rarg___boxed(lean_object*, lean_object*);
lean_object* l_HashMapImp_find_x3f___at_Lean_Elab_ElabFnTable_insert___spec__5(lean_object*);
lean_object* l_Lean_SMap_empty___at_Lean_Elab_ElabAttributeExtensionState_inhabited___spec__1___closed__3;
lean_object* l_Lean_Elab_evalSyntaxConstant(lean_object*, lean_object*);
lean_object* l_Lean_Elab_ElabAttribute_inhabited___closed__1;
lean_object* l_PersistentHashMap_findAtAux___main___at_Lean_Elab_ElabFnTable_insert___spec__4___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_ElabAttribute_inhabited___closed__2;
@ -295,6 +298,7 @@ lean_object* l_Lean_Elab_declareBuiltinMacro___closed__1;
extern lean_object* l_Lean_mkAppStx___closed__9;
lean_object* l_AssocList_contains___main___at_Lean_Elab_ElabFnTable_insert___spec__15___rarg___boxed(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_1__ElabAttribute_mkInitial___rarg(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_5__ElabAttribute_addImportedParsers(lean_object*);
lean_object* lean_io_ref_set(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_SMap_insert___at_Lean_Elab_ElabFnTable_insert___spec__9(lean_object*);
lean_object* l_PersistentHashMap_getCollisionNodeSize___rarg(lean_object*);
@ -319,6 +323,7 @@ lean_object* l_List_foldl___main___at_Lean_MacroScopesView_review___spec__1(lean
lean_object* l_Lean_SMap_insert___at_Lean_Elab_ElabFnTable_insert___spec__9___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_checkSyntaxNodeKind(lean_object*, lean_object*);
lean_object* l_AssocList_find___main___at_Lean_Elab_ElabFnTable_insert___spec__8___rarg___boxed(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_7__ElabAttribute_add___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
lean_object* l_mkHashMap___at_Lean_Elab_ElabAttribute_inhabited___spec__2___rarg(lean_object*);
lean_object* l_PersistentHashMap_findAtAux___main___at_Lean_Elab_ElabFnTable_insert___spec__4___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_AssocList_contains___main___at_Lean_Elab_ElabFnTable_insert___spec__26(lean_object*);
@ -335,7 +340,6 @@ uint8_t l_List_isEmpty___rarg(lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_mkAppN___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_AssocList_find___main___at_Lean_Elab_getMacros___spec__6(lean_object*, lean_object*);
lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__1;
lean_object* lean_usize_to_nat(size_t);
lean_object* l_Lean_Elab_mkMacroAttribute___closed__2;
lean_object* l_Lean_SMap_find_x3f___at_Lean_Elab_ElabFnTable_insert___spec__1(lean_object*);
@ -344,33 +348,32 @@ lean_object* l_Lean_SMap_empty___at_Lean_Elab_ElabAttribute_inhabited___spec__1_
lean_object* l_Lean_Elab_builtinMacroFnTable;
lean_object* l_Lean_SMap_empty___at_Lean_Elab_ElabAttributeExtensionState_inhabited___spec__1___closed__2;
lean_object* l_Lean_Elab_liftMacroM___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_5__ElabAttribute_addImportedParsers___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_mkAppStx___closed__2;
lean_object* l_Lean_Elab_mkMacroAttribute___closed__1;
lean_object* l_IO_ofExcept___at___private_Init_Lean_Elab_Util_6__ElabAttribute_add___spec__1(lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_SMap_empty___at_Lean_Elab_ElabAttribute_inhabited___spec__1(lean_object*);
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_5__ElabAttribute_addImportedParsers___spec__1(lean_object*);
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_8__expandMacroFns(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_ElabFnTable_insert___spec__13___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_registerBuiltinMacroAttr___closed__4;
lean_object* l___private_Init_Lean_Elab_Util_7__expandMacroFns(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__4;
extern lean_object* l_Lean_initAttr;
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_ElabFnTable_insert___spec__24(lean_object*);
lean_object* l_Lean_Elab_syntaxNodeKindOfAttrParam(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_mkAppStx___closed__1;
lean_object* l_PersistentHashMap_mkCollisionNode___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_5__ElabAttribute_addImportedParsers___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_AssocList_find___main___at_Lean_Elab_ElabFnTable_insert___spec__6(lean_object*);
lean_object* l_PersistentHashMap_findAux___main___at_Lean_Elab_getMacros___spec__3___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_AssocList_find___main___at_Lean_Elab_getMacros___spec__6___boxed(lean_object*, lean_object*);
lean_object* l_HashMapImp_expand___at_Lean_Elab_ElabFnTable_insert___spec__27(lean_object*);
lean_object* l_Lean_Elab_mkElabFnOfConstant___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_declareBuiltinMacro___closed__3;
lean_object* l___private_Init_Lean_Elab_Util_3__evalConstantUnsafe(lean_object*);
lean_object* l_Lean_Elab_getBetterRef(lean_object*, lean_object*);
uint8_t lean_string_dec_eq(lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_PersistentHashMap_insertAtCollisionNodeAux___main___at_Lean_Elab_ElabFnTable_insert___spec__12___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__3;
lean_object* l_PersistentHashMap_insert___at_Lean_Elab_ElabFnTable_insert___spec__21___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_PersistentHashMap_insertAtCollisionNodeAux___main___at_Lean_Elab_ElabFnTable_insert___spec__12(lean_object*);
lean_object* l_Lean_Syntax_prettyPrint(lean_object* x_1) {
@ -3775,7 +3778,7 @@ x_2 = lean_alloc_closure((void*)(l___private_Init_Lean_Elab_Util_2__throwUnexpec
return x_2;
}
}
lean_object* l___private_Init_Lean_Elab_Util_3__mkElabFnOfConstantUnsafe___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l___private_Init_Lean_Elab_Util_3__evalConstantUnsafe___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
@ -3842,15 +3845,15 @@ return x_18;
}
}
}
lean_object* l___private_Init_Lean_Elab_Util_3__mkElabFnOfConstantUnsafe(lean_object* x_1) {
lean_object* l___private_Init_Lean_Elab_Util_3__evalConstantUnsafe(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l___private_Init_Lean_Elab_Util_3__mkElabFnOfConstantUnsafe___rarg), 3, 0);
x_2 = lean_alloc_closure((void*)(l___private_Init_Lean_Elab_Util_3__evalConstantUnsafe___rarg), 3, 0);
return x_2;
}
}
lean_object* l_Lean_Elab_mkElabFnOfConstant(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
lean_object* l___private_Init_Lean_Elab_Util_4__evalConstant(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
@ -3858,18 +3861,37 @@ x_5 = l_Lean_mkAttributeImplOfConstant___closed__1;
return x_5;
}
}
lean_object* l_Lean_Elab_mkElabFnOfConstant___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
lean_object* l___private_Init_Lean_Elab_Util_4__evalConstant___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_Lean_Elab_mkElabFnOfConstant(x_1, x_2, x_3, x_4);
x_5 = l___private_Init_Lean_Elab_Util_4__evalConstant(x_1, x_2, x_3, x_4);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
return x_5;
}
}
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
lean_object* _init_l_Lean_Elab_evalSyntaxConstant___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_mkAppStx___closed__2;
x_2 = l_Lean_Parser_Syntax_paren___elambda__1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Elab_evalSyntaxConstant(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4;
x_3 = l_Lean_Elab_evalSyntaxConstant___closed__1;
x_4 = l___private_Init_Lean_Elab_Util_3__evalConstantUnsafe___rarg(x_1, x_3, x_2);
return x_4;
}
}
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_5__ElabAttribute_addImportedParsers___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8; uint8_t x_9;
@ -3898,7 +3920,7 @@ x_14 = lean_ctor_get(x_11, 1);
lean_inc(x_14);
lean_inc(x_1);
lean_inc(x_2);
x_15 = l___private_Init_Lean_Elab_Util_3__mkElabFnOfConstantUnsafe___rarg(x_2, x_1, x_14);
x_15 = l___private_Init_Lean_Elab_Util_3__evalConstantUnsafe___rarg(x_2, x_1, x_14);
if (lean_obj_tag(x_15) == 0)
{
lean_object* x_16; lean_object* x_17; lean_object* x_18;
@ -3934,15 +3956,15 @@ goto _start;
}
}
}
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___spec__1(lean_object* x_1) {
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_5__ElabAttribute_addImportedParsers___spec__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___spec__1___rarg___boxed), 7, 0);
x_2 = lean_alloc_closure((void*)(l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_5__ElabAttribute_addImportedParsers___spec__1___rarg___boxed), 7, 0);
return x_2;
}
}
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___spec__2___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_5__ElabAttribute_addImportedParsers___spec__2___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8; uint8_t x_9;
@ -3970,7 +3992,7 @@ lean_dec(x_5);
x_14 = lean_unsigned_to_nat(0u);
lean_inc(x_2);
lean_inc(x_1);
x_15 = l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___spec__1___rarg(x_1, x_2, x_11, x_11, x_14, x_6, x_7);
x_15 = l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_5__ElabAttribute_addImportedParsers___spec__1___rarg(x_1, x_2, x_11, x_11, x_14, x_6, x_7);
lean_dec(x_11);
if (lean_obj_tag(x_15) == 0)
{
@ -4013,15 +4035,15 @@ return x_22;
}
}
}
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___spec__2(lean_object* x_1) {
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_5__ElabAttribute_addImportedParsers___spec__2(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___spec__2___rarg___boxed), 7, 0);
x_2 = lean_alloc_closure((void*)(l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_5__ElabAttribute_addImportedParsers___spec__2___rarg___boxed), 7, 0);
return x_2;
}
}
lean_object* l___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
lean_object* l___private_Init_Lean_Elab_Util_5__ElabAttribute_addImportedParsers___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
@ -4035,7 +4057,7 @@ x_8 = lean_ctor_get(x_6, 1);
lean_inc(x_8);
lean_dec(x_6);
x_9 = lean_unsigned_to_nat(0u);
x_10 = l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___spec__2___rarg(x_1, x_3, x_4, x_4, x_9, x_7, x_8);
x_10 = l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_5__ElabAttribute_addImportedParsers___spec__2___rarg(x_1, x_3, x_4, x_4, x_9, x_7, x_8);
if (lean_obj_tag(x_10) == 0)
{
uint8_t x_11;
@ -4118,45 +4140,45 @@ return x_27;
}
}
}
lean_object* l___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers(lean_object* x_1) {
lean_object* l___private_Init_Lean_Elab_Util_5__ElabAttribute_addImportedParsers(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___rarg___boxed), 5, 0);
x_2 = lean_alloc_closure((void*)(l___private_Init_Lean_Elab_Util_5__ElabAttribute_addImportedParsers___rarg___boxed), 5, 0);
return x_2;
}
}
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___spec__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_5__ElabAttribute_addImportedParsers___spec__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8;
x_8 = l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___spec__1___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
x_8 = l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_5__ElabAttribute_addImportedParsers___spec__1___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
lean_dec(x_4);
lean_dec(x_3);
return x_8;
}
}
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___spec__2___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_5__ElabAttribute_addImportedParsers___spec__2___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8;
x_8 = l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___spec__2___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
x_8 = l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_5__ElabAttribute_addImportedParsers___spec__2___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
lean_dec(x_4);
lean_dec(x_3);
return x_8;
}
}
lean_object* l___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
lean_object* l___private_Init_Lean_Elab_Util_5__ElabAttribute_addImportedParsers___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = l___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___rarg(x_1, x_2, x_3, x_4, x_5);
x_6 = l___private_Init_Lean_Elab_Util_5__ElabAttribute_addImportedParsers___rarg(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_4);
lean_dec(x_2);
return x_6;
}
}
lean_object* l___private_Init_Lean_Elab_Util_5__ElabAttribute_addExtensionEntry___rarg(lean_object* x_1, lean_object* x_2) {
lean_object* l___private_Init_Lean_Elab_Util_6__ElabAttribute_addExtensionEntry___rarg(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; lean_object* x_8; lean_object* x_9; lean_object* x_10;
@ -4184,15 +4206,15 @@ lean_ctor_set(x_10, 1, x_9);
return x_10;
}
}
lean_object* l___private_Init_Lean_Elab_Util_5__ElabAttribute_addExtensionEntry(lean_object* x_1) {
lean_object* l___private_Init_Lean_Elab_Util_6__ElabAttribute_addExtensionEntry(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l___private_Init_Lean_Elab_Util_5__ElabAttribute_addExtensionEntry___rarg), 2, 0);
x_2 = lean_alloc_closure((void*)(l___private_Init_Lean_Elab_Util_6__ElabAttribute_addExtensionEntry___rarg), 2, 0);
return x_2;
}
}
lean_object* l_IO_ofExcept___at___private_Init_Lean_Elab_Util_6__ElabAttribute_add___spec__1(lean_object* x_1, lean_object* x_2) {
lean_object* l_IO_ofExcept___at___private_Init_Lean_Elab_Util_7__ElabAttribute_add___spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
if (lean_obj_tag(x_1) == 0)
@ -4219,13 +4241,13 @@ return x_7;
}
}
}
lean_object* l___private_Init_Lean_Elab_Util_6__ElabAttribute_add___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, uint8_t x_7, lean_object* x_8) {
lean_object* l___private_Init_Lean_Elab_Util_7__ElabAttribute_add___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, uint8_t x_7, lean_object* x_8) {
_start:
{
lean_object* x_9;
lean_inc(x_5);
lean_inc(x_4);
x_9 = l___private_Init_Lean_Elab_Util_3__mkElabFnOfConstantUnsafe___rarg(x_4, x_2, x_5);
x_9 = l___private_Init_Lean_Elab_Util_3__evalConstantUnsafe___rarg(x_4, x_2, x_5);
if (lean_obj_tag(x_9) == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12;
@ -4250,7 +4272,7 @@ lean_inc(x_13);
lean_dec(x_9);
lean_inc(x_4);
x_14 = l_Lean_Elab_syntaxNodeKindOfAttrParam(x_4, x_1, x_6);
x_15 = l_IO_ofExcept___at___private_Init_Lean_Elab_Util_6__ElabAttribute_add___spec__1(x_14, x_8);
x_15 = l_IO_ofExcept___at___private_Init_Lean_Elab_Util_7__ElabAttribute_add___spec__1(x_14, x_8);
lean_dec(x_14);
if (lean_obj_tag(x_15) == 0)
{
@ -4320,30 +4342,30 @@ return x_30;
}
}
}
lean_object* l___private_Init_Lean_Elab_Util_6__ElabAttribute_add(lean_object* x_1) {
lean_object* l___private_Init_Lean_Elab_Util_7__ElabAttribute_add(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l___private_Init_Lean_Elab_Util_6__ElabAttribute_add___rarg___boxed), 8, 0);
x_2 = lean_alloc_closure((void*)(l___private_Init_Lean_Elab_Util_7__ElabAttribute_add___rarg___boxed), 8, 0);
return x_2;
}
}
lean_object* l_IO_ofExcept___at___private_Init_Lean_Elab_Util_6__ElabAttribute_add___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
lean_object* l_IO_ofExcept___at___private_Init_Lean_Elab_Util_7__ElabAttribute_add___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_IO_ofExcept___at___private_Init_Lean_Elab_Util_6__ElabAttribute_add___spec__1(x_1, x_2);
x_3 = l_IO_ofExcept___at___private_Init_Lean_Elab_Util_7__ElabAttribute_add___spec__1(x_1, x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* l___private_Init_Lean_Elab_Util_6__ElabAttribute_add___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
lean_object* l___private_Init_Lean_Elab_Util_7__ElabAttribute_add___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
uint8_t x_9; lean_object* x_10;
x_9 = lean_unbox(x_7);
lean_dec(x_7);
x_10 = l___private_Init_Lean_Elab_Util_6__ElabAttribute_add___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_9, x_8);
x_10 = l___private_Init_Lean_Elab_Util_7__ElabAttribute_add___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_9, x_8);
lean_dec(x_6);
lean_dec(x_1);
return x_10;
@ -5247,7 +5269,7 @@ lean_object* _init_l_Lean_Elab_mkElabAttributeAux___rarg___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Init_Lean_Elab_Util_5__ElabAttribute_addExtensionEntry___rarg), 2, 0);
x_1 = lean_alloc_closure((void*)(l___private_Init_Lean_Elab_Util_6__ElabAttribute_addExtensionEntry___rarg), 2, 0);
return x_1;
}
}
@ -5283,7 +5305,7 @@ lean_inc(x_6);
x_8 = lean_alloc_closure((void*)(l___private_Init_Lean_Elab_Util_1__ElabAttribute_mkInitial___rarg___boxed), 2, 1);
lean_closure_set(x_8, 0, x_6);
lean_inc(x_3);
x_9 = lean_alloc_closure((void*)(l___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___rarg___boxed), 5, 2);
x_9 = lean_alloc_closure((void*)(l___private_Init_Lean_Elab_Util_5__ElabAttribute_addImportedParsers___rarg___boxed), 5, 2);
lean_closure_set(x_9, 0, x_3);
lean_closure_set(x_9, 1, x_6);
x_10 = l_Lean_Elab_mkElabAttributeAux___rarg___closed__1;
@ -5310,7 +5332,7 @@ x_17 = l_Lean_Elab_mkElabAttributeAux___rarg___closed__4;
lean_inc(x_5);
x_18 = lean_string_append(x_5, x_17);
lean_inc(x_15);
x_19 = lean_alloc_closure((void*)(l___private_Init_Lean_Elab_Util_6__ElabAttribute_add___rarg___boxed), 8, 3);
x_19 = lean_alloc_closure((void*)(l___private_Init_Lean_Elab_Util_7__ElabAttribute_add___rarg___boxed), 8, 3);
lean_closure_set(x_19, 0, x_2);
lean_closure_set(x_19, 1, x_3);
lean_closure_set(x_19, 2, x_15);
@ -5837,7 +5859,7 @@ lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_8 = l_Lean_mkAppStx___closed__6;
lean_inc(x_1);
x_9 = l_Lean_Elab_syntaxNodeKindOfAttrParam(x_1, x_8, x_3);
x_10 = l_IO_ofExcept___at___private_Init_Lean_Elab_Util_6__ElabAttribute_add___spec__1(x_9, x_5);
x_10 = l_IO_ofExcept___at___private_Init_Lean_Elab_Util_7__ElabAttribute_add___spec__1(x_9, x_5);
lean_dec(x_9);
if (lean_obj_tag(x_10) == 0)
{
@ -6222,7 +6244,7 @@ lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
lean_object* l___private_Init_Lean_Elab_Util_7__expandMacroFns___main(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
lean_object* l___private_Init_Lean_Elab_Util_8__expandMacroFns___main(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
if (lean_obj_tag(x_2) == 0)
@ -6267,11 +6289,11 @@ goto _start;
}
}
}
lean_object* l___private_Init_Lean_Elab_Util_7__expandMacroFns(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
lean_object* l___private_Init_Lean_Elab_Util_8__expandMacroFns(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l___private_Init_Lean_Elab_Util_7__expandMacroFns___main(x_1, x_2, x_3, x_4);
x_5 = l___private_Init_Lean_Elab_Util_8__expandMacroFns___main(x_1, x_2, x_3, x_4);
return x_5;
}
}
@ -6526,7 +6548,7 @@ lean_object* x_13; lean_object* x_14;
x_13 = lean_ctor_get(x_10, 0);
lean_inc(x_13);
lean_dec(x_10);
x_14 = l___private_Init_Lean_Elab_Util_7__expandMacroFns___main(x_2, x_13, x_3, x_4);
x_14 = l___private_Init_Lean_Elab_Util_8__expandMacroFns___main(x_2, x_13, x_3, x_4);
return x_14;
}
}
@ -6855,7 +6877,7 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Elab_adaptMacro___rarg), 4, 0);
return x_2;
}
}
lean_object* _init_l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__1() {
lean_object* _init_l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -6865,7 +6887,7 @@ x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__2() {
lean_object* _init_l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__2() {
_start:
{
lean_object* x_1;
@ -6873,21 +6895,21 @@ x_1 = lean_mk_string("step");
return x_1;
}
}
lean_object* _init_l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__3() {
lean_object* _init_l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__1;
x_2 = l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__2;
x_1 = l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__1;
x_2 = l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__2;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l___private_Init_Lean_Elab_Util_8__regTraceClasses(lean_object* x_1) {
lean_object* l___private_Init_Lean_Elab_Util_9__regTraceClasses(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__1;
x_2 = l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__1;
x_3 = l_Lean_registerTraceClass(x_2, x_1);
if (lean_obj_tag(x_3) == 0)
{
@ -6895,7 +6917,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___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__3;
x_5 = l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__3;
x_6 = l_Lean_registerTraceClass(x_5, x_4);
return x_6;
}
@ -6992,6 +7014,8 @@ l___private_Init_Lean_Elab_Util_2__throwUnexpectedElabType___rarg___closed__2 =
lean_mark_persistent(l___private_Init_Lean_Elab_Util_2__throwUnexpectedElabType___rarg___closed__2);
l___private_Init_Lean_Elab_Util_2__throwUnexpectedElabType___rarg___closed__3 = _init_l___private_Init_Lean_Elab_Util_2__throwUnexpectedElabType___rarg___closed__3();
lean_mark_persistent(l___private_Init_Lean_Elab_Util_2__throwUnexpectedElabType___rarg___closed__3);
l_Lean_Elab_evalSyntaxConstant___closed__1 = _init_l_Lean_Elab_evalSyntaxConstant___closed__1();
lean_mark_persistent(l_Lean_Elab_evalSyntaxConstant___closed__1);
l_Lean_SMap_empty___at_Lean_Elab_mkElabAttributeAux___spec__4___closed__1 = _init_l_Lean_SMap_empty___at_Lean_Elab_mkElabAttributeAux___spec__4___closed__1();
lean_mark_persistent(l_Lean_SMap_empty___at_Lean_Elab_mkElabAttributeAux___spec__4___closed__1);
l_Lean_SMap_empty___at_Lean_Elab_mkElabAttributeAux___spec__4___closed__2 = _init_l_Lean_SMap_empty___at_Lean_Elab_mkElabAttributeAux___spec__4___closed__2();
@ -7085,13 +7109,13 @@ if (lean_io_result_is_error(res)) return res;
l_Lean_Elab_macroAttribute = lean_io_result_get_value(res);
lean_mark_persistent(l_Lean_Elab_macroAttribute);
lean_dec_ref(res);
l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__1 = _init_l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__1();
lean_mark_persistent(l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__1);
l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__2 = _init_l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__2();
lean_mark_persistent(l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__2);
l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__3 = _init_l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__3();
lean_mark_persistent(l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__3);
res = l___private_Init_Lean_Elab_Util_8__regTraceClasses(lean_io_mk_world());
l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__1 = _init_l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__1();
lean_mark_persistent(l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__1);
l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__2 = _init_l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__2();
lean_mark_persistent(l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__2);
l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__3 = _init_l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__3();
lean_mark_persistent(l___private_Init_Lean_Elab_Util_9__regTraceClasses___closed__3);
res = l___private_Init_Lean_Elab_Util_9__regTraceClasses(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_mk_io_result(lean_box(0));

122
stage0/stdlib/Init/Lean/Expr.c
View file

@ -63,12 +63,14 @@ uint64_t l_Bool_toUInt64(uint8_t);
lean_object* l_Lean_Expr_updateMData_x21___closed__2;
lean_object* l_Lean_Expr_instantiateLevelParamsArray___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Literal_hasLess;
lean_object* l_Lean_Expr_isOptParam___boxed(lean_object*);
lean_object* l_Lean_Expr_updateMData_x21___closed__1;
lean_object* l_List_map___main___at_Lean_Expr_instantiateLevelParams___spec__4(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__3;
lean_object* l_Lean_mkForallEx___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_Data_hasBeq___boxed(lean_object*, lean_object*);
lean_object* l_Lean_mkLambda___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAutoParamTactic_x3f(lean_object*);
lean_object* l_Lean_mkLit(lean_object*);
lean_object* l_Lean_Expr_getAppRevArgs(lean_object*);
lean_object* l_Lean_Expr_hasLevelParamEx___boxed(lean_object*);
@ -103,6 +105,7 @@ lean_object* l_Lean_Expr_lt___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Expr_updateLet___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_appFn_x21(lean_object*);
lean_object* l_Lean_Expr_hasLevelMVar___boxed(lean_object*);
lean_object* l_Lean_Expr_isAutoParam___boxed(lean_object*);
uint8_t l_Lean_Expr_isAppOf(lean_object*, lean_object*);
lean_object* l_Lean_Expr_mvarId_x21___closed__2;
lean_object* l_Lean_BinderInfo_toUInt64___boxed(lean_object*);
@ -234,6 +237,7 @@ lean_object* l_Lean_mkDecIsTrue___closed__1;
lean_object* l_Lean_BinderInfo_beq___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Expr_instantiateLevelParams(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Expr_5__withAppRevAux___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAutoParamTactic_x3f___boxed(lean_object*);
lean_object* l_Lean_Expr_Data_hasLevelParam___boxed(lean_object*);
lean_object* l___private_Init_Lean_Expr_5__withAppRevAux___main(lean_object*);
lean_object* l_Lean_Expr_isFVar___boxed(lean_object*);
@ -303,11 +307,14 @@ lean_object* l_Lean_mkDecIsFalse(lean_object*, lean_object*);
uint8_t lean_expr_quick_lt(lean_object*, lean_object*);
lean_object* l_Lean_mkFVar(lean_object*);
uint8_t l_Lean_Expr_isAppOfArity___main(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAutoParamTactic_x3f___closed__1;
uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
lean_object* l_Lean_Expr_mkData___boxed__const__1;
lean_object* l_Lean_MData_empty;
size_t lean_usize_of_nat(lean_object*);
size_t l_Lean_ExprStructEq_hash(lean_object*);
uint8_t l_Lean_Expr_isAutoParam(lean_object*);
lean_object* l_Lean_Expr_getAutoParamTactic_x3f___closed__2;
lean_object* l_Lean_Level_instantiateParams___main(lean_object*, lean_object*);
uint8_t l_Lean_Expr_isLambda(lean_object*);
lean_object* l_Lean_Expr_updateSort_x21___closed__2;
@ -446,6 +453,7 @@ lean_object* l_Lean_Expr_Data_hasFVar___boxed(lean_object*);
uint8_t l_Lean_Expr_isProj(lean_object*);
uint8_t l_Lean_Expr_binderInfo(lean_object*);
size_t lean_usize_mix_hash(size_t, size_t);
uint8_t l_Lean_Expr_isOptParam(lean_object*);
lean_object* lean_expr_abstract(lean_object*, lean_object*);
lean_object* l_Lean_Expr_getArg_x21(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkApp2(lean_object*, lean_object*, lean_object*);
@ -7292,6 +7300,96 @@ lean_dec(x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Expr_getAutoParamTactic_x3f___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("autoParam");
return x_1;
}
}
lean_object* _init_l_Lean_Expr_getAutoParamTactic_x3f___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Expr_getAutoParamTactic_x3f___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Expr_getAutoParamTactic_x3f(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4;
x_2 = l_Lean_Expr_getAutoParamTactic_x3f___closed__2;
x_3 = lean_unsigned_to_nat(2u);
x_4 = l_Lean_Expr_isAppOfArity___main(x_1, x_2, x_3);
if (x_4 == 0)
{
lean_object* x_5;
x_5 = lean_box(0);
return x_5;
}
else
{
lean_object* x_6; lean_object* x_7;
x_6 = l_Lean_Expr_appArg_x21(x_1);
x_7 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_7, 0, x_6);
return x_7;
}
}
}
lean_object* l_Lean_Expr_getAutoParamTactic_x3f___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Expr_getAutoParamTactic_x3f(x_1);
lean_dec(x_1);
return x_2;
}
}
uint8_t l_Lean_Expr_isOptParam(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4;
x_2 = l_Lean_Expr_getOptParamDefault_x3f___closed__2;
x_3 = lean_unsigned_to_nat(2u);
x_4 = l_Lean_Expr_isAppOfArity___main(x_1, x_2, x_3);
return x_4;
}
}
lean_object* l_Lean_Expr_isOptParam___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l_Lean_Expr_isOptParam(x_1);
lean_dec(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
uint8_t l_Lean_Expr_isAutoParam(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4;
x_2 = l_Lean_Expr_getAutoParamTactic_x3f___closed__2;
x_3 = lean_unsigned_to_nat(2u);
x_4 = l_Lean_Expr_isAppOfArity___main(x_1, x_2, x_3);
return x_4;
}
}
lean_object* l_Lean_Expr_isAutoParam___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l_Lean_Expr_isAutoParam(x_1);
lean_dec(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
lean_object* l___private_Init_Lean_Expr_10__hasAnyFVarAux___main(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -7516,7 +7614,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(769u);
x_2 = lean_unsigned_to_nat(781u);
x_3 = lean_unsigned_to_nat(18u);
x_4 = l_Lean_Expr_appFn_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7558,7 +7656,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(778u);
x_2 = lean_unsigned_to_nat(790u);
x_3 = lean_unsigned_to_nat(18u);
x_4 = l_Lean_Expr_constName_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7607,7 +7705,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(787u);
x_2 = lean_unsigned_to_nat(799u);
x_3 = lean_unsigned_to_nat(14u);
x_4 = l_Lean_Expr_updateSort_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7664,7 +7762,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(804u);
x_2 = lean_unsigned_to_nat(816u);
x_3 = lean_unsigned_to_nat(17u);
x_4 = l_Lean_Expr_updateMData_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7705,7 +7803,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(809u);
x_2 = lean_unsigned_to_nat(821u);
x_3 = lean_unsigned_to_nat(18u);
x_4 = l_Lean_Expr_updateProj_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7756,7 +7854,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(818u);
x_2 = lean_unsigned_to_nat(830u);
x_3 = lean_unsigned_to_nat(21u);
x_4 = l_Lean_Expr_updateForall_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7800,7 +7898,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(823u);
x_2 = lean_unsigned_to_nat(835u);
x_3 = lean_unsigned_to_nat(21u);
x_4 = l_Lean_Expr_updateForall_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7854,7 +7952,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(832u);
x_2 = lean_unsigned_to_nat(844u);
x_3 = lean_unsigned_to_nat(17u);
x_4 = l_Lean_Expr_updateLambda_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7898,7 +7996,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(837u);
x_2 = lean_unsigned_to_nat(849u);
x_3 = lean_unsigned_to_nat(17u);
x_4 = l_Lean_Expr_updateLambda_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7942,7 +8040,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(846u);
x_2 = lean_unsigned_to_nat(858u);
x_3 = lean_unsigned_to_nat(20u);
x_4 = l_Lean_Expr_letName_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -9937,6 +10035,10 @@ l_Lean_Expr_getOptParamDefault_x3f___closed__1 = _init_l_Lean_Expr_getOptParamDe
lean_mark_persistent(l_Lean_Expr_getOptParamDefault_x3f___closed__1);
l_Lean_Expr_getOptParamDefault_x3f___closed__2 = _init_l_Lean_Expr_getOptParamDefault_x3f___closed__2();
lean_mark_persistent(l_Lean_Expr_getOptParamDefault_x3f___closed__2);
l_Lean_Expr_getAutoParamTactic_x3f___closed__1 = _init_l_Lean_Expr_getAutoParamTactic_x3f___closed__1();
lean_mark_persistent(l_Lean_Expr_getAutoParamTactic_x3f___closed__1);
l_Lean_Expr_getAutoParamTactic_x3f___closed__2 = _init_l_Lean_Expr_getAutoParamTactic_x3f___closed__2();
lean_mark_persistent(l_Lean_Expr_getAutoParamTactic_x3f___closed__2);
l_Lean_Expr_updateApp_x21___closed__1 = _init_l_Lean_Expr_updateApp_x21___closed__1();
lean_mark_persistent(l_Lean_Expr_updateApp_x21___closed__1);
l_Lean_Expr_updateConst_x21___closed__1 = _init_l_Lean_Expr_updateConst_x21___closed__1();

237
stage0/stdlib/Init/Lean/Parser/Command.c
View file

@ -96,6 +96,7 @@ lean_object* l_Lean_Parser_Command_protected___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_set__option___elambda__1___closed__6;
lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_stxQuot___elambda__1___spec__1(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_haveAssign___closed__2;
extern lean_object* l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__1;
lean_object* l_Lean_Parser_Command_structExplicitBinder___closed__11;
lean_object* l_Lean_Parser_Command_declId___elambda__1___closed__3;
lean_object* l_Lean_Parser_Command_openRenaming;
@ -202,7 +203,6 @@ lean_object* l_Lean_Parser_Command_structureTk___elambda__1___closed__1;
lean_object* l_Lean_Parser_Command_check___closed__5;
lean_object* l_Lean_Parser_Command_def___elambda__1___closed__3;
lean_object* l_Lean_Parser_Command_attrArg___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_stxQuot___elambda__1___closed__8;
lean_object* l_Lean_Parser_Command_classInductive___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_exit___elambda__1___closed__9;
lean_object* l_Lean_Parser_Command_structExplicitBinder___elambda__1___closed__3;
@ -317,7 +317,6 @@ lean_object* l_Lean_Parser_Command_openRenamingItem___closed__4;
lean_object* l_Lean_Parser_Command_open___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_extends___closed__5;
lean_object* l_Lean_Parser_Command_private___closed__5;
lean_object* l_Lean_Parser_Term_stxQuot___elambda__1___closed__9;
lean_object* l_Lean_Parser_Command_resolve__name___elambda__1___closed__9;
lean_object* l_Lean_Parser_Command_variables___closed__6;
lean_object* l_Lean_Parser_Command_attribute___elambda__1___closed__7;
@ -426,6 +425,7 @@ lean_object* l_Lean_Parser_Command_constant___closed__2;
lean_object* l_Lean_Parser_Command_export___closed__9;
lean_object* l_Lean_Parser_noFirstTokenInfo(lean_object*);
lean_object* l_Lean_Parser_Command_check__failure___elambda__1(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_tacticBlock___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_set__option___elambda__1___closed__2;
lean_object* l_Lean_Parser_nonReservedSymbolInfo(lean_object*, uint8_t);
lean_object* l_Lean_Parser_Command_example___elambda__1(lean_object*, lean_object*);
@ -586,7 +586,6 @@ lean_object* l_Lean_Parser_Command_end___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_declaration___closed__4;
lean_object* l_Lean_Parser_Command_theorem___closed__7;
lean_object* l_Lean_Parser_Command_structInstBinder___closed__2;
extern lean_object* l_Lean_mkAppStx___closed__6;
lean_object* l_Lean_Parser_Command_instance___elambda__1___closed__1;
lean_object* l_Lean_Parser_Command_relaxedInferMod___closed__4;
lean_object* l_Lean_Parser_Command_inferMod;
@ -644,6 +643,7 @@ lean_object* l_Lean_Parser_Command_variable;
lean_object* l_Lean_Parser_Command_universes___closed__4;
lean_object* l_Lean_Parser_Command_classTk___elambda__1___closed__4;
lean_object* l_Lean_Parser_Command_constant___elambda__1___closed__6;
extern lean_object* l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_relaxedInferMod___elambda__1___closed__4;
lean_object* l_Lean_Parser_Command_declSig___elambda__1(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_haveAssign___elambda__1___closed__8;
@ -870,7 +870,6 @@ extern lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___a
lean_object* l_Lean_Parser_categoryParser___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_variable___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_classInductive___elambda__1___closed__1;
lean_object* l_Lean_Parser_Command_end___elambda__1___closed__9;
lean_object* l_Lean_Parser_Command_instance___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_noncomputable___closed__4;
lean_object* l_Lean_Parser_Command_structInstBinder___elambda__1___closed__2;
@ -1321,43 +1320,25 @@ return x_17;
lean_object* _init_l_Lean_Parser_Term_stxQuot___elambda__1___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("stxQuot");
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Term_stxQuot___elambda__1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_mkAppStx___closed__6;
x_2 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_stxQuot___elambda__1___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2;
x_1 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Parser_Term_stxQuot___elambda__1___closed__4() {
lean_object* _init_l_Lean_Parser_Term_stxQuot___elambda__1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__1;
x_2 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__3;
x_1 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__1;
x_2 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__1;
x_3 = 1;
x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
return x_4;
}
}
lean_object* _init_l_Lean_Parser_Term_stxQuot___elambda__1___closed__5() {
lean_object* _init_l_Lean_Parser_Term_stxQuot___elambda__1___closed__3() {
_start:
{
lean_object* x_1;
@ -1365,41 +1346,41 @@ x_1 = lean_mk_string("`(");
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Term_stxQuot___elambda__1___closed__6() {
lean_object* _init_l_Lean_Parser_Term_stxQuot___elambda__1___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__5;
x_1 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__3;
x_2 = l_String_trim(x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Parser_Term_stxQuot___elambda__1___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Char_HasRepr___closed__1;
x_2 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__4;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_stxQuot___elambda__1___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__5;
x_2 = l_Char_HasRepr___closed__1;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_stxQuot___elambda__1___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Char_HasRepr___closed__1;
x_2 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__6;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_stxQuot___elambda__1___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__7;
x_2 = l_Char_HasRepr___closed__1;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_stxQuot___elambda__1___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__8;
x_2 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__6;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
@ -1410,7 +1391,7 @@ lean_object* l_Lean_Parser_Term_stxQuot___elambda__1(lean_object* x_1, lean_obje
_start:
{
lean_object* x_3; lean_object* x_4; uint8_t x_5;
x_3 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__4;
x_3 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2;
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
lean_inc(x_2);
@ -1443,13 +1424,13 @@ lean_object* x_80; lean_object* x_81; uint8_t x_82;
x_80 = lean_ctor_get(x_79, 1);
lean_inc(x_80);
lean_dec(x_79);
x_81 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__6;
x_81 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__4;
x_82 = lean_string_dec_eq(x_80, x_81);
lean_dec(x_80);
if (x_82 == 0)
{
lean_object* x_83; lean_object* x_84;
x_83 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__9;
x_83 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__7;
x_84 = l_Lean_Parser_ParserState_mkErrorsAt(x_76, x_83, x_75);
x_35 = x_84;
goto block_74;
@ -1465,7 +1446,7 @@ else
{
lean_object* x_85; lean_object* x_86;
lean_dec(x_79);
x_85 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__9;
x_85 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__7;
x_86 = l_Lean_Parser_ParserState_mkErrorsAt(x_76, x_85, x_75);
x_35 = x_86;
goto block_74;
@ -1475,7 +1456,7 @@ else
{
lean_object* x_87; lean_object* x_88;
lean_dec(x_77);
x_87 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__9;
x_87 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__7;
x_88 = l_Lean_Parser_ParserState_mkErrorsAt(x_76, x_87, x_75);
x_35 = x_88;
goto block_74;
@ -1514,7 +1495,7 @@ if (x_17 == 0)
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_18 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___closed__7;
x_19 = l_Lean_Parser_ParserState_mkErrorsAt(x_11, x_18, x_10);
x_20 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2;
x_20 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_21 = l_Lean_Parser_ParserState_mkNode(x_19, x_20, x_7);
return x_21;
}
@ -1522,7 +1503,7 @@ else
{
lean_object* x_22; lean_object* x_23;
lean_dec(x_10);
x_22 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2;
x_22 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_23 = l_Lean_Parser_ParserState_mkNode(x_11, x_22, x_7);
return x_23;
}
@ -1533,7 +1514,7 @@ lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27;
lean_dec(x_14);
x_24 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___closed__7;
x_25 = l_Lean_Parser_ParserState_mkErrorsAt(x_11, x_24, x_10);
x_26 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2;
x_26 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_27 = l_Lean_Parser_ParserState_mkNode(x_25, x_26, x_7);
return x_27;
}
@ -1544,7 +1525,7 @@ lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31;
lean_dec(x_12);
x_28 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___closed__7;
x_29 = l_Lean_Parser_ParserState_mkErrorsAt(x_11, x_28, x_10);
x_30 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2;
x_30 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_31 = l_Lean_Parser_ParserState_mkNode(x_29, x_30, x_7);
return x_31;
}
@ -1554,7 +1535,7 @@ else
lean_object* x_32; lean_object* x_33;
lean_dec(x_9);
lean_dec(x_1);
x_32 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2;
x_32 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_33 = l_Lean_Parser_ParserState_mkNode(x_8, x_32, x_7);
return x_33;
}
@ -1694,7 +1675,7 @@ else
lean_object* x_72; lean_object* x_73;
lean_dec(x_36);
lean_dec(x_1);
x_72 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2;
x_72 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_73 = l_Lean_Parser_ParserState_mkNode(x_35, x_72, x_7);
return x_73;
}
@ -1765,13 +1746,13 @@ lean_object* x_177; lean_object* x_178; uint8_t x_179;
x_177 = lean_ctor_get(x_176, 1);
lean_inc(x_177);
lean_dec(x_176);
x_178 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__6;
x_178 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__4;
x_179 = lean_string_dec_eq(x_177, x_178);
lean_dec(x_177);
if (x_179 == 0)
{
lean_object* x_180; lean_object* x_181;
x_180 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__9;
x_180 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__7;
lean_inc(x_91);
x_181 = l_Lean_Parser_ParserState_mkErrorsAt(x_173, x_180, x_91);
x_132 = x_181;
@ -1787,7 +1768,7 @@ else
{
lean_object* x_182; lean_object* x_183;
lean_dec(x_176);
x_182 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__9;
x_182 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__7;
lean_inc(x_91);
x_183 = l_Lean_Parser_ParserState_mkErrorsAt(x_173, x_182, x_91);
x_132 = x_183;
@ -1798,7 +1779,7 @@ else
{
lean_object* x_184; lean_object* x_185;
lean_dec(x_174);
x_184 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__9;
x_184 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__7;
lean_inc(x_91);
x_185 = l_Lean_Parser_ParserState_mkErrorsAt(x_173, x_184, x_91);
x_132 = x_185;
@ -1838,7 +1819,7 @@ if (x_109 == 0)
lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113; lean_object* x_114;
x_110 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___closed__7;
x_111 = l_Lean_Parser_ParserState_mkErrorsAt(x_103, x_110, x_102);
x_112 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2;
x_112 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_113 = l_Lean_Parser_ParserState_mkNode(x_111, x_112, x_99);
x_114 = l_Lean_Parser_mergeOrElseErrors(x_113, x_94, x_91);
lean_dec(x_91);
@ -1848,7 +1829,7 @@ else
{
lean_object* x_115; lean_object* x_116; lean_object* x_117;
lean_dec(x_102);
x_115 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2;
x_115 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_116 = l_Lean_Parser_ParserState_mkNode(x_103, x_115, x_99);
x_117 = l_Lean_Parser_mergeOrElseErrors(x_116, x_94, x_91);
lean_dec(x_91);
@ -1861,7 +1842,7 @@ lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* x_121;
lean_dec(x_106);
x_118 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___closed__7;
x_119 = l_Lean_Parser_ParserState_mkErrorsAt(x_103, x_118, x_102);
x_120 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2;
x_120 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_121 = l_Lean_Parser_ParserState_mkNode(x_119, x_120, x_99);
x_122 = l_Lean_Parser_mergeOrElseErrors(x_121, x_94, x_91);
lean_dec(x_91);
@ -1874,7 +1855,7 @@ lean_object* x_123; lean_object* x_124; lean_object* x_125; lean_object* x_126;
lean_dec(x_104);
x_123 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___closed__7;
x_124 = l_Lean_Parser_ParserState_mkErrorsAt(x_103, x_123, x_102);
x_125 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2;
x_125 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_126 = l_Lean_Parser_ParserState_mkNode(x_124, x_125, x_99);
x_127 = l_Lean_Parser_mergeOrElseErrors(x_126, x_94, x_91);
lean_dec(x_91);
@ -1886,7 +1867,7 @@ else
lean_object* x_128; lean_object* x_129; lean_object* x_130;
lean_dec(x_101);
lean_dec(x_1);
x_128 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2;
x_128 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_129 = l_Lean_Parser_ParserState_mkNode(x_100, x_128, x_99);
x_130 = l_Lean_Parser_mergeOrElseErrors(x_129, x_94, x_91);
lean_dec(x_91);
@ -2028,7 +2009,7 @@ else
lean_object* x_169; lean_object* x_170; lean_object* x_171;
lean_dec(x_133);
lean_dec(x_1);
x_169 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2;
x_169 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_170 = l_Lean_Parser_ParserState_mkNode(x_132, x_169, x_99);
x_171 = l_Lean_Parser_mergeOrElseErrors(x_170, x_94, x_91);
lean_dec(x_91);
@ -2044,7 +2025,7 @@ lean_object* _init_l_Lean_Parser_Term_stxQuot___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__6;
x_1 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__4;
x_2 = l_Lean_Parser_Level_paren___closed__1;
x_3 = l_Lean_Parser_symbolInfo(x_1, x_2);
return x_3;
@ -2098,7 +2079,7 @@ lean_object* _init_l_Lean_Parser_Term_stxQuot___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2;
x_1 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_2 = l_Lean_Parser_Term_stxQuot___closed__5;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
@ -2108,7 +2089,7 @@ lean_object* _init_l_Lean_Parser_Term_stxQuot___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__4;
x_1 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Term_stxQuot___closed__6;
@ -2149,7 +2130,7 @@ _start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l_Lean_Parser_termParser___closed__2;
x_3 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2;
x_3 = l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Term_stxQuot;
x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
@ -23103,43 +23084,35 @@ return x_6;
lean_object* _init_l_Lean_Parser_Command_end___elambda__1___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("end");
return x_1;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_docComment___elambda__1___closed__2;
x_2 = l_Lean_Parser_Term_tacticBlock___elambda__1___closed__7;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Command_end___elambda__1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_docComment___elambda__1___closed__2;
x_2 = l_Lean_Parser_Command_end___elambda__1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Command_end___elambda__1___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Command_end___elambda__1___closed__2;
x_1 = l_Lean_Parser_Command_end___elambda__1___closed__1;
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Parser_Command_end___elambda__1___closed__4() {
lean_object* _init_l_Lean_Parser_Command_end___elambda__1___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Command_end___elambda__1___closed__1;
x_2 = l_Lean_Parser_Command_end___elambda__1___closed__3;
x_1 = l_Lean_Parser_Term_tacticBlock___elambda__1___closed__7;
x_2 = l_Lean_Parser_Command_end___elambda__1___closed__2;
x_3 = 1;
x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
return x_4;
}
}
lean_object* _init_l_Lean_Parser_Command_end___elambda__1___closed__5() {
lean_object* _init_l_Lean_Parser_Command_end___elambda__1___closed__4() {
_start:
{
lean_object* x_1;
@ -23147,21 +23120,31 @@ x_1 = lean_mk_string("end ");
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Command_end___elambda__1___closed__6() {
lean_object* _init_l_Lean_Parser_Command_end___elambda__1___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Command_end___elambda__1___closed__5;
x_1 = l_Lean_Parser_Command_end___elambda__1___closed__4;
x_2 = l_String_trim(x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Parser_Command_end___elambda__1___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Char_HasRepr___closed__1;
x_2 = l_Lean_Parser_Command_end___elambda__1___closed__5;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Command_end___elambda__1___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Char_HasRepr___closed__1;
x_2 = l_Lean_Parser_Command_end___elambda__1___closed__6;
x_1 = l_Lean_Parser_Command_end___elambda__1___closed__6;
x_2 = l_Char_HasRepr___closed__1;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
@ -23170,18 +23153,8 @@ lean_object* _init_l_Lean_Parser_Command_end___elambda__1___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_end___elambda__1___closed__7;
x_2 = l_Char_HasRepr___closed__1;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Command_end___elambda__1___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_Command_end___elambda__1___closed__8;
x_2 = l_Lean_Parser_Command_end___elambda__1___closed__7;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
@ -23192,7 +23165,7 @@ lean_object* l_Lean_Parser_Command_end___elambda__1(lean_object* x_1, lean_objec
_start:
{
lean_object* x_3; lean_object* x_4; uint8_t x_5;
x_3 = l_Lean_Parser_Command_end___elambda__1___closed__4;
x_3 = l_Lean_Parser_Command_end___elambda__1___closed__3;
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
lean_inc(x_2);
@ -23225,13 +23198,13 @@ lean_object* x_38; lean_object* x_39; uint8_t x_40;
x_38 = lean_ctor_get(x_37, 1);
lean_inc(x_38);
lean_dec(x_37);
x_39 = l_Lean_Parser_Command_end___elambda__1___closed__6;
x_39 = l_Lean_Parser_Command_end___elambda__1___closed__5;
x_40 = lean_string_dec_eq(x_38, x_39);
lean_dec(x_38);
if (x_40 == 0)
{
lean_object* x_41; lean_object* x_42;
x_41 = l_Lean_Parser_Command_end___elambda__1___closed__9;
x_41 = l_Lean_Parser_Command_end___elambda__1___closed__8;
x_42 = l_Lean_Parser_ParserState_mkErrorsAt(x_34, x_41, x_33);
x_8 = x_42;
goto block_32;
@ -23247,7 +23220,7 @@ else
{
lean_object* x_43; lean_object* x_44;
lean_dec(x_37);
x_43 = l_Lean_Parser_Command_end___elambda__1___closed__9;
x_43 = l_Lean_Parser_Command_end___elambda__1___closed__8;
x_44 = l_Lean_Parser_ParserState_mkErrorsAt(x_34, x_43, x_33);
x_8 = x_44;
goto block_32;
@ -23257,7 +23230,7 @@ else
{
lean_object* x_45; lean_object* x_46;
lean_dec(x_35);
x_45 = l_Lean_Parser_Command_end___elambda__1___closed__9;
x_45 = l_Lean_Parser_Command_end___elambda__1___closed__8;
x_46 = l_Lean_Parser_ParserState_mkErrorsAt(x_34, x_45, x_33);
x_8 = x_46;
goto block_32;
@ -23285,7 +23258,7 @@ lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18;
lean_dec(x_12);
x_15 = l_Lean_nullKind;
x_16 = l_Lean_Parser_ParserState_mkNode(x_13, x_15, x_11);
x_17 = l_Lean_Parser_Command_end___elambda__1___closed__2;
x_17 = l_Lean_Parser_Command_end___elambda__1___closed__1;
x_18 = l_Lean_Parser_ParserState_mkNode(x_16, x_17, x_7);
return x_18;
}
@ -23303,7 +23276,7 @@ lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24;
lean_dec(x_12);
x_21 = l_Lean_nullKind;
x_22 = l_Lean_Parser_ParserState_mkNode(x_13, x_21, x_11);
x_23 = l_Lean_Parser_Command_end___elambda__1___closed__2;
x_23 = l_Lean_Parser_Command_end___elambda__1___closed__1;
x_24 = l_Lean_Parser_ParserState_mkNode(x_22, x_23, x_7);
return x_24;
}
@ -23313,7 +23286,7 @@ lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean
x_25 = l_Lean_Parser_ParserState_restore(x_13, x_11, x_12);
x_26 = l_Lean_nullKind;
x_27 = l_Lean_Parser_ParserState_mkNode(x_25, x_26, x_11);
x_28 = l_Lean_Parser_Command_end___elambda__1___closed__2;
x_28 = l_Lean_Parser_Command_end___elambda__1___closed__1;
x_29 = l_Lean_Parser_ParserState_mkNode(x_27, x_28, x_7);
return x_29;
}
@ -23324,7 +23297,7 @@ else
lean_object* x_30; lean_object* x_31;
lean_dec(x_9);
lean_dec(x_1);
x_30 = l_Lean_Parser_Command_end___elambda__1___closed__2;
x_30 = l_Lean_Parser_Command_end___elambda__1___closed__1;
x_31 = l_Lean_Parser_ParserState_mkNode(x_8, x_30, x_7);
return x_31;
}
@ -23395,13 +23368,13 @@ lean_object* x_91; lean_object* x_92; uint8_t x_93;
x_91 = lean_ctor_get(x_90, 1);
lean_inc(x_91);
lean_dec(x_90);
x_92 = l_Lean_Parser_Command_end___elambda__1___closed__6;
x_92 = l_Lean_Parser_Command_end___elambda__1___closed__5;
x_93 = lean_string_dec_eq(x_91, x_92);
lean_dec(x_91);
if (x_93 == 0)
{
lean_object* x_94; lean_object* x_95;
x_94 = l_Lean_Parser_Command_end___elambda__1___closed__9;
x_94 = l_Lean_Parser_Command_end___elambda__1___closed__8;
lean_inc(x_49);
x_95 = l_Lean_Parser_ParserState_mkErrorsAt(x_87, x_94, x_49);
x_58 = x_95;
@ -23417,7 +23390,7 @@ else
{
lean_object* x_96; lean_object* x_97;
lean_dec(x_90);
x_96 = l_Lean_Parser_Command_end___elambda__1___closed__9;
x_96 = l_Lean_Parser_Command_end___elambda__1___closed__8;
lean_inc(x_49);
x_97 = l_Lean_Parser_ParserState_mkErrorsAt(x_87, x_96, x_49);
x_58 = x_97;
@ -23428,7 +23401,7 @@ else
{
lean_object* x_98; lean_object* x_99;
lean_dec(x_88);
x_98 = l_Lean_Parser_Command_end___elambda__1___closed__9;
x_98 = l_Lean_Parser_Command_end___elambda__1___closed__8;
lean_inc(x_49);
x_99 = l_Lean_Parser_ParserState_mkErrorsAt(x_87, x_98, x_49);
x_58 = x_99;
@ -23457,7 +23430,7 @@ lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean
lean_dec(x_62);
x_65 = l_Lean_nullKind;
x_66 = l_Lean_Parser_ParserState_mkNode(x_63, x_65, x_61);
x_67 = l_Lean_Parser_Command_end___elambda__1___closed__2;
x_67 = l_Lean_Parser_Command_end___elambda__1___closed__1;
x_68 = l_Lean_Parser_ParserState_mkNode(x_66, x_67, x_57);
x_69 = l_Lean_Parser_mergeOrElseErrors(x_68, x_52, x_49);
lean_dec(x_49);
@ -23477,7 +23450,7 @@ lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean
lean_dec(x_62);
x_72 = l_Lean_nullKind;
x_73 = l_Lean_Parser_ParserState_mkNode(x_63, x_72, x_61);
x_74 = l_Lean_Parser_Command_end___elambda__1___closed__2;
x_74 = l_Lean_Parser_Command_end___elambda__1___closed__1;
x_75 = l_Lean_Parser_ParserState_mkNode(x_73, x_74, x_57);
x_76 = l_Lean_Parser_mergeOrElseErrors(x_75, x_52, x_49);
lean_dec(x_49);
@ -23489,7 +23462,7 @@ lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; lean
x_77 = l_Lean_Parser_ParserState_restore(x_63, x_61, x_62);
x_78 = l_Lean_nullKind;
x_79 = l_Lean_Parser_ParserState_mkNode(x_77, x_78, x_61);
x_80 = l_Lean_Parser_Command_end___elambda__1___closed__2;
x_80 = l_Lean_Parser_Command_end___elambda__1___closed__1;
x_81 = l_Lean_Parser_ParserState_mkNode(x_79, x_80, x_57);
x_82 = l_Lean_Parser_mergeOrElseErrors(x_81, x_52, x_49);
lean_dec(x_49);
@ -23502,7 +23475,7 @@ else
lean_object* x_83; lean_object* x_84; lean_object* x_85;
lean_dec(x_59);
lean_dec(x_1);
x_83 = l_Lean_Parser_Command_end___elambda__1___closed__2;
x_83 = l_Lean_Parser_Command_end___elambda__1___closed__1;
x_84 = l_Lean_Parser_ParserState_mkNode(x_58, x_83, x_57);
x_85 = l_Lean_Parser_mergeOrElseErrors(x_84, x_52, x_49);
lean_dec(x_49);
@ -23519,7 +23492,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_Command_end___elambda__1___closed__6;
x_2 = l_Lean_Parser_Command_end___elambda__1___closed__5;
x_3 = l_Lean_Parser_symbolInfo(x_2, x_1);
return x_3;
}
@ -23538,7 +23511,7 @@ lean_object* _init_l_Lean_Parser_Command_end___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_end___elambda__1___closed__2;
x_1 = l_Lean_Parser_Command_end___elambda__1___closed__1;
x_2 = l_Lean_Parser_Command_end___closed__2;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
@ -23548,7 +23521,7 @@ lean_object* _init_l_Lean_Parser_Command_end___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Command_end___elambda__1___closed__4;
x_1 = l_Lean_Parser_Command_end___elambda__1___closed__3;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Command_end___closed__3;
@ -23589,7 +23562,7 @@ _start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l_Lean_Parser_regBuiltinCommandParserAttr___closed__4;
x_3 = l_Lean_Parser_Command_end___elambda__1___closed__2;
x_3 = l_Lean_Parser_Command_end___elambda__1___closed__1;
x_4 = 1;
x_5 = l_Lean_Parser_Command_end;
x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
@ -34173,10 +34146,6 @@ l_Lean_Parser_Term_stxQuot___elambda__1___closed__6 = _init_l_Lean_Parser_Term_s
lean_mark_persistent(l_Lean_Parser_Term_stxQuot___elambda__1___closed__6);
l_Lean_Parser_Term_stxQuot___elambda__1___closed__7 = _init_l_Lean_Parser_Term_stxQuot___elambda__1___closed__7();
lean_mark_persistent(l_Lean_Parser_Term_stxQuot___elambda__1___closed__7);
l_Lean_Parser_Term_stxQuot___elambda__1___closed__8 = _init_l_Lean_Parser_Term_stxQuot___elambda__1___closed__8();
lean_mark_persistent(l_Lean_Parser_Term_stxQuot___elambda__1___closed__8);
l_Lean_Parser_Term_stxQuot___elambda__1___closed__9 = _init_l_Lean_Parser_Term_stxQuot___elambda__1___closed__9();
lean_mark_persistent(l_Lean_Parser_Term_stxQuot___elambda__1___closed__9);
l_Lean_Parser_Term_stxQuot___closed__1 = _init_l_Lean_Parser_Term_stxQuot___closed__1();
lean_mark_persistent(l_Lean_Parser_Term_stxQuot___closed__1);
l_Lean_Parser_Term_stxQuot___closed__2 = _init_l_Lean_Parser_Term_stxQuot___closed__2();
@ -35395,8 +35364,6 @@ l_Lean_Parser_Command_end___elambda__1___closed__7 = _init_l_Lean_Parser_Command
lean_mark_persistent(l_Lean_Parser_Command_end___elambda__1___closed__7);
l_Lean_Parser_Command_end___elambda__1___closed__8 = _init_l_Lean_Parser_Command_end___elambda__1___closed__8();
lean_mark_persistent(l_Lean_Parser_Command_end___elambda__1___closed__8);
l_Lean_Parser_Command_end___elambda__1___closed__9 = _init_l_Lean_Parser_Command_end___elambda__1___closed__9();
lean_mark_persistent(l_Lean_Parser_Command_end___elambda__1___closed__9);
l_Lean_Parser_Command_end___closed__1 = _init_l_Lean_Parser_Command_end___closed__1();
lean_mark_persistent(l_Lean_Parser_Command_end___closed__1);
l_Lean_Parser_Command_end___closed__2 = _init_l_Lean_Parser_Command_end___closed__2();

30
stage0/stdlib/Init/Lean/Parser/Syntax.c
View file

@ -164,7 +164,6 @@ lean_object* l_Lean_Parser_quotedSymbolFn(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_syntax___elambda__1___closed__2;
extern lean_object* l_Lean_Parser_Level_addLit___elambda__1___closed__6;
lean_object* l___regBuiltinParser_Lean_Parser_Command_reserve(lean_object*);
extern lean_object* l_Lean_Parser_Term_stxQuot___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_identPrec;
lean_object* l_Lean_Parser_Command_infixl___closed__2;
lean_object* l_Lean_Parser_Syntax_many1___closed__4;
@ -174,7 +173,6 @@ lean_object* l_Lean_Parser_Command_strLitPrec___closed__2;
lean_object* l_Lean_Parser_Syntax_char___closed__2;
lean_object* l_Lean_Parser_Command_postfix___elambda__1___closed__8;
lean_object* l_Lean_Parser_Syntax_try___elambda__1___closed__8;
extern lean_object* l_Lean_Parser_Term_stxQuot___elambda__1___closed__9;
lean_object* l_Lean_Parser_Syntax_char___elambda__1___closed__5;
lean_object* l_Lean_Parser_Syntax_sepBy___closed__4;
lean_object* l_Lean_Parser_Command_macro___closed__5;
@ -189,6 +187,7 @@ lean_object* l_Lean_Parser_Syntax_str___elambda__1___closed__6;
lean_object* l_Lean_Parser_identEqFn(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_mixfix___elambda__1___closed__1;
lean_object* l_Lean_Parser_Command_mixfix___closed__8;
extern lean_object* l_Lean_Parser_Term_stxQuot___elambda__1___closed__4;
lean_object* l_Lean_Parser_Syntax_ident___closed__3;
lean_object* l_Lean_Parser_Command_macroArgSimple___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_macro__rules___closed__6;
@ -678,6 +677,7 @@ lean_object* l_Lean_Parser_Command_macro___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_macroTailCommand___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_maxPrec___closed__2;
lean_object* l_Lean_Parser_optPrecedence___closed__1;
extern lean_object* l_Lean_Parser_Term_stxQuot___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_reserve___closed__3;
uint8_t lean_string_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Syntax_orelse;
@ -13141,13 +13141,13 @@ lean_object* x_32; lean_object* x_33; uint8_t x_34;
x_32 = lean_ctor_get(x_31, 1);
lean_inc(x_32);
lean_dec(x_31);
x_33 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__6;
x_33 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__4;
x_34 = lean_string_dec_eq(x_32, x_33);
lean_dec(x_32);
if (x_34 == 0)
{
lean_object* x_35; lean_object* x_36;
x_35 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__9;
x_35 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__7;
x_36 = l_Lean_Parser_ParserState_mkErrorsAt(x_28, x_35, x_27);
x_3 = x_36;
goto block_22;
@ -13163,7 +13163,7 @@ else
{
lean_object* x_37; lean_object* x_38;
lean_dec(x_31);
x_37 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__9;
x_37 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__7;
x_38 = l_Lean_Parser_ParserState_mkErrorsAt(x_28, x_37, x_27);
x_3 = x_38;
goto block_22;
@ -13173,7 +13173,7 @@ else
{
lean_object* x_39; lean_object* x_40;
lean_dec(x_29);
x_39 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__9;
x_39 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__7;
x_40 = l_Lean_Parser_ParserState_mkErrorsAt(x_28, x_39, x_27);
x_3 = x_40;
goto block_22;
@ -13322,7 +13322,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__6;
x_2 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__4;
x_3 = l_Lean_Parser_symbolInfo(x_2, x_1);
return x_3;
}
@ -13637,13 +13637,13 @@ lean_object* x_53; lean_object* x_54; uint8_t x_55;
x_53 = lean_ctor_get(x_52, 1);
lean_inc(x_53);
lean_dec(x_52);
x_54 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__6;
x_54 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__4;
x_55 = lean_string_dec_eq(x_53, x_54);
lean_dec(x_53);
if (x_55 == 0)
{
lean_object* x_56; lean_object* x_57;
x_56 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__9;
x_56 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__7;
x_57 = l_Lean_Parser_ParserState_mkErrorsAt(x_49, x_56, x_48);
x_20 = x_57;
goto block_43;
@ -13659,7 +13659,7 @@ else
{
lean_object* x_58; lean_object* x_59;
lean_dec(x_52);
x_58 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__9;
x_58 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__7;
x_59 = l_Lean_Parser_ParserState_mkErrorsAt(x_49, x_58, x_48);
x_20 = x_59;
goto block_43;
@ -13669,7 +13669,7 @@ else
{
lean_object* x_60; lean_object* x_61;
lean_dec(x_50);
x_60 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__9;
x_60 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__7;
x_61 = l_Lean_Parser_ParserState_mkErrorsAt(x_49, x_60, x_48);
x_20 = x_61;
goto block_43;
@ -13979,13 +13979,13 @@ lean_object* x_46; lean_object* x_47; uint8_t x_48;
x_46 = lean_ctor_get(x_45, 1);
lean_inc(x_46);
lean_dec(x_45);
x_47 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__6;
x_47 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__4;
x_48 = lean_string_dec_eq(x_46, x_47);
lean_dec(x_46);
if (x_48 == 0)
{
lean_object* x_49; lean_object* x_50;
x_49 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__9;
x_49 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__7;
lean_inc(x_9);
x_50 = l_Lean_Parser_ParserState_mkErrorsAt(x_42, x_49, x_9);
x_21 = x_50;
@ -14001,7 +14001,7 @@ else
{
lean_object* x_51; lean_object* x_52;
lean_dec(x_45);
x_51 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__9;
x_51 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__7;
lean_inc(x_9);
x_52 = l_Lean_Parser_ParserState_mkErrorsAt(x_42, x_51, x_9);
x_21 = x_52;
@ -14012,7 +14012,7 @@ else
{
lean_object* x_53; lean_object* x_54;
lean_dec(x_43);
x_53 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__9;
x_53 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__7;
lean_inc(x_9);
x_54 = l_Lean_Parser_ParserState_mkErrorsAt(x_42, x_53, x_9);
x_21 = x_54;

2211
stage0/stdlib/Init/Lean/Parser/Tactic.c
View file

File diff suppressed because it is too large Load diff

3597
stage0/stdlib/Init/Lean/Parser/Term.c
View file

File diff suppressed because it is too large Load diff

521
stage0/stdlib/Init/Lean/Syntax.c
View file

@ -16,9 +16,9 @@ extern "C" {
lean_object* l_Lean_Syntax_reprint___main___closed__1;
lean_object* l_Lean_Syntax_formatStxAux___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_reprint___main___boxed(lean_object*);
lean_object* l___private_Init_Lean_Syntax_5__reprintLeaf(lean_object*, lean_object*);
lean_object* lean_array_set(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_Syntax_reprint___main___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Syntax_4__reprintLeaf(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Syntax_1__updateInfo(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_setTailInfoAux(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_reprint___boxed(lean_object*);
@ -30,10 +30,10 @@ lean_object* l_Lean_Syntax_ifNodeKind___rarg(lean_object*, lean_object*, lean_ob
uint8_t lean_name_eq(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_mrewriteBottomUp___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getIdAt(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Syntax_4__updateFirst___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_HasToString;
extern lean_object* l_Array_empty___closed__1;
lean_object* l_Lean_SyntaxNode_withArgs(lean_object*);
lean_object* l___private_Init_Lean_Syntax_4__reprintLeaf___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_reprint___main(lean_object*);
lean_object* l_Lean_Syntax_mrewriteBottomUp___main___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_mrewriteBottomUp(lean_object*);
@ -51,7 +51,9 @@ lean_object* l_Lean_Syntax_getNumArgs___boxed(lean_object*);
lean_object* l___private_Init_Lean_Syntax_3__updateLast___main___at_Lean_Syntax_setTailInfoAux___main___spec__1(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_mkAppStx___closed__4;
lean_object* l_Lean_mkAtom(lean_object*);
lean_object* l_Lean_Syntax_setHeadInfo(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_mreplace___main(lean_object*);
lean_object* l___private_Init_Lean_Syntax_4__updateFirst___main(lean_object*);
lean_object* l_Lean_Syntax_Lean_HasFormat(lean_object*);
lean_object* l_Lean_Syntax_truncateTrailing(lean_object*);
lean_object* l_Lean_Syntax_mreplace___rarg(lean_object*, lean_object*, lean_object*);
@ -69,6 +71,7 @@ lean_object* l_Lean_Syntax_getTailWithInfo___main(lean_object*);
lean_object* l_Lean_Syntax_formatStxAux___main___closed__4;
lean_object* l_Lean_SyntaxNode_getIdAt(lean_object*, lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l_Array_umapMAux___main___at_Lean_Syntax_replaceInfo___main___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_SyntaxNode_getKind___boxed(lean_object*);
lean_object* l_Lean_Syntax_formatStxAux___main___closed__2;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
@ -84,6 +87,8 @@ lean_object* l_List_map___main___at_Lean_Syntax_formatStxAux___main___spec__5___
lean_object* l_Lean_unreachIsNodeMissing(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getIdAt___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_formatStx___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_replaceInfo___main(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Syntax_4__updateFirst(lean_object*, lean_object*);
lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Syntax_3__updateLast(lean_object*);
lean_object* l_Lean_Syntax_updateLeading(lean_object*);
@ -101,6 +106,7 @@ lean_object* l_Lean_Syntax_formatStx(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_mreplace___main___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Function_comp___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_umapMAux___main___at_Lean_Syntax_rewriteBottomUp___spec__2(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_replaceInfo(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_isMissing___boxed(lean_object*);
lean_object* l_Lean_Syntax_mreplace(lean_object*);
lean_object* l___private_Init_Lean_Syntax_3__updateLast___main(lean_object*);
@ -142,6 +148,7 @@ lean_object* l_Lean_Syntax_setArg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_SourceInfo_updateTrailing(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Syntax_2__updateLeadingAux(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getTailWithInfo(lean_object*);
lean_object* l_Lean_Syntax_setHeadInfoAux___main(lean_object*, lean_object*);
lean_object* l_String_quote(lean_object*);
lean_object* l_Lean_Syntax_HasToString___closed__2;
lean_object* l_Lean_Syntax_mrewriteBottomUp___main___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
@ -150,6 +157,7 @@ extern lean_object* l_Lean_Format_sbracket___closed__1;
extern lean_object* l_Lean_Format_paren___closed__2;
lean_object* l_Lean_unreachIsNodeAtom___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Syntax_3__updateLast___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Syntax_4__updateFirst___main___at_Lean_Syntax_setHeadInfoAux___main___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_List_map___main___at_Lean_Syntax_formatStxAux___main___spec__4___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_findSomeRevMAux___main___at_Lean_Syntax_getTailWithInfo___main___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_setTailInfoAux___main(lean_object*, lean_object*);
@ -162,6 +170,7 @@ lean_object* l_Array_iterateMAux___main___at_Lean_Syntax_reprint___main___spec__
lean_object* l_Array_umapMAux___main___at_Lean_Syntax_updateLeading___spec__2(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_HasToString___closed__1;
extern lean_object* l_Lean_mkOptionalNode___closed__1;
lean_object* l___private_Init_Lean_Syntax_4__updateFirst___main___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_mrewriteBottomUp___main(lean_object*);
lean_object* l_Lean_SyntaxNode_getIdAt___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getTailInfo(lean_object*);
@ -188,13 +197,16 @@ lean_object* l_Lean_Syntax_mrewriteBottomUp___main___rarg___lambda__2(lean_objec
lean_object* l_Lean_Syntax_ifNodeKind___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_modifyArgs(lean_object*, lean_object*);
lean_object* l_Lean_mkNode(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Syntax_5__reprintLeaf___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getTailInfo___main(lean_object*);
lean_object* l_Lean_SyntaxNode_getArg(lean_object*, lean_object*);
lean_object* l_Lean_Format_joinSep___main___at_Lean_Syntax_formatStxAux___main___spec__2___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_formatStxAux___main___closed__7;
lean_object* l_Lean_Syntax_formatStxAux(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_reprint(lean_object*);
lean_object* l_Lean_Syntax_setHeadInfoAux(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_mreplace___main___rarg___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Syntax_4__updateFirst___rarg(lean_object*, lean_object*, lean_object*);
uint8_t lean_string_dec_eq(lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_Lean_SourceInfo_updateTrailing(lean_object* x_1, lean_object* x_2) {
@ -2927,7 +2939,502 @@ return x_10;
}
}
}
lean_object* l___private_Init_Lean_Syntax_4__reprintLeaf(lean_object* x_1, lean_object* x_2) {
lean_object* l___private_Init_Lean_Syntax_4__updateFirst___main___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; uint8_t x_5;
x_4 = lean_array_get_size(x_1);
x_5 = lean_nat_dec_lt(x_3, x_4);
lean_dec(x_4);
if (x_5 == 0)
{
lean_object* x_6;
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_6 = lean_box(0);
return x_6;
}
else
{
lean_object* x_7; lean_object* x_8;
x_7 = lean_array_fget(x_1, x_3);
lean_inc(x_2);
x_8 = lean_apply_1(x_2, x_7);
if (lean_obj_tag(x_8) == 0)
{
lean_object* x_9; lean_object* x_10;
x_9 = lean_unsigned_to_nat(1u);
x_10 = lean_nat_add(x_3, x_9);
lean_dec(x_3);
x_3 = x_10;
goto _start;
}
else
{
uint8_t x_12;
lean_dec(x_2);
x_12 = !lean_is_exclusive(x_8);
if (x_12 == 0)
{
lean_object* x_13; lean_object* x_14;
x_13 = lean_ctor_get(x_8, 0);
x_14 = lean_array_fset(x_1, x_3, x_13);
lean_dec(x_3);
lean_ctor_set(x_8, 0, x_14);
return x_8;
}
else
{
lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_15 = lean_ctor_get(x_8, 0);
lean_inc(x_15);
lean_dec(x_8);
x_16 = lean_array_fset(x_1, x_3, x_15);
lean_dec(x_3);
x_17 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_17, 0, x_16);
return x_17;
}
}
}
}
}
lean_object* l___private_Init_Lean_Syntax_4__updateFirst___main(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l___private_Init_Lean_Syntax_4__updateFirst___main___rarg), 3, 0);
return x_2;
}
}
lean_object* l___private_Init_Lean_Syntax_4__updateFirst___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l___private_Init_Lean_Syntax_4__updateFirst___main___rarg(x_1, x_2, x_3);
return x_4;
}
}
lean_object* l___private_Init_Lean_Syntax_4__updateFirst(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l___private_Init_Lean_Syntax_4__updateFirst___rarg), 3, 0);
return x_3;
}
}
lean_object* l___private_Init_Lean_Syntax_4__updateFirst___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l___private_Init_Lean_Syntax_4__updateFirst(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
lean_object* l___private_Init_Lean_Syntax_4__updateFirst___main___at_Lean_Syntax_setHeadInfoAux___main___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; uint8_t x_5;
x_4 = lean_array_get_size(x_2);
x_5 = lean_nat_dec_lt(x_3, x_4);
lean_dec(x_4);
if (x_5 == 0)
{
lean_object* x_6;
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_6 = lean_box(0);
return x_6;
}
else
{
lean_object* x_7; lean_object* x_8;
x_7 = lean_array_fget(x_2, x_3);
lean_inc(x_1);
x_8 = l_Lean_Syntax_setHeadInfoAux___main(x_1, x_7);
if (lean_obj_tag(x_8) == 0)
{
lean_object* x_9; lean_object* x_10;
x_9 = lean_unsigned_to_nat(1u);
x_10 = lean_nat_add(x_3, x_9);
lean_dec(x_3);
x_3 = x_10;
goto _start;
}
else
{
uint8_t x_12;
lean_dec(x_1);
x_12 = !lean_is_exclusive(x_8);
if (x_12 == 0)
{
lean_object* x_13; lean_object* x_14;
x_13 = lean_ctor_get(x_8, 0);
x_14 = lean_array_fset(x_2, x_3, x_13);
lean_dec(x_3);
lean_ctor_set(x_8, 0, x_14);
return x_8;
}
else
{
lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_15 = lean_ctor_get(x_8, 0);
lean_inc(x_15);
lean_dec(x_8);
x_16 = lean_array_fset(x_2, x_3, x_15);
lean_dec(x_3);
x_17 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_17, 0, x_16);
return x_17;
}
}
}
}
}
lean_object* l_Lean_Syntax_setHeadInfoAux___main(lean_object* x_1, lean_object* x_2) {
_start:
{
switch (lean_obj_tag(x_2)) {
case 0:
{
lean_object* x_3;
lean_dec(x_1);
x_3 = lean_box(0);
return x_3;
}
case 1:
{
uint8_t x_4;
x_4 = !lean_is_exclusive(x_2);
if (x_4 == 0)
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_5 = lean_ctor_get(x_2, 0);
x_6 = lean_ctor_get(x_2, 1);
x_7 = lean_array_get_size(x_6);
x_8 = l___private_Init_Lean_Syntax_4__updateFirst___main___at_Lean_Syntax_setHeadInfoAux___main___spec__1(x_1, x_6, x_7);
if (lean_obj_tag(x_8) == 0)
{
lean_object* x_9;
lean_free_object(x_2);
lean_dec(x_5);
x_9 = lean_box(0);
return x_9;
}
else
{
uint8_t x_10;
x_10 = !lean_is_exclusive(x_8);
if (x_10 == 0)
{
lean_object* x_11;
x_11 = lean_ctor_get(x_8, 0);
lean_ctor_set(x_2, 1, x_11);
lean_ctor_set(x_8, 0, x_2);
return x_8;
}
else
{
lean_object* x_12; lean_object* x_13;
x_12 = lean_ctor_get(x_8, 0);
lean_inc(x_12);
lean_dec(x_8);
lean_ctor_set(x_2, 1, x_12);
x_13 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_13, 0, x_2);
return x_13;
}
}
}
else
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_14 = lean_ctor_get(x_2, 0);
x_15 = lean_ctor_get(x_2, 1);
lean_inc(x_15);
lean_inc(x_14);
lean_dec(x_2);
x_16 = lean_array_get_size(x_15);
x_17 = l___private_Init_Lean_Syntax_4__updateFirst___main___at_Lean_Syntax_setHeadInfoAux___main___spec__1(x_1, x_15, x_16);
if (lean_obj_tag(x_17) == 0)
{
lean_object* x_18;
lean_dec(x_14);
x_18 = lean_box(0);
return x_18;
}
else
{
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_19 = lean_ctor_get(x_17, 0);
lean_inc(x_19);
if (lean_is_exclusive(x_17)) {
lean_ctor_release(x_17, 0);
x_20 = x_17;
} else {
lean_dec_ref(x_17);
x_20 = lean_box(0);
}
x_21 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_21, 0, x_14);
lean_ctor_set(x_21, 1, x_19);
if (lean_is_scalar(x_20)) {
x_22 = lean_alloc_ctor(1, 1, 0);
} else {
x_22 = x_20;
}
lean_ctor_set(x_22, 0, x_21);
return x_22;
}
}
}
case 2:
{
uint8_t x_23;
x_23 = !lean_is_exclusive(x_2);
if (x_23 == 0)
{
lean_object* x_24; lean_object* x_25;
x_24 = lean_ctor_get(x_2, 0);
lean_dec(x_24);
lean_ctor_set(x_2, 0, x_1);
x_25 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_25, 0, x_2);
return x_25;
}
else
{
lean_object* x_26; lean_object* x_27; lean_object* x_28;
x_26 = lean_ctor_get(x_2, 1);
lean_inc(x_26);
lean_dec(x_2);
x_27 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_27, 0, x_1);
lean_ctor_set(x_27, 1, x_26);
x_28 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_28, 0, x_27);
return x_28;
}
}
default:
{
uint8_t x_29;
x_29 = !lean_is_exclusive(x_2);
if (x_29 == 0)
{
lean_object* x_30; lean_object* x_31;
x_30 = lean_ctor_get(x_2, 0);
lean_dec(x_30);
lean_ctor_set(x_2, 0, x_1);
x_31 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_31, 0, x_2);
return x_31;
}
else
{
lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36;
x_32 = lean_ctor_get(x_2, 1);
x_33 = lean_ctor_get(x_2, 2);
x_34 = lean_ctor_get(x_2, 3);
lean_inc(x_34);
lean_inc(x_33);
lean_inc(x_32);
lean_dec(x_2);
x_35 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_35, 0, x_1);
lean_ctor_set(x_35, 1, x_32);
lean_ctor_set(x_35, 2, x_33);
lean_ctor_set(x_35, 3, x_34);
x_36 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_36, 0, x_35);
return x_36;
}
}
}
}
}
lean_object* l_Lean_Syntax_setHeadInfoAux(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_Syntax_setHeadInfoAux___main(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Syntax_setHeadInfo(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
lean_inc(x_1);
x_3 = l_Lean_Syntax_setHeadInfoAux___main(x_2, x_1);
if (lean_obj_tag(x_3) == 0)
{
return x_1;
}
else
{
lean_object* x_4;
lean_dec(x_1);
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
lean_dec(x_3);
return x_4;
}
}
}
lean_object* l_Array_umapMAux___main___at_Lean_Syntax_replaceInfo___main___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; uint8_t x_5;
x_4 = lean_array_get_size(x_3);
x_5 = lean_nat_dec_lt(x_2, x_4);
lean_dec(x_4);
if (x_5 == 0)
{
lean_object* x_6; lean_object* x_7;
lean_dec(x_2);
lean_dec(x_1);
x_6 = l_Array_empty___closed__1;
x_7 = x_3;
return x_7;
}
else
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
x_8 = lean_array_fget(x_3, x_2);
x_9 = lean_box(0);
x_10 = x_9;
x_11 = lean_array_fset(x_3, x_2, x_10);
lean_inc(x_8);
lean_inc(x_1);
x_12 = l_Lean_Syntax_replaceInfo___main(x_1, x_8);
x_13 = lean_unsigned_to_nat(1u);
x_14 = lean_nat_add(x_2, x_13);
x_15 = x_12;
lean_dec(x_8);
x_16 = lean_array_fset(x_11, x_2, x_15);
lean_dec(x_2);
x_2 = x_14;
x_3 = x_16;
goto _start;
}
}
}
lean_object* l_Lean_Syntax_replaceInfo___main(lean_object* x_1, lean_object* x_2) {
_start:
{
switch (lean_obj_tag(x_2)) {
case 0:
{
lean_dec(x_1);
return x_2;
}
case 1:
{
uint8_t x_3;
x_3 = !lean_is_exclusive(x_2);
if (x_3 == 0)
{
lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = lean_ctor_get(x_2, 1);
x_5 = lean_unsigned_to_nat(0u);
x_6 = l_Array_umapMAux___main___at_Lean_Syntax_replaceInfo___main___spec__1(x_1, x_5, x_4);
lean_ctor_set(x_2, 1, x_6);
return x_2;
}
else
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_7 = lean_ctor_get(x_2, 0);
x_8 = lean_ctor_get(x_2, 1);
lean_inc(x_8);
lean_inc(x_7);
lean_dec(x_2);
x_9 = lean_unsigned_to_nat(0u);
x_10 = l_Array_umapMAux___main___at_Lean_Syntax_replaceInfo___main___spec__1(x_1, x_9, x_8);
x_11 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_11, 0, x_7);
lean_ctor_set(x_11, 1, x_10);
return x_11;
}
}
case 2:
{
uint8_t x_12;
x_12 = !lean_is_exclusive(x_2);
if (x_12 == 0)
{
lean_object* x_13; lean_object* x_14;
x_13 = lean_ctor_get(x_2, 0);
lean_dec(x_13);
x_14 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_14, 0, x_1);
lean_ctor_set(x_2, 0, x_14);
return x_2;
}
else
{
lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_15 = lean_ctor_get(x_2, 1);
lean_inc(x_15);
lean_dec(x_2);
x_16 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_16, 0, x_1);
x_17 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set(x_17, 1, x_15);
return x_17;
}
}
default:
{
uint8_t x_18;
x_18 = !lean_is_exclusive(x_2);
if (x_18 == 0)
{
lean_object* x_19; lean_object* x_20;
x_19 = lean_ctor_get(x_2, 0);
lean_dec(x_19);
x_20 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_20, 0, x_1);
lean_ctor_set(x_2, 0, x_20);
return x_2;
}
else
{
lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_21 = lean_ctor_get(x_2, 1);
x_22 = lean_ctor_get(x_2, 2);
x_23 = lean_ctor_get(x_2, 3);
lean_inc(x_23);
lean_inc(x_22);
lean_inc(x_21);
lean_dec(x_2);
x_24 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_24, 0, x_1);
x_25 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_25, 0, x_24);
lean_ctor_set(x_25, 1, x_21);
lean_ctor_set(x_25, 2, x_22);
lean_ctor_set(x_25, 3, x_23);
return x_25;
}
}
}
}
}
lean_object* l_Lean_Syntax_replaceInfo(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_Syntax_replaceInfo___main(x_1, x_2);
return x_3;
}
}
lean_object* l___private_Init_Lean_Syntax_5__reprintLeaf(lean_object* x_1, lean_object* x_2) {
_start:
{
if (lean_obj_tag(x_1) == 0)
@ -2959,11 +3466,11 @@ return x_18;
}
}
}
lean_object* l___private_Init_Lean_Syntax_4__reprintLeaf___boxed(lean_object* x_1, lean_object* x_2) {
lean_object* l___private_Init_Lean_Syntax_5__reprintLeaf___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l___private_Init_Lean_Syntax_4__reprintLeaf(x_1, x_2);
x_3 = l___private_Init_Lean_Syntax_5__reprintLeaf(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
@ -3153,7 +3660,7 @@ case 2:
lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24;
x_21 = lean_ctor_get(x_1, 0);
x_22 = lean_ctor_get(x_1, 1);
x_23 = l___private_Init_Lean_Syntax_4__reprintLeaf(x_21, x_22);
x_23 = l___private_Init_Lean_Syntax_5__reprintLeaf(x_21, x_22);
x_24 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_24, 0, x_23);
return x_24;
@ -3167,7 +3674,7 @@ x_27 = lean_ctor_get(x_25, 0);
x_28 = lean_ctor_get(x_25, 1);
x_29 = lean_ctor_get(x_25, 2);
x_30 = lean_string_utf8_extract(x_27, x_28, x_29);
x_31 = l___private_Init_Lean_Syntax_4__reprintLeaf(x_26, x_30);
x_31 = l___private_Init_Lean_Syntax_5__reprintLeaf(x_26, x_30);
lean_dec(x_30);
x_32 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_32, 0, x_31);

28
stage0/stdlib/Init/LeanInit.c
View file

@ -216,6 +216,7 @@ lean_object* l_Lean_ParserDescr_inhabited___closed__1;
lean_object* l_Lean_NameGenerator_mkChild(lean_object*);
lean_object* l_Lean_Syntax_isCharLit_x3f___boxed(lean_object*);
lean_object* l___private_Init_LeanInit_2__assembleParts(lean_object*, lean_object*);
lean_object* l_Lean_SourceInfo_inhabited;
size_t lean_usize_of_nat(lean_object*);
lean_object* l_Lean_nullKind___closed__1;
lean_object* l_Lean_Syntax_decodeStrLit___boxed(lean_object*);
@ -243,6 +244,7 @@ lean_object* l_Lean_identKind;
lean_object* l_Lean_mkCTermId(lean_object*);
uint8_t l_UInt32_decEq(uint32_t, uint32_t);
lean_object* l_Lean_Syntax_inhabited;
extern lean_object* l_Substring_drop___closed__2;
lean_object* l_Lean_Macro_throwError___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkAppStx___closed__5;
lean_object* l_Lean_Macro_throwError___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -252,6 +254,7 @@ lean_object* l___private_Init_LeanInit_3__extractImported(lean_object*, lean_obj
lean_object* l___private_Init_LeanInit_5__extractMacroScopesAux___main(lean_object*, lean_object*);
uint8_t l_Lean_Syntax_hasArgs(lean_object*);
lean_object* l_Lean_monadQuotationTrans___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_SourceInfo_inhabited___closed__1;
lean_object* l_String_quote(lean_object*);
uint8_t l_Char_isAlphanum(uint32_t);
lean_object* l___private_Init_LeanInit_12__decodeQuotedChar(lean_object*, lean_object*);
@ -1523,6 +1526,27 @@ x_1 = l_Lean_ParserDescr_inhabited___closed__1;
return x_1;
}
}
lean_object* _init_l_Lean_SourceInfo_inhabited___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Substring_drop___closed__2;
x_2 = lean_unsigned_to_nat(0u);
x_3 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
lean_ctor_set(x_3, 2, x_1);
return x_3;
}
}
lean_object* _init_l_Lean_SourceInfo_inhabited() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_SourceInfo_inhabited___closed__1;
return x_1;
}
}
lean_object* _init_l_Lean_Syntax_inhabited() {
_start:
{
@ -6751,6 +6775,10 @@ l_Lean_ParserDescr_inhabited___closed__1 = _init_l_Lean_ParserDescr_inhabited___
lean_mark_persistent(l_Lean_ParserDescr_inhabited___closed__1);
l_Lean_ParserDescr_inhabited = _init_l_Lean_ParserDescr_inhabited();
lean_mark_persistent(l_Lean_ParserDescr_inhabited);
l_Lean_SourceInfo_inhabited___closed__1 = _init_l_Lean_SourceInfo_inhabited___closed__1();
lean_mark_persistent(l_Lean_SourceInfo_inhabited___closed__1);
l_Lean_SourceInfo_inhabited = _init_l_Lean_SourceInfo_inhabited();
lean_mark_persistent(l_Lean_SourceInfo_inhabited);
l_Lean_Syntax_inhabited = _init_l_Lean_Syntax_inhabited();
lean_mark_persistent(l_Lean_Syntax_inhabited);
l_Lean_choiceKind___closed__1 = _init_l_Lean_choiceKind___closed__1();