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

chore: update stage0

Browse source
This commit is contained in:
Sebastian Ullrich 2021-01-15 15:06:25 +01:00
parent d1ff0991f4
commit d5ddcacc84
36 changed files with 13350 additions and 12141 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
stage0/src/Init/Data/UInt.lean generated
View file

@ -43,6 +43,11 @@ instance : Div UInt8 := ⟨UInt8.div⟩
instance : HasLess UInt8 := ⟨UInt8.lt⟩
instance : HasLessEq UInt8 := ⟨UInt8.le⟩
@[extern c inline "#1 << #2"]
constant UInt8.shiftLeft (a b : UInt8) : UInt8
@[extern c inline "#1 >> #2"]
constant UInt8.shiftRight (a b : UInt8) : UInt8
set_option bootstrap.gen_matcher_code false in
@[extern c inline "#1 < #2"]
def UInt8.decLt (a b : UInt8) : Decidable (a < b) :=
@ -93,6 +98,11 @@ instance : Div UInt16 := ⟨UInt16.div⟩
instance : HasLess UInt16 := ⟨UInt16.lt⟩
instance : HasLessEq UInt16 := ⟨UInt16.le⟩
@[extern c inline "#1 << #2"]
constant UInt16.shiftLeft (a b : UInt16) : UInt16
@[extern c inline "#1 >> #2"]
constant UInt16.shiftRight (a b : UInt16) : UInt16
set_option bootstrap.gen_matcher_code false in
@[extern c inline "#1 < #2"]
def UInt16.decLt (a b : UInt16) : Decidable (a < b) :=

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

@ -229,8 +229,45 @@ def copyInfo (s : Syntax) (source : Syntax) : Syntax :=
let s := s.copyHeadInfo source
s.copyTailInfo source
/--
Copy head and tail position information from `source` to `s`.
`leading` and `trailing` information is not preserved. -/
def copyRangePos (s : Syntax) (source : Syntax) : Syntax :=
match source.getPos with
| none => s
| some pos =>
let s := s.setHeadInfo { pos := pos }
match source.getTailInfo with
| some { pos := some pos, .. } =>
let s := s.setTailInfo { pos := pos }
/- The trailing token at `s` may be different from `source`.
So, we retrieve the tail positions and adjust `pos` to make sure the `s.getTailPos == source.getTailPos`. -/
match source.getTailPos, s.getTailPos with
| some pos₁, some pos₂ =>
if pos₁ < pos₂ then
s.setTailInfo { pos := some ((pos : Nat) - (pos₂ - pos₁) : Nat) }
else if pos₁ > pos₂ then
s.setTailInfo { pos := some ((pos : Nat) + (pos₁ - pos₂) : Nat) }
else
s
| _, _ => s
| _ => s
/-- Return the first atom/identifier that has position information -/
partial def getHead? : Syntax → Option Syntax
| stx@(atom { pos := some _, .. } ..) => some stx
| stx@(ident { pos := some _, .. } ..) => some stx
| node _ args => args.findSome? getHead?
| _ => none
end Syntax
/-- Use the head atom/identifier of the current `ref` as the `ref` -/
@[inline] def withHeadRefOnly {m : Type → Type} [Monad m] [MonadRef m] {α} (x : m α) : m α := do
match (← getRef).getHead? with
| none => x
| some ref => withRef ref x
def mkAtom (val : String) : Syntax :=
Syntax.atom {} val

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

@ -532,7 +532,7 @@ private partial def findMethod? (env : Environment) (structName fieldName : Name
private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM LValResolution := do
match eType.getAppFn, lval with
| Expr.const structName _ _, LVal.fieldIdx idx =>
| Expr.const structName _ _, LVal.fieldIdx _ idx =>
if idx == 0 then
throwError "invalid projection, index must be greater than 0"
let env ← getEnv
@ -548,7 +548,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
pure $ LValResolution.projIdx structName (idx - 1)
else
throwLValError e eType m!"invalid projection, structure has only {fieldNames.size} field(s)"
| Expr.const structName _ _, LVal.fieldName fieldName =>
| Expr.const structName _ _, LVal.fieldName _ fieldName =>
let env ← getEnv
let searchEnv : Unit → TermElabM LValResolution := fun _ => do
match findMethod? env structName (Name.mkSimple fieldName) with
@ -576,13 +576,13 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
| none => searchCtx ()
else
searchCtx ()
| Expr.const structName _ _, LVal.getOp idx =>
| Expr.const structName _ _, LVal.getOp _ idx =>
let env ← getEnv
let fullName := Name.mkStr structName "getOp"
match env.find? fullName with
| some _ => pure $ LValResolution.getOp fullName idx
| none => throwLValError e eType m!"invalid [..] notation because environment does not contain '{fullName}'"
| _, LVal.getOp idx =>
| _, LVal.getOp _ idx =>
throwLValError e eType "invalid [..] notation, type is not of the form (C ...) where C is a constant"
| _, _ =>
throwLValError e eType "invalid field notation, type is not of the form (C ...) where C is a constant"
@ -690,10 +690,12 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
match lvalRes with
| LValResolution.projIdx structName idx =>
let f := mkProj structName idx f
addTermInfo lval.getRef f
loop f lvals
| LValResolution.projFn baseStructName structName fieldName =>
let f ← mkBaseProjections baseStructName structName f
let projFn ← mkConst (baseStructName ++ fieldName)
addTermInfo lval.getRef projFn
if lvals.isEmpty then
let namedArgs ← addNamedArg namedArgs { name := `self, val := Arg.expr f }
elabAppArgs projFn namedArgs args expectedType? explicit ellipsis
@ -703,6 +705,7 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
| LValResolution.const baseStructName structName constName =>
let f ← if baseStructName != structName then mkBaseProjections baseStructName structName f else pure f
let projFn ← mkConst constName
addTermInfo lval.getRef projFn
if lvals.isEmpty then
let projFnType ← inferType projFn
let (args, namedArgs) ← addLValArg baseStructName constName f args namedArgs projFnType
@ -711,6 +714,7 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
let f ← elabAppArgs projFn #[] #[Arg.expr f] (expectedType? := none) (explicit := false) (ellipsis := false)
loop f lvals
| LValResolution.localRec baseName fullName fvar =>
addTermInfo lval.getRef fvar
if lvals.isEmpty then
let fvarType ← inferType fvar
let (args, namedArgs) ← addLValArg baseName fullName f args namedArgs fvarType
@ -720,6 +724,7 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
loop f lvals
| LValResolution.getOp fullName idx =>
let getOpFn ← mkConst fullName
addTermInfo lval.getRef getOpFn
if lvals.isEmpty then
let namedArgs ← addNamedArg namedArgs { name := `self, val := Arg.expr f }
let namedArgs ← addNamedArg namedArgs { name := `idx, val := Arg.stx idx }
@ -770,7 +775,9 @@ private partial def elabAppFnId (fIdent : Syntax) (fExplicitUnivs : List Level)
-- Set `errToSorry` to `false` if `funLVals` > 1. See comment above about the interaction between `errToSorry` and `observing`.
withReader (fun ctx => { ctx with errToSorry := funLVals.length == 1 && ctx.errToSorry }) do
funLVals.foldlM (init := acc) fun acc ⟨f, fields⟩ => do
let lvals' := fields.map LVal.fieldName
unless lvals.isEmpty && args.isEmpty && namedArgs.isEmpty do
addTermInfo fIdent f
let lvals' := fields.map (LVal.fieldName fIdent)
let s ← observing do
let e ← elabAppLVals f (lvals' ++ lvals) namedArgs args expectedType? explicit ellipsis
if overloaded then ensureHasType expectedType? e else pure e
@ -784,17 +791,17 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
withReader (fun ctx => { ctx with errToSorry := false }) do
f.getArgs.foldlM (fun acc f => elabAppFn f lvals namedArgs args expectedType? explicit ellipsis true acc) acc
else match f with
| `($(e).$idx:fieldIdx) =>
let idx := idx.isFieldIdx?.get!
elabAppFn e (LVal.fieldIdx idx :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
| `($(e).$idxStx:fieldIdx) =>
let idx := idxStx.isFieldIdx?.get!
elabAppFn e (LVal.fieldIdx idxStx idx :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
| `($e |>. $field) => do
let f ← `($(e).$field)
elabAppFn f lvals namedArgs args expectedType? explicit ellipsis overloaded acc
| `($(e).$field:ident) =>
let newLVals := field.getId.eraseMacroScopes.components.map (fun n => LVal.fieldName (toString n))
let newLVals := field.getId.eraseMacroScopes.components.map (fun n => LVal.fieldName field (toString n))
elabAppFn e (newLVals ++ lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
| `($e[$idx]) =>
elabAppFn e (LVal.getOp idx :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
| `($e[%$bracket $idx]) =>
elabAppFn e (LVal.getOp bracket idx :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
| `($id:ident@$t:term) =>
throwError "unexpected occurrence of named pattern"
| `($id:ident) => do

28
stage0/src/Lean/Elab/Binders.lean generated
View file

@ -144,6 +144,13 @@ private def matchBinder (stx : Syntax) : TermElabM (Array BinderView) :=
private def registerFailedToInferBinderTypeInfo (type : Expr) (ref : Syntax) : TermElabM Unit :=
registerCustomErrorIfMVar type ref "failed to infer binder type"
private def addLocalVarInfoCore (lctx : LocalContext) (stx : Syntax) (fvar : Expr) : TermElabM Unit := do
if (← getInfoState).enabled then
pushInfoTree <| InfoTree.node (children := {}) <| Info.ofTermInfo { lctx := lctx, expr := fvar, stx := stx }
private def addLocalVarInfo (stx : Syntax) (fvar : Expr) : TermElabM Unit := do
addLocalVarInfoCore (← getLCtx) stx fvar
private partial def elabBinderViews {α} (binderViews : Array BinderView) (catchAutoBoundImplicit : Bool) (fvars : Array Expr) (k : Array Expr → TermElabM α)
: TermElabM α :=
let rec loop (i : Nat) (fvars : Array Expr) : TermElabM α := do
@ -152,12 +159,14 @@ private partial def elabBinderViews {α} (binderViews : Array BinderView) (catch
if catchAutoBoundImplicit then
elabTypeWithAutoBoundImplicit binderView.type fun type => do
registerFailedToInferBinderTypeInfo type binderView.type
withLocalDecl binderView.id.getId binderView.bi type fun fvar =>
withLocalDecl binderView.id.getId binderView.bi type fun fvar => do
addLocalVarInfo binderView.id fvar
loop (i+1) (fvars.push fvar)
else
let type ← elabType binderView.type
registerFailedToInferBinderTypeInfo type binderView.type
withLocalDecl binderView.id.getId binderView.bi type fun fvar =>
withLocalDecl binderView.id.getId binderView.bi type fun fvar => do
addLocalVarInfo binderView.id fvar
loop (i+1) (fvars.push fvar)
else
k fvars
@ -321,6 +330,7 @@ private partial def elabFunBinderViews (binderViews : Array BinderView) (i : Nat
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
addLocalVarInfoCore lctx binderView.id fvar
let s ← withRef binderView.id $ propagateExpectedType fvar type s
let s := { s with lctx := lctx }
match (← isClass? type) with
@ -480,7 +490,7 @@ def expandMatchAltsWhereDecls (matchAltsWhereDecls : Syntax) : MacroM Syntax :=
The default elaboration order is `binders`, `typeStx`, `valStx`, and `body`.
If `elabBodyFirst == true`, then we use the order `binders`, `typeStx`, `body`, and `valStx`. -/
def elabLetDeclAux (n : Name) (binders : Array Syntax) (typeStx : Syntax) (valStx : Syntax) (body : Syntax)
def elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx : Syntax) (valStx : Syntax) (body : Syntax)
(expectedType? : Option Expr) (useLetExpr : Bool) (elabBodyFirst : Bool) : TermElabM Expr := do
let (type, val, arity) ← elabBinders binders fun xs => do
let type ← elabType typeStx
@ -494,15 +504,17 @@ def elabLetDeclAux (n : Name) (binders : Array Syntax) (typeStx : Syntax) (valSt
let type ← mkForallFVars xs type
let val ← mkLambdaFVars xs val
pure (type, val, xs.size)
trace[Elab.let.decl]! "{n} : {type} := {val}"
trace[Elab.let.decl]! "{id.getId} : {type} := {val}"
let result ←
if useLetExpr then
withLetDecl n type val fun x => do
withLetDecl id.getId type val fun x => do
addLocalVarInfo id x
let body ← elabTerm body expectedType?
let body ← instantiateMVars body
mkLetFVars #[x] body
else
let f ← withLocalDecl n BinderInfo.default type fun x => do
let f ← withLocalDecl id.getId BinderInfo.default type fun x => do
addLocalVarInfo id x
let body ← elabTerm body expectedType?
let body ← instantiateMVars body
mkLambdaFVars #[x] body
@ -516,14 +528,14 @@ def elabLetDeclAux (n : Name) (binders : Array Syntax) (typeStx : Syntax) (valSt
pure result
structure LetIdDeclView where
id : Name
id : Syntax
binders : Array Syntax
type : Syntax
value : Syntax
def mkLetIdDeclView (letIdDecl : Syntax) : LetIdDeclView :=
-- `letIdDecl` is of the form `ident >> many bracketedBinder >> optType >> " := " >> termParser
let id := letIdDecl[0].getId
let id := letIdDecl[0]
let binders := letIdDecl[1].getArgs
let optType := letIdDecl[2]
let type := expandOptType letIdDecl optType

4
stage0/src/Lean/Elab/Command.lean generated
View file

@ -287,7 +287,9 @@ def liftTermElabM {α} (declName? : Option Name) (x : TermElabM α) : CommandEla
let (((ea, termS), metaS), coreS) ← liftEIO x
let infoTrees := termS.infoState.trees.map fun tree =>
let tree := tree.substitute termS.infoState.assignment
InfoTree.context { env := coreS.env, mctx := metaS.mctx, currNamespace := scope.currNamespace, openDecls := scope.openDecls, options := scope.opts } tree
InfoTree.context {
env := coreS.env, fileMap := ctx.fileMap, mctx := metaS.mctx, currNamespace := scope.currNamespace, openDecls := scope.openDecls, options := scope.opts
} tree
modify fun s => { s with
env := coreS.env
messages := addTraceAsMessages ctx (s.messages ++ termS.messages) coreS.traceState

9
stage0/src/Lean/Elab/Do.lean generated
View file

@ -862,7 +862,7 @@ def actionTerminalToTerm (action : Syntax) : M Syntax := do
let r ← actionTerminalToTermCore action
pure $ r.copyInfo ref
def seqToTermCore (action : Syntax) (k : Syntax) : MacroM Syntax := withFreshMacroScope do
def seqToTermCore (action : Syntax) (k : Syntax) : M Syntax := withFreshMacroScope do
if action.getKind == `Lean.Parser.Term.doDbgTrace then
let msg := action[1]
`(dbgTrace! $msg; $k)
@ -870,9 +870,10 @@ def seqToTermCore (action : Syntax) (k : Syntax) : MacroM Syntax := withFreshMac
let cond := action[1]
`(assert! $cond; $k)
else
let action := Syntax.copyRangePos (← `(($action : $((←read).m) PUnit))) action
`(Bind.bind $action (fun (_ : PUnit) => $k))
def seqToTerm (action : Syntax) (k : Syntax) : MacroM Syntax := do
def seqToTerm (action : Syntax) (k : Syntax) : M Syntax := do
let r ← seqToTermCore action k
return r.copyInfo action
@ -894,7 +895,9 @@ def declToTermCore (decl : Syntax) (k : Syntax) : M Syntax := withFreshMacroScop
let doElem := arg[3]
-- `doElem` must be a `doExpr action`. See `doLetArrowToCode`
match isDoExpr? doElem with
| some action => `(Bind.bind $action (fun ($id:ident : $type) => $k))
| some action =>
let action := Syntax.copyRangePos (← `(($action : $((← read).m) $type))) action
`(Bind.bind $action (fun ($id:ident : $type) => $k))
| none => Macro.throwErrorAt decl "unexpected kind of 'do' declaration"
else
Macro.throwErrorAt decl "unexpected kind of 'do' declaration"

5
stage0/src/Lean/Elab/InfoTree.lean generated
View file

@ -20,6 +20,7 @@ open Std (PersistentArray PersistentArray.empty PersistentHashMap)
assignments are stored at `mctx`. -/
structure ContextInfo where
env : Environment
fileMap : FileMap
mctx : MetavarContext := {}
options : Options := {}
currNamespace : Name := Name.anonymous
@ -101,7 +102,9 @@ def ContextInfo.ppSyntax (info : ContextInfo) (lctx : LocalContext) (stx : Synta
def TermInfo.format (cinfo : ContextInfo) (info : TermInfo) : IO Format := do
cinfo.runMetaM info.lctx do
return f!"{← Meta.ppExpr info.expr} : {← Meta.ppExpr (← Meta.inferType info.expr)}"
let pos := info.stx.getPos.getD 0
let endPos := info.stx.getTailPos.getD pos
return f!"{← Meta.ppExpr info.expr} : {← Meta.ppExpr (← Meta.inferType info.expr)} @ {cinfo.fileMap.toPosition pos}-{cinfo.fileMap.toPosition endPos}"
def ContextInfo.ppGoals (cinfo : ContextInfo) (goals : List MVarId) : IO Format :=
if goals.isEmpty then

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

@ -696,7 +696,7 @@ def ignoreUnusedAlts (opts : Options) : Bool :=
def reportMatcherResultErrors (altLHSS : List AltLHS) (result : MatcherResult) : TermElabM Unit := do
unless result.counterExamples.isEmpty do
throwError! "missing cases:\n{Meta.Match.counterExamplesToMessageData result.counterExamples}"
withHeadRefOnly <| throwError! "missing cases:\n{Meta.Match.counterExamplesToMessageData result.counterExamples}"
unless ignoreUnusedAlts (← getOptions) || result.unusedAltIdxs.isEmpty do
let mut i := 0
for alt in altLHSS do

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

@ -50,7 +50,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
let preresolved := r ++ preresolved
let val := quote val
-- `scp` is bound in stxQuot.expand
`(Syntax.ident (SourceInfo.mk none none none) $(quote rawVal) (addMacroScope mainModule $val scp) $(quote preresolved))
`(Syntax.ident info $(quote rawVal) (addMacroScope mainModule $val scp) $(quote preresolved))
-- if antiquotation, insert contents as-is, else recurse
| stx@(Syntax.node k _) => do
if isAntiquot stx && !isEscapedAntiquot stx then

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

@ -275,15 +275,20 @@ builtin_initialize termElabAttribute : KeyedDeclsAttribute TermElab ← mkTermEl
`[LVal.fieldName "foo", LVal.getOp i, LVal.fieldIdx 1]`.
Recall that the notation `a[i]` is not just for accessing arrays in Lean. -/
inductive LVal where
| fieldIdx (i : Nat)
| fieldName (name : String)
| getOp (idx : Syntax)
| fieldIdx (ref : Syntax) (i : Nat)
| fieldName (ref : Syntax) (name : String)
| getOp (ref : Syntax) (idx : Syntax)
def LVal.getRef : LVal → Syntax
| LVal.fieldIdx ref _ => ref
| LVal.fieldName ref _ => ref
| LVal.getOp ref _ => ref
instance : ToString LVal where
toString
| LVal.fieldIdx i => toString i
| LVal.fieldName n => n
| LVal.getOp idx => "[" ++ toString idx ++ "]"
| LVal.fieldIdx _ i => toString i
| LVal.fieldName _ n => n
| LVal.getOp _ idx => "[" ++ toString idx ++ "]"
def getDeclName? : TermElabM (Option Name) := return (← read).declName?
def getLetRecsToLift : TermElabM (List LetRecToLift) := return (← get).letRecsToLift
@ -987,6 +992,10 @@ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone :
| some expectedType => elabImplicitLambda stx catchExPostpone expectedType #[]
| none => elabUsingElabFns stx expectedType? catchExPostpone
def addTermInfo (stx : Syntax) (e : Expr) : TermElabM Unit := do
if (← getInfoState).enabled then
pushInfoTree <| InfoTree.node (children := {}) <| Info.ofTermInfo { lctx := (← getLCtx), expr := e, stx := stx }
def mkTermInfo (stx : Syntax) (e : Expr) : TermElabM (Sum Info MVarId) := do
let isHole? : TermElabM (Option MVarId) := do
match e with

2
stage0/src/Lean/Meta/ExprDefEq.lean generated
View file

@ -566,7 +566,7 @@ instance : MonadCache Expr Expr CheckAssignmentM := {
private def addAssignmentInfo (msg : MessageData) : CheckAssignmentM MessageData := do
let ctx ← read
return m!" @ {mkMVar ctx.mvarId} {ctx.fvars} := {ctx.rhs}"
return m!"{msg} @ {mkMVar ctx.mvarId} {ctx.fvars} := {ctx.rhs}"
@[specialize] def checkFVar (check : Expr → CheckAssignmentM Expr) (fvar : Expr) : CheckAssignmentM Expr := do
let ctxMeta ← readThe Meta.Context

5
stage0/src/Lean/Meta/Match/Match.lean generated
View file

@ -551,6 +551,11 @@ private partial def process (p : Problem) : StateRefT State MetaM Unit := withIn
else if isArrayLitTransition p then
let ps ← processArrayLit p
ps.forM process
else if hasNatValPattern p then
-- This branch is reachable when `p`, for example, is just values without an else-alternative.
-- We added it just to get better error messages.
traceStep ("nat value to constructor")
process (expandNatValuePattern p)
else
checkNextPatternTypes p
throwNonSupported p

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

@ -215,7 +215,8 @@ def isIdent (stx : Syntax) : Bool :=
-- NOTE: Doesn't call `categoryParser` directly in contrast to most other "static" quotations, so call `evalInsideQuot` explicitly
@[builtinTermParser] def funBinder.quot : Parser := parser! "`(funBinder|" >> toggleInsideQuot (evalInsideQuot ``funBinder funBinder) >> ")"
@[builtinTermParser] def bracketedBinder.quot : Parser := parser! "`(bracketedBinder|" >> toggleInsideQuot (evalInsideQuot ``bracketedBinder bracketedBinder) >> ")"
def bracketedBinderF := bracketedBinder -- no default arg
@[builtinTermParser] def bracketedBinder.quot : Parser := parser! "`(bracketedBinder|" >> toggleInsideQuot (evalInsideQuot ``bracketedBinderF bracketedBinder) >> ")"
@[builtinTermParser] def matchDiscr.quot : Parser := parser! "`(matchDiscr|" >> toggleInsideQuot (evalInsideQuot ``matchDiscr matchDiscr) >> ")"
@[builtinTermParser] def attr.quot : Parser := parser! "`(attr|" >> toggleInsideQuot attrParser >> ")"

2
stage0/stdlib/CMakeLists.txt generated
View file

File diff suppressed because one or more lines are too long

60
stage0/stdlib/Init/Data/UInt.c generated
View file

@ -126,6 +126,8 @@ uint64_t l_instOfNatUInt64(lean_object*);
lean_object* l_instSubUInt8___closed__1;
lean_object* l_UInt8_add___boxed(lean_object*, lean_object*);
lean_object* l_instHModUInt16NatUInt16___closed__1;
uint8_t l_UInt8_shiftRight(uint8_t, uint8_t);
uint16_t l_UInt16_shiftLeft(uint16_t, uint16_t);
uint32_t l_Nat_toUInt32(lean_object*);
lean_object* l_instAddUInt64___closed__1;
lean_object* l_instMulUInt8___closed__1;
@ -145,16 +147,19 @@ size_t lean_usize_modn(size_t, lean_object*);
lean_object* l_instMulUInt16;
uint16_t l_UInt16_lor(uint16_t, uint16_t);
uint8_t lean_uint8_of_nat(lean_object*);
lean_object* l_UInt8_shiftRight___boxed(lean_object*, lean_object*);
lean_object* l_UInt64_ofNat___boxed(lean_object*);
lean_object* l_instModUSize___closed__1;
lean_object* l_instSubUInt64;
lean_object* l_USize_shiftLeft___boxed(lean_object*, lean_object*);
lean_object* l_instMulUInt64___closed__1;
uint8_t l_UInt8_shiftLeft(uint8_t, uint8_t);
size_t l_USize_mul(size_t, size_t);
uint64_t l_UInt64_land(uint64_t, uint64_t);
uint16_t l_UInt16_div(uint16_t, uint16_t);
lean_object* l_instMulUInt8;
uint8_t l_UInt8_land(uint8_t, uint8_t);
uint16_t l_UInt16_shiftRight(uint16_t, uint16_t);
size_t lean_usize_of_nat(lean_object*);
lean_object* l_instDivUInt32;
lean_object* l_UInt64_shiftLeft___boxed(lean_object*, lean_object*);
@ -168,6 +173,7 @@ lean_object* l_UInt16_add___boxed(lean_object*, lean_object*);
uint32_t lean_uint32_of_nat(lean_object*);
uint64_t l_UInt64_mul(uint64_t, uint64_t);
size_t l_USize_land(size_t, size_t);
lean_object* l_UInt16_shiftLeft___boxed(lean_object*, lean_object*);
lean_object* l_USize_mod___boxed(lean_object*, lean_object*);
uint8_t l_instDecidableLessEq__3(uint64_t, uint64_t);
lean_object* l_instDivUInt16;
@ -229,9 +235,11 @@ lean_object* l_USize_toUInt32___boxed(lean_object*);
uint32_t l_UInt32_lor(uint32_t, uint32_t);
lean_object* l_UInt16_lor___boxed(lean_object*, lean_object*);
lean_object* l_UInt32_modn___boxed(lean_object*, lean_object*);
lean_object* l_UInt8_shiftLeft___boxed(lean_object*, lean_object*);
lean_object* l_UInt8_decLt___boxed(lean_object*, lean_object*);
lean_object* l_USize_lor___boxed(lean_object*, lean_object*);
lean_object* l_UInt8_mul___boxed(lean_object*, lean_object*);
lean_object* l_UInt16_shiftRight___boxed(lean_object*, lean_object*);
uint8_t l_instDecidableLessEq__4(size_t, size_t);
lean_object* l_UInt64_add___boxed(lean_object*, lean_object*);
lean_object* l_UInt64_lor___boxed(lean_object*, lean_object*);
@ -538,6 +546,32 @@ x_1 = lean_box(0);
return x_1;
}
}
lean_object* l_UInt8_shiftLeft___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; uint8_t x_4; uint8_t x_5; lean_object* x_6;
x_3 = lean_unbox(x_1);
lean_dec(x_1);
x_4 = lean_unbox(x_2);
lean_dec(x_2);
x_5 = x_3 << x_4;
x_6 = lean_box(x_5);
return x_6;
}
}
lean_object* l_UInt8_shiftRight___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; uint8_t x_4; uint8_t x_5; lean_object* x_6;
x_3 = lean_unbox(x_1);
lean_dec(x_1);
x_4 = lean_unbox(x_2);
lean_dec(x_2);
x_5 = x_3 >> x_4;
x_6 = lean_box(x_5);
return x_6;
}
}
lean_object* l_UInt8_decLt___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -877,6 +911,32 @@ x_1 = lean_box(0);
return x_1;
}
}
lean_object* l_UInt16_shiftLeft___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint16_t x_3; uint16_t x_4; uint16_t x_5; lean_object* x_6;
x_3 = lean_unbox(x_1);
lean_dec(x_1);
x_4 = lean_unbox(x_2);
lean_dec(x_2);
x_5 = x_3 << x_4;
x_6 = lean_box(x_5);
return x_6;
}
}
lean_object* l_UInt16_shiftRight___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint16_t x_3; uint16_t x_4; uint16_t x_5; lean_object* x_6;
x_3 = lean_unbox(x_1);
lean_dec(x_1);
x_4 = lean_unbox(x_2);
lean_dec(x_2);
x_5 = x_3 >> x_4;
x_6 = lean_box(x_5);
return x_6;
}
}
lean_object* l_UInt16_decLt___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{

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

File diff suppressed because it is too large Load diff

14
stage0/stdlib/Lean/Compiler/IR/Format.c generated
View file

@ -26,6 +26,7 @@ lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatExpr___closed_
lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatCtorInfo___closed__3;
lean_object* l_Lean_IR_formatFnBodyHead___closed__29;
lean_object* l_Lean_IR_instToFormatDecl(lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__4;
lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatExpr___closed__7;
lean_object* l_Std_fmt___at_Lean_Position_instToFormatPosition___spec__1(lean_object*);
lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatExpr___closed__8;
@ -65,7 +66,6 @@ lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatExpr___closed_
lean_object* l_Lean_IR_formatAlt___closed__4;
lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatIRType___closed__22;
lean_object* lean_array_get_size(lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__4;
lean_object* lean_string_append(lean_object*, lean_object*);
lean_object* l_Lean_IR_instToFormatParam;
lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatExpr___closed__25;
@ -3590,7 +3590,7 @@ x_13 = l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatIRType(x_3);
x_14 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_14, 0, x_12);
lean_ctor_set(x_14, 1, x_13);
x_15 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__4;
x_15 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__4;
x_16 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_16, 0, x_14);
lean_ctor_set(x_16, 1, x_15);
@ -3683,7 +3683,7 @@ x_53 = l_Lean_IR_formatFnBodyHead___closed__9;
x_54 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_54, 0, x_53);
lean_ctor_set(x_54, 1, x_52);
x_55 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__4;
x_55 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__4;
x_56 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_56, 0, x_54);
lean_ctor_set(x_56, 1, x_55);
@ -3791,7 +3791,7 @@ x_103 = l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatIRType(x_84);
x_104 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_104, 0, x_102);
lean_ctor_set(x_104, 1, x_103);
x_105 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__4;
x_105 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__4;
x_106 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_106, 0, x_104);
lean_ctor_set(x_106, 1, x_105);
@ -4530,7 +4530,7 @@ x_15 = l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatIRType(x_4);
x_16 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_16, 0, x_14);
lean_ctor_set(x_16, 1, x_15);
x_17 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__4;
x_17 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__4;
x_18 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_18, 0, x_16);
lean_ctor_set(x_18, 1, x_17);
@ -4680,7 +4680,7 @@ x_82 = l_Lean_IR_formatFnBodyHead___closed__9;
x_83 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_83, 0, x_82);
lean_ctor_set(x_83, 1, x_81);
x_84 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__4;
x_84 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__4;
x_85 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_85, 0, x_83);
lean_ctor_set(x_85, 1, x_84);
@ -4816,7 +4816,7 @@ x_146 = l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatIRType(x_126);
x_147 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_147, 0, x_145);
lean_ctor_set(x_147, 1, x_146);
x_148 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__4;
x_148 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__4;
x_149 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_149, 0, x_147);
lean_ctor_set(x_149, 1, x_148);

8
stage0/stdlib/Lean/Data/Format.c generated
View file

@ -15,6 +15,7 @@ extern "C" {
#endif
extern lean_object* l_Lean_Name_toString___closed__1;
lean_object* l_Lean_instToFormatName(lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__4;
lean_object* l_Std_Format_pretty_x27(lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Std_Format_joinSep___at_Lean_formatKVMap___spec__1(lean_object*, lean_object*);
@ -22,7 +23,6 @@ extern lean_object* l_Std_Format_defWidth;
lean_object* l_Std_Format_getWidth(lean_object*);
extern lean_object* l_instReprSigma___rarg___closed__1;
lean_object* l_Lean_instToFormatKVMap;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__4;
lean_object* lean_string_append(lean_object*, lean_object*);
extern lean_object* l_Std_Format_sbracket___closed__4;
lean_object* l_Std_Format_getIndent___closed__1;
@ -621,7 +621,7 @@ x_4 = l_Lean_Name_toString___closed__1;
x_5 = l_Lean_Name_toStringWithSep(x_4, x_2);
x_6 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_6, 0, x_5);
x_7 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__4;
x_7 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__4;
x_8 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_8, 0, x_6);
lean_ctor_set(x_8, 1, x_7);
@ -774,7 +774,7 @@ x_8 = l_Lean_Name_toString___closed__1;
x_9 = l_Lean_Name_toStringWithSep(x_8, x_6);
x_10 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_10, 0, x_9);
x_11 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__4;
x_11 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__4;
x_12 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_12, 0, x_10);
lean_ctor_set(x_12, 1, x_11);
@ -912,7 +912,7 @@ x_52 = l_Lean_Name_toString___closed__1;
x_53 = l_Lean_Name_toStringWithSep(x_52, x_50);
x_54 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_54, 0, x_53);
x_55 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__4;
x_55 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__4;
x_56 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_56, 0, x_54);
lean_ctor_set(x_56, 1, x_55);

18
stage0/stdlib/Lean/Data/Position.c generated
View file

@ -13,7 +13,9 @@
#ifdef __cplusplus
extern "C" {
#endif
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__27;
lean_object* l_Lean_FileMap_toPosition_match__1(lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__4;
lean_object* l_Std_fmt___at_Lean_Position_instToFormatPosition___spec__1(lean_object*);
lean_object* lean_nat_div(lean_object*, lean_object*);
uint8_t l___private_Lean_Data_Position_0__Lean_decEqPosition____x40_Lean_Data_Position___hyg_16_(lean_object*, lean_object*);
@ -25,12 +27,10 @@ extern lean_object* l_Array_empty___closed__1;
extern lean_object* l_Lean_instInhabitedParserDescr___closed__1;
extern lean_object* l_instReprSigma___rarg___closed__1;
lean_object* l_Nat_decLt___boxed(lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__27;
extern lean_object* l_instInhabitedNat;
extern lean_object* l_instReprSigma___rarg___closed__7;
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__4;
lean_object* lean_string_append(lean_object*, lean_object*);
lean_object* l_prodHasDecidableLt___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Position_0__Lean_decEqPosition____x40_Lean_Data_Position___hyg_16__match__1(lean_object*);
@ -42,6 +42,7 @@ lean_object* l_Lean_instReprPosition;
lean_object* lean_string_utf8_next(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Position_0__Lean_decEqPosition____x40_Lean_Data_Position___hyg_16____boxed(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Position_0__Lean_reprPosition____x40_Lean_Data_Position___hyg_115____closed__3;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__25;
lean_object* l_Lean_FileMap_toPosition_toColumn(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Position_0__Lean_decEqPosition____x40_Lean_Data_Position___hyg_16__match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -51,7 +52,6 @@ lean_object* l_Array_back___at_Lean_FileMap_toPosition___spec__1___boxed(lean_ob
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_instReprPosition___closed__1;
lean_object* l_Lean_FileMap_toPosition_match__1___rarg(lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__25;
lean_object* l_Nat_repr(lean_object*);
extern lean_object* l_instReprSigma___rarg___closed__5;
lean_object* l_Lean_Position_instToFormatPosition_match__1___rarg(lean_object*, lean_object*);
@ -75,12 +75,12 @@ lean_object* l_Array_back___at_Lean_FileMap_toPosition___spec__1(lean_object*);
lean_object* l_Lean_instDecidableEqPosition___boxed(lean_object*, lean_object*);
lean_object* l_Lean_instInhabitedFileMap___closed__1;
lean_object* l_Lean_Position_instToFormatPosition(lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__26;
lean_object* l_Lean_Position_lt___closed__1;
lean_object* l_Lean_Position_instToFormatPosition_match__1(lean_object*);
lean_object* l_Lean_instInhabitedPosition___closed__1;
extern lean_object* l_Lean_mkOptionalNode___closed__2;
lean_object* l___private_Lean_Data_Position_0__Lean_reprPosition____x40_Lean_Data_Position___hyg_115_(lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__26;
lean_object* l___private_Lean_Data_Position_0__Lean_reprPosition____x40_Lean_Data_Position___hyg_115____closed__4;
extern lean_object* l_instReprSigma___rarg___closed__6;
uint8_t lean_string_utf8_at_end(lean_object*, lean_object*);
@ -227,7 +227,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Data_Position_0__Lean_reprPosition____x40_Lean_Data_Position___hyg_115____closed__3;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__4;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__4;
x_3 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -277,7 +277,7 @@ x_12 = l___private_Lean_Data_Position_0__Lean_reprPosition____x40_Lean_Data_Posi
x_13 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_13, 0, x_11);
lean_ctor_set(x_13, 1, x_12);
x_14 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__4;
x_14 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__4;
x_15 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_15, 0, x_13);
lean_ctor_set(x_15, 1, x_14);
@ -290,15 +290,15 @@ lean_ctor_set(x_18, 0, x_17);
x_19 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_19, 0, x_15);
lean_ctor_set(x_19, 1, x_18);
x_20 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__26;
x_20 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__26;
x_21 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_19);
x_22 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__27;
x_22 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__27;
x_23 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_23, 0, x_21);
lean_ctor_set(x_23, 1, x_22);
x_24 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__25;
x_24 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__25;
x_25 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_25, 0, x_24);
lean_ctor_set(x_25, 1, x_23);

28
stage0/stdlib/Lean/DeclarationRange.c generated
View file

@ -19,8 +19,10 @@ extern lean_object* l_Lean_Name_toString___closed__1;
extern lean_object* l_Lean_mkMapDeclarationExtension___rarg___closed__1;
lean_object* l_Lean_addDeclarationRanges___rarg(lean_object*, lean_object*, lean_object*);
size_t l_USize_add(size_t, size_t);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__27;
extern lean_object* l_Lean_mkMapDeclarationExtension___rarg___closed__2;
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__4;
lean_object* lean_nat_div(lean_object*, lean_object*);
uint8_t l___private_Lean_Data_Position_0__Lean_decEqPosition____x40_Lean_Data_Position___hyg_16_(lean_object*, lean_object*);
lean_object* l_Lean_PersistentEnvExtension_getModuleEntries___rarg(lean_object*, lean_object*, lean_object*);
@ -41,10 +43,8 @@ lean_object* lean_st_ref_get(lean_object*, lean_object*);
uint8_t lean_name_eq(lean_object*, lean_object*);
lean_object* l_Lean_declRangeExt___elambda__3___boxed(lean_object*, lean_object*);
lean_object* l_Lean_declRangeExt;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__27;
lean_object* lean_array_get_size(lean_object*);
lean_object* l___private_Lean_DeclarationRange_0__Lean_decEqDeclarationRange____x40_Lean_DeclarationRange___hyg_16__match__1(lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__4;
lean_object* lean_string_append(lean_object*, lean_object*);
lean_object* l_Lean_instReprDeclarationRange;
lean_object* l_Lean_declRangeExt___elambda__1___boxed(lean_object*);
@ -56,6 +56,7 @@ lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Lean_Name_toStringWithSep(lean_object*, lean_object*);
lean_object* l_Lean_findDeclarationRanges_x3f___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
lean_object* l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRange____x40_Lean_DeclarationRange___hyg_115____closed__3;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__25;
lean_object* l_Lean_findDeclarationRanges_x3f___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_registerSimplePersistentEnvExtension___rarg___lambda__2(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_binSearchAux___at_Lean_findDeclarationRangesCore_x3f___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -74,7 +75,6 @@ lean_object* l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRange____x
lean_object* l_Array_qsort_sort___at_Lean_initFn____x40_Lean_DeclarationRange___hyg_216____spec__2___boxed(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_instDecidableEqDeclarationRange(lean_object*, lean_object*);
lean_object* l_Lean_declRangeExt___elambda__1(lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__25;
lean_object* l_Lean_initFn____x40_Lean_DeclarationRange___hyg_216____closed__1;
extern lean_object* l_IO_instInhabitedError___closed__1;
lean_object* l_Std_RBNode_find___at_Lean_findDeclarationRangesCore_x3f___spec__2(lean_object*, lean_object*);
@ -127,6 +127,7 @@ lean_object* l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRange____x
extern lean_object* l_Lean_instInhabitedName;
lean_object* l_Lean_Environment_getModuleIdxFor_x3f(lean_object*, lean_object*);
lean_object* l_List_toArrayAux___rarg(lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__26;
lean_object* l_Lean_instInhabitedDeclarationRange;
lean_object* l_Lean_declRangeExt___elambda__3(lean_object*, lean_object*);
uint8_t l_Lean_TagDeclarationExtension_isTagged(lean_object*, lean_object*, lean_object*);
@ -137,7 +138,6 @@ lean_object* l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRange____x
lean_object* l___private_Lean_Data_Position_0__Lean_reprPosition____x40_Lean_Data_Position___hyg_115_(lean_object*, lean_object*);
lean_object* l_Lean_declRangeExt___elambda__2___boxed(lean_object*);
lean_object* l_Array_anyMUnsafe_any___at_Lean_initFn____x40_Lean_DeclarationRange___hyg_216____spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__26;
lean_object* l_EStateM_pure___rarg(lean_object*, lean_object*);
lean_object* l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRanges____x40_Lean_DeclarationRange___hyg_172____closed__6;
lean_object* l_Lean_findDeclarationRangesCore_x3f___rarg(lean_object*, lean_object*, lean_object*);
@ -280,7 +280,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRange____x40_Lean_DeclarationRange___hyg_115____closed__3;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__4;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__4;
x_3 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -329,7 +329,7 @@ x_12 = l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRange____x40_Lea
x_13 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_13, 0, x_11);
lean_ctor_set(x_13, 1, x_12);
x_14 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__4;
x_14 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__4;
x_15 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_15, 0, x_13);
lean_ctor_set(x_15, 1, x_14);
@ -340,15 +340,15 @@ x_17 = l___private_Lean_Data_Position_0__Lean_reprPosition____x40_Lean_Data_Posi
x_18 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_18, 0, x_15);
lean_ctor_set(x_18, 1, x_17);
x_19 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__26;
x_19 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__26;
x_20 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_20, 0, x_19);
lean_ctor_set(x_20, 1, x_18);
x_21 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__27;
x_21 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__27;
x_22 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_22, 0, x_20);
lean_ctor_set(x_22, 1, x_21);
x_23 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__25;
x_23 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__25;
x_24 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_24, 0, x_23);
lean_ctor_set(x_24, 1, x_22);
@ -438,7 +438,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRanges____x40_Lean_DeclarationRange___hyg_172____closed__3;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__4;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__4;
x_3 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -487,7 +487,7 @@ x_12 = l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRanges____x40_Le
x_13 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_13, 0, x_11);
lean_ctor_set(x_13, 1, x_12);
x_14 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__4;
x_14 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__4;
x_15 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_15, 0, x_13);
lean_ctor_set(x_15, 1, x_14);
@ -498,15 +498,15 @@ x_17 = l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRange____x40_Lea
x_18 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_18, 0, x_15);
lean_ctor_set(x_18, 1, x_17);
x_19 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__26;
x_19 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__26;
x_20 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_20, 0, x_19);
lean_ctor_set(x_20, 1, x_18);
x_21 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__27;
x_21 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__27;
x_22 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_22, 0, x_20);
lean_ctor_set(x_22, 1, x_21);
x_23 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__25;
x_23 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__25;
x_24 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_24, 0, x_23);
lean_ctor_set(x_24, 1, x_22);

5558
stage0/stdlib/Lean/Elab/App.c generated
View file

File diff suppressed because it is too large Load diff

1355
stage0/stdlib/Lean/Elab/Binders.c generated
View file

File diff suppressed because it is too large Load diff

585
stage0/stdlib/Lean/Elab/Command.c generated
View file

@ -50,7 +50,7 @@ lean_object* l_List_foldl___at_Lean_Elab_addMacroStack___spec__1(lean_object*, l
lean_object* l_Lean_Elab_logTrace___at_Lean_Elab_Command_elabCommand___spec__10___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Command_0__Lean_Elab_Command_elabCommandUsing_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_instMonadInfoTreeCommandElabM___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_mapM___at_Lean_Elab_Command_liftTermElabM___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_mapM___at_Lean_Elab_Command_liftTermElabM___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_addMacroStack___at_Lean_Elab_Command_instAddErrorMessageContextCommandElabM___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_withIncRecDepth___rarg___lambda__2___closed__2;
lean_object* l_Lean_Elab_Command_instAddMessageContextCommandElabM___closed__1;
@ -226,7 +226,7 @@ lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabOpenHiding___s
lean_object* l_Lean_Elab_Command_modifyScope___at_Lean_Elab_Command_addOpenDecl___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
size_t l_USize_shiftRight(size_t, size_t);
lean_object* l_Lean_Elab_Command_elabCommand_match__2(lean_object*);
lean_object* l_Std_PersistentArray_mapM___at_Lean_Elab_Command_liftTermElabM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_mapM___at_Lean_Elab_Command_liftTermElabM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_log___at_Lean_Elab_Command_runLinters___spec__3(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_getLevelNames___rarg(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Command_0__Lean_Elab_Command_popScopes_match__1(lean_object*, lean_object*);
@ -252,7 +252,7 @@ lean_object* l_Lean_Elab_Command_instMonadQuotationCommandElabM___closed__2;
lean_object* l___private_Lean_Elab_Command_0__Lean_Elab_Command_popScopes(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabSynth___closed__2;
lean_object* l_Lean_Elab_Command_instMonadInfoTreeCommandElabM___closed__2;
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_Elab_Command_modifyScope___at_Lean_Elab_Command_elabVariables___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabEvalUnsafe___lambda__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabUniverses___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -405,7 +405,7 @@ lean_object* l_Lean_Elab_Command_liftCoreM___rarg___boxed(lean_object*, lean_obj
lean_object* l_Lean_ScopedEnvExtension_pushScope___rarg(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Command_namespace___elambda__1___closed__2;
lean_object* l_Lean_Elab_Command_elabEvalUnsafe_match__3___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Command_0__Lean_Elab_Command_addScope___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ofExcept___at_Lean_Elab_Command_elabEvalUnsafe___spec__3___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Command_elabSetOption(lean_object*);
@ -512,7 +512,7 @@ lean_object* l_Lean_Elab_Command_instMonadLogCommandElabM___lambda__3(lean_objec
lean_object* l_Lean_Elab_Command_runLinters_match__1___boxed(lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_expandDeclId___spec__10___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Unhygienic_run___rarg___closed__2;
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_instMonadRecDepthCommandElabM___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_mkElabAttribute___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabEnd___closed__2;
@ -786,14 +786,14 @@ lean_object* l_Lean_Elab_expandDeclId___at_Lean_Elab_Command_expandDeclId___spec
lean_object* l_Lean_Elab_Command_elabChoiceAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_instMonadEnvCommandElabM___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Core_State_ngen___default___closed__1;
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabVariable___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Command_0__Lean_Elab_Command_mkMetaContext;
lean_object* l___private_Lean_Elab_Command_0__Lean_Elab_Command_addScopes_match__1(lean_object*);
lean_object* l_Lean_Elab_Command_mkCommandElabAttributeUnsafe___closed__7;
lean_object* l_Lean_Elab_Command_instMonadLogCommandElabM___closed__4;
lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at_Lean_Elab_Command_expandDeclId___spec__4___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_Elab_Command_elabEvalUnsafe___closed__3;
lean_object* l_Lean_throwError___at_Lean_Elab_Command_expandDeclId___spec__5(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Command_0__Lean_Elab_Command_addTraceAsMessages___spec__9(lean_object*, lean_object*, size_t, size_t, lean_object*);
@ -855,7 +855,7 @@ lean_object* l_Lean_mkConst(lean_object*, lean_object*);
lean_object* l_Lean_mkSimpleThunk(lean_object*);
lean_object* l___private_Lean_Elab_Command_0__Lean_Elab_Command_addScopes(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabNamespace___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlFromMAux___at___private_Lean_Elab_Command_0__Lean_Elab_Command_addTraceAsMessages___spec__2(lean_object*, lean_object*, size_t, size_t, lean_object*);
uint8_t l_Lean_Elab_getMacroStackOption(lean_object*);
lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at_Lean_Elab_Command_expandDeclId___spec__4(lean_object*, lean_object*, lean_object*, lean_object*);
@ -867,7 +867,7 @@ lean_object* l_Lean_Elab_Command_instMonadLogCommandElabM___lambda__1___boxed(le
lean_object* l_Lean_Elab_Command_instMonadLogCommandElabM___closed__5;
lean_object* l_Lean_Elab_Command_elabEnd___lambda__1___closed__3;
lean_object* l_Lean_Elab_Command_liftTermElabM___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_mapMAux___at_Lean_Elab_Command_liftTermElabM___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_mapMAux___at_Lean_Elab_Command_liftTermElabM___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_checkNotAlreadyDeclared___rarg___lambda__2___closed__2;
lean_object* l_Lean_Elab_mkDeclName___at_Lean_Elab_Command_expandDeclId___spec__2___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_instMonadLogCommandElabM___closed__7;
@ -880,7 +880,7 @@ lean_object* l_Lean_Elab_Command_instMonadLiftTIOCommandElabM___rarg___boxed(lea
lean_object* l_Lean_Elab_Command_instInhabitedScope___closed__1;
extern lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFns___closed__2;
lean_object* l_Lean_Elab_Term_withAutoBoundImplicitLocal___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_mapMAux___at_Lean_Elab_Command_liftTermElabM___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_mapMAux___at_Lean_Elab_Command_liftTermElabM___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_checkNotAlreadyDeclared___rarg___lambda__1___closed__2;
lean_object* l_Lean_Elab_Command_liftEIO___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_logTrace___at_Lean_Elab_Command_elabCommand___spec__10(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -10946,274 +10946,280 @@ x_3 = lean_alloc_closure((void*)(l_Lean_Elab_Command_liftTermElabM_match__2___ra
return x_3;
}
}
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, size_t x_5, size_t x_6, lean_object* x_7) {
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, size_t x_6, size_t x_7, lean_object* x_8) {
_start:
{
uint8_t x_8;
x_8 = x_6 < x_5;
if (x_8 == 0)
uint8_t x_9;
x_9 = x_7 < x_6;
if (x_9 == 0)
{
lean_object* x_9;
lean_dec(x_4);
x_9 = x_7;
return x_9;
}
else
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; size_t x_15; size_t x_16; lean_object* x_17; lean_object* x_18;
x_10 = lean_array_uget(x_7, x_6);
x_11 = lean_unsigned_to_nat(0u);
x_12 = lean_array_uset(x_7, x_6, x_11);
x_13 = x_10;
lean_inc(x_4);
x_14 = l_Std_PersistentArray_mapMAux___at_Lean_Elab_Command_liftTermElabM___spec__2(x_1, x_2, x_3, x_4, x_13);
x_15 = 1;
x_16 = x_6 + x_15;
x_17 = x_14;
x_18 = lean_array_uset(x_12, x_6, x_17);
x_6 = x_16;
x_7 = x_18;
goto _start;
}
}
}
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, size_t x_5, size_t x_6, lean_object* x_7) {
_start:
{
uint8_t x_8;
x_8 = x_6 < x_5;
if (x_8 == 0)
{
lean_object* x_9;
lean_dec(x_4);
x_9 = x_7;
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; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; size_t x_24; size_t x_25; lean_object* x_26; lean_object* x_27;
x_10 = lean_array_uget(x_7, x_6);
x_11 = lean_unsigned_to_nat(0u);
x_12 = lean_array_uset(x_7, x_6, x_11);
x_13 = x_10;
x_14 = lean_ctor_get(x_4, 5);
lean_inc(x_14);
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
lean_dec(x_14);
x_16 = l_Lean_Elab_InfoTree_substitute(x_13, x_15);
x_17 = lean_ctor_get(x_3, 0);
x_18 = lean_ctor_get(x_2, 0);
x_19 = lean_ctor_get(x_1, 1);
x_20 = lean_ctor_get(x_1, 2);
x_21 = lean_ctor_get(x_1, 3);
lean_inc(x_21);
lean_inc(x_20);
lean_inc(x_19);
lean_inc(x_18);
lean_inc(x_17);
x_22 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_22, 0, x_17);
lean_ctor_set(x_22, 1, x_18);
lean_ctor_set(x_22, 2, x_19);
lean_ctor_set(x_22, 3, x_20);
lean_ctor_set(x_22, 4, x_21);
x_23 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_23, 0, x_22);
lean_ctor_set(x_23, 1, x_16);
x_24 = 1;
x_25 = x_6 + x_24;
x_26 = x_23;
x_27 = lean_array_uset(x_12, x_6, x_26);
x_6 = x_25;
x_7 = x_27;
goto _start;
}
}
}
lean_object* l_Std_PersistentArray_mapMAux___at_Lean_Elab_Command_liftTermElabM___spec__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
if (lean_obj_tag(x_5) == 0)
{
uint8_t x_6;
x_6 = !lean_is_exclusive(x_5);
if (x_6 == 0)
{
lean_object* x_7; lean_object* x_8; size_t x_9; size_t x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_7 = lean_ctor_get(x_5, 0);
x_8 = lean_array_get_size(x_7);
x_9 = lean_usize_of_nat(x_8);
lean_dec(x_8);
x_10 = 0;
x_11 = x_7;
x_12 = l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__3(x_1, x_2, x_3, x_4, x_9, x_10, x_11);
x_13 = x_12;
lean_ctor_set(x_5, 0, x_13);
return x_5;
}
else
{
lean_object* x_14; lean_object* x_15; size_t x_16; size_t x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_14 = lean_ctor_get(x_5, 0);
lean_inc(x_14);
lean_object* x_10;
lean_dec(x_5);
x_15 = lean_array_get_size(x_14);
x_16 = lean_usize_of_nat(x_15);
lean_dec(x_15);
x_17 = 0;
x_18 = x_14;
x_19 = l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__3(x_1, x_2, x_3, x_4, x_16, x_17, x_18);
x_20 = x_19;
x_21 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_21, 0, x_20);
return x_21;
}
x_10 = x_8;
return x_10;
}
else
{
uint8_t x_22;
x_22 = !lean_is_exclusive(x_5);
if (x_22 == 0)
{
lean_object* x_23; lean_object* x_24; size_t x_25; size_t x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29;
x_23 = lean_ctor_get(x_5, 0);
x_24 = lean_array_get_size(x_23);
x_25 = lean_usize_of_nat(x_24);
lean_dec(x_24);
x_26 = 0;
x_27 = x_23;
x_28 = l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__4(x_1, x_2, x_3, x_4, x_25, x_26, x_27);
x_29 = x_28;
lean_ctor_set(x_5, 0, x_29);
return x_5;
}
else
{
lean_object* x_30; lean_object* x_31; size_t x_32; size_t x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37;
x_30 = lean_ctor_get(x_5, 0);
lean_inc(x_30);
lean_dec(x_5);
x_31 = lean_array_get_size(x_30);
x_32 = lean_usize_of_nat(x_31);
lean_dec(x_31);
x_33 = 0;
x_34 = x_30;
x_35 = l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__4(x_1, x_2, x_3, x_4, x_32, x_33, x_34);
x_36 = x_35;
x_37 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_37, 0, x_36);
return x_37;
}
}
}
}
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__5(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, size_t x_5, size_t x_6, lean_object* x_7) {
_start:
{
uint8_t x_8;
x_8 = x_6 < x_5;
if (x_8 == 0)
{
lean_object* x_9;
lean_dec(x_4);
x_9 = x_7;
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; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; size_t x_24; size_t x_25; lean_object* x_26; lean_object* x_27;
x_10 = lean_array_uget(x_7, x_6);
x_11 = lean_unsigned_to_nat(0u);
x_12 = lean_array_uset(x_7, x_6, x_11);
x_13 = x_10;
x_14 = lean_ctor_get(x_4, 5);
lean_inc(x_14);
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
lean_dec(x_14);
x_16 = l_Lean_Elab_InfoTree_substitute(x_13, x_15);
x_17 = lean_ctor_get(x_3, 0);
x_18 = lean_ctor_get(x_2, 0);
x_19 = lean_ctor_get(x_1, 1);
x_20 = lean_ctor_get(x_1, 2);
x_21 = lean_ctor_get(x_1, 3);
lean_inc(x_21);
lean_inc(x_20);
lean_inc(x_19);
lean_inc(x_18);
lean_inc(x_17);
x_22 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_22, 0, x_17);
lean_ctor_set(x_22, 1, x_18);
lean_ctor_set(x_22, 2, x_19);
lean_ctor_set(x_22, 3, x_20);
lean_ctor_set(x_22, 4, x_21);
x_23 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_23, 0, x_22);
lean_ctor_set(x_23, 1, x_16);
x_24 = 1;
x_25 = x_6 + x_24;
x_26 = x_23;
x_27 = lean_array_uset(x_12, x_6, x_26);
x_6 = x_25;
x_7 = x_27;
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; size_t x_16; size_t x_17; lean_object* x_18; lean_object* x_19;
x_11 = lean_array_uget(x_8, x_7);
x_12 = lean_unsigned_to_nat(0u);
x_13 = lean_array_uset(x_8, x_7, x_12);
x_14 = x_11;
lean_inc(x_5);
x_15 = l_Std_PersistentArray_mapMAux___at_Lean_Elab_Command_liftTermElabM___spec__2(x_1, x_2, x_3, x_4, x_5, x_14);
x_16 = 1;
x_17 = x_7 + x_16;
x_18 = x_15;
x_19 = lean_array_uset(x_13, x_7, x_18);
x_7 = x_17;
x_8 = x_19;
goto _start;
}
}
}
lean_object* l_Std_PersistentArray_mapM___at_Lean_Elab_Command_liftTermElabM___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, size_t x_6, size_t x_7, lean_object* x_8) {
_start:
{
uint8_t x_6;
x_6 = !lean_is_exclusive(x_5);
if (x_6 == 0)
uint8_t x_9;
x_9 = x_7 < x_6;
if (x_9 == 0)
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; size_t x_11; size_t x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_7 = lean_ctor_get(x_5, 0);
x_8 = lean_ctor_get(x_5, 1);
lean_inc(x_4);
x_9 = l_Std_PersistentArray_mapMAux___at_Lean_Elab_Command_liftTermElabM___spec__2(x_1, x_2, x_3, x_4, x_7);
x_10 = lean_array_get_size(x_8);
x_11 = lean_usize_of_nat(x_10);
lean_dec(x_10);
x_12 = 0;
x_13 = x_8;
x_14 = l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__5(x_1, x_2, x_3, x_4, x_11, x_12, x_13);
x_15 = x_14;
lean_ctor_set(x_5, 1, x_15);
lean_ctor_set(x_5, 0, x_9);
return x_5;
lean_object* x_10;
lean_dec(x_5);
x_10 = x_8;
return x_10;
}
else
{
lean_object* x_16; lean_object* x_17; lean_object* x_18; size_t x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; size_t x_23; size_t x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28;
x_16 = lean_ctor_get(x_5, 0);
x_17 = lean_ctor_get(x_5, 1);
x_18 = lean_ctor_get(x_5, 2);
x_19 = lean_ctor_get_usize(x_5, 4);
x_20 = lean_ctor_get(x_5, 3);
lean_inc(x_20);
lean_inc(x_18);
lean_inc(x_17);
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; size_t x_26; size_t x_27; lean_object* x_28; lean_object* x_29;
x_11 = lean_array_uget(x_8, x_7);
x_12 = lean_unsigned_to_nat(0u);
x_13 = lean_array_uset(x_8, x_7, x_12);
x_14 = x_11;
x_15 = lean_ctor_get(x_5, 5);
lean_inc(x_15);
x_16 = lean_ctor_get(x_15, 0);
lean_inc(x_16);
lean_dec(x_15);
x_17 = l_Lean_Elab_InfoTree_substitute(x_14, x_16);
x_18 = lean_ctor_get(x_4, 0);
x_19 = lean_ctor_get(x_1, 1);
x_20 = lean_ctor_get(x_3, 0);
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_inc(x_20);
lean_inc(x_19);
lean_inc(x_18);
x_24 = lean_alloc_ctor(0, 6, 0);
lean_ctor_set(x_24, 0, x_18);
lean_ctor_set(x_24, 1, x_19);
lean_ctor_set(x_24, 2, x_20);
lean_ctor_set(x_24, 3, x_21);
lean_ctor_set(x_24, 4, x_22);
lean_ctor_set(x_24, 5, x_23);
x_25 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_25, 0, x_24);
lean_ctor_set(x_25, 1, x_17);
x_26 = 1;
x_27 = x_7 + x_26;
x_28 = x_25;
x_29 = lean_array_uset(x_13, x_7, x_28);
x_7 = x_27;
x_8 = x_29;
goto _start;
}
}
}
lean_object* l_Std_PersistentArray_mapMAux___at_Lean_Elab_Command_liftTermElabM___spec__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
if (lean_obj_tag(x_6) == 0)
{
uint8_t x_7;
x_7 = !lean_is_exclusive(x_6);
if (x_7 == 0)
{
lean_object* x_8; lean_object* x_9; size_t x_10; size_t x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_8 = lean_ctor_get(x_6, 0);
x_9 = lean_array_get_size(x_8);
x_10 = lean_usize_of_nat(x_9);
lean_dec(x_9);
x_11 = 0;
x_12 = x_8;
x_13 = l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__3(x_1, x_2, x_3, x_4, x_5, x_10, x_11, x_12);
x_14 = x_13;
lean_ctor_set(x_6, 0, x_14);
return x_6;
}
else
{
lean_object* x_15; lean_object* x_16; size_t x_17; size_t x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_15 = lean_ctor_get(x_6, 0);
lean_inc(x_15);
lean_dec(x_6);
x_16 = lean_array_get_size(x_15);
x_17 = lean_usize_of_nat(x_16);
lean_dec(x_16);
x_18 = 0;
x_19 = x_15;
x_20 = l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__3(x_1, x_2, x_3, x_4, x_5, x_17, x_18, x_19);
x_21 = x_20;
x_22 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_22, 0, x_21);
return x_22;
}
}
else
{
uint8_t x_23;
x_23 = !lean_is_exclusive(x_6);
if (x_23 == 0)
{
lean_object* x_24; lean_object* x_25; size_t x_26; size_t x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30;
x_24 = lean_ctor_get(x_6, 0);
x_25 = lean_array_get_size(x_24);
x_26 = lean_usize_of_nat(x_25);
lean_dec(x_25);
x_27 = 0;
x_28 = x_24;
x_29 = l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__4(x_1, x_2, x_3, x_4, x_5, x_26, x_27, x_28);
x_30 = x_29;
lean_ctor_set(x_6, 0, x_30);
return x_6;
}
else
{
lean_object* x_31; lean_object* x_32; size_t x_33; size_t x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38;
x_31 = lean_ctor_get(x_6, 0);
lean_inc(x_31);
lean_dec(x_6);
x_32 = lean_array_get_size(x_31);
x_33 = lean_usize_of_nat(x_32);
lean_dec(x_32);
x_34 = 0;
x_35 = x_31;
x_36 = l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__4(x_1, x_2, x_3, x_4, x_5, x_33, x_34, x_35);
x_37 = x_36;
x_38 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_38, 0, x_37);
return x_38;
}
}
}
}
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__5(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, size_t x_6, size_t x_7, lean_object* x_8) {
_start:
{
uint8_t x_9;
x_9 = x_7 < x_6;
if (x_9 == 0)
{
lean_object* x_10;
lean_dec(x_5);
lean_inc(x_4);
x_21 = l_Std_PersistentArray_mapMAux___at_Lean_Elab_Command_liftTermElabM___spec__2(x_1, x_2, x_3, x_4, x_16);
x_22 = lean_array_get_size(x_17);
x_23 = lean_usize_of_nat(x_22);
lean_dec(x_22);
x_24 = 0;
x_25 = x_17;
x_26 = l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__5(x_1, x_2, x_3, x_4, x_23, x_24, x_25);
x_27 = x_26;
x_28 = lean_alloc_ctor(0, 4, sizeof(size_t)*1);
lean_ctor_set(x_28, 0, x_21);
lean_ctor_set(x_28, 1, x_27);
lean_ctor_set(x_28, 2, x_18);
lean_ctor_set(x_28, 3, x_20);
lean_ctor_set_usize(x_28, 4, x_19);
return x_28;
x_10 = x_8;
return x_10;
}
else
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; size_t x_26; size_t x_27; lean_object* x_28; lean_object* x_29;
x_11 = lean_array_uget(x_8, x_7);
x_12 = lean_unsigned_to_nat(0u);
x_13 = lean_array_uset(x_8, x_7, x_12);
x_14 = x_11;
x_15 = lean_ctor_get(x_5, 5);
lean_inc(x_15);
x_16 = lean_ctor_get(x_15, 0);
lean_inc(x_16);
lean_dec(x_15);
x_17 = l_Lean_Elab_InfoTree_substitute(x_14, x_16);
x_18 = lean_ctor_get(x_4, 0);
x_19 = lean_ctor_get(x_1, 1);
x_20 = lean_ctor_get(x_3, 0);
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_inc(x_20);
lean_inc(x_19);
lean_inc(x_18);
x_24 = lean_alloc_ctor(0, 6, 0);
lean_ctor_set(x_24, 0, x_18);
lean_ctor_set(x_24, 1, x_19);
lean_ctor_set(x_24, 2, x_20);
lean_ctor_set(x_24, 3, x_21);
lean_ctor_set(x_24, 4, x_22);
lean_ctor_set(x_24, 5, x_23);
x_25 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_25, 0, x_24);
lean_ctor_set(x_25, 1, x_17);
x_26 = 1;
x_27 = x_7 + x_26;
x_28 = x_25;
x_29 = lean_array_uset(x_13, x_7, x_28);
x_7 = x_27;
x_8 = x_29;
goto _start;
}
}
}
lean_object* l_Std_PersistentArray_mapM___at_Lean_Elab_Command_liftTermElabM___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
uint8_t x_7;
x_7 = !lean_is_exclusive(x_6);
if (x_7 == 0)
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; size_t x_12; size_t x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
x_8 = lean_ctor_get(x_6, 0);
x_9 = lean_ctor_get(x_6, 1);
lean_inc(x_5);
x_10 = l_Std_PersistentArray_mapMAux___at_Lean_Elab_Command_liftTermElabM___spec__2(x_1, x_2, x_3, x_4, x_5, x_8);
x_11 = lean_array_get_size(x_9);
x_12 = lean_usize_of_nat(x_11);
lean_dec(x_11);
x_13 = 0;
x_14 = x_9;
x_15 = l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__5(x_1, x_2, x_3, x_4, x_5, x_12, x_13, x_14);
x_16 = x_15;
lean_ctor_set(x_6, 1, x_16);
lean_ctor_set(x_6, 0, x_10);
return x_6;
}
else
{
lean_object* x_17; lean_object* x_18; lean_object* x_19; size_t x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; size_t x_24; size_t x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29;
x_17 = lean_ctor_get(x_6, 0);
x_18 = lean_ctor_get(x_6, 1);
x_19 = lean_ctor_get(x_6, 2);
x_20 = lean_ctor_get_usize(x_6, 4);
x_21 = lean_ctor_get(x_6, 3);
lean_inc(x_21);
lean_inc(x_19);
lean_inc(x_18);
lean_inc(x_17);
lean_dec(x_6);
lean_inc(x_5);
x_22 = l_Std_PersistentArray_mapMAux___at_Lean_Elab_Command_liftTermElabM___spec__2(x_1, x_2, x_3, x_4, x_5, x_17);
x_23 = lean_array_get_size(x_18);
x_24 = lean_usize_of_nat(x_23);
lean_dec(x_23);
x_25 = 0;
x_26 = x_18;
x_27 = l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__5(x_1, x_2, x_3, x_4, x_5, x_24, x_25, x_26);
x_28 = x_27;
x_29 = lean_alloc_ctor(0, 4, sizeof(size_t)*1);
lean_ctor_set(x_29, 0, x_22);
lean_ctor_set(x_29, 1, x_28);
lean_ctor_set(x_29, 2, x_19);
lean_ctor_set(x_29, 3, x_21);
lean_ctor_set_usize(x_29, 4, x_20);
return x_29;
}
}
}
@ -11409,7 +11415,7 @@ x_41 = lean_ctor_get(x_40, 1);
lean_inc(x_41);
lean_dec(x_40);
lean_inc(x_39);
x_42 = l_Std_PersistentArray_mapM___at_Lean_Elab_Command_liftTermElabM___spec__1(x_13, x_33, x_36, x_39, x_41);
x_42 = l_Std_PersistentArray_mapM___at_Lean_Elab_Command_liftTermElabM___spec__1(x_3, x_13, x_33, x_36, x_39, x_41);
lean_dec(x_33);
lean_dec(x_13);
x_43 = lean_st_ref_take(x_4, x_37);
@ -11712,71 +11718,76 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Command_liftTermElabM___rarg___boxe
return x_2;
}
}
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__3___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_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__3___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:
{
size_t x_8; size_t x_9; lean_object* x_10;
x_8 = lean_unbox_usize(x_5);
lean_dec(x_5);
size_t x_9; size_t x_10; lean_object* x_11;
x_9 = lean_unbox_usize(x_6);
lean_dec(x_6);
x_10 = l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__3(x_1, x_2, x_3, x_4, x_8, x_9, x_7);
x_10 = lean_unbox_usize(x_7);
lean_dec(x_7);
x_11 = l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__3(x_1, x_2, x_3, x_4, x_5, x_9, x_10, x_8);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_10;
return x_11;
}
}
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__4___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__4___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
size_t x_8; size_t x_9; lean_object* x_10;
x_8 = lean_unbox_usize(x_5);
lean_dec(x_5);
size_t x_9; size_t x_10; lean_object* x_11;
x_9 = lean_unbox_usize(x_6);
lean_dec(x_6);
x_10 = l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__4(x_1, x_2, x_3, x_4, x_8, x_9, x_7);
x_10 = lean_unbox_usize(x_7);
lean_dec(x_7);
x_11 = l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__4(x_1, x_2, x_3, x_4, x_5, x_9, x_10, x_8);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_10;
return x_11;
}
}
lean_object* l_Std_PersistentArray_mapMAux___at_Lean_Elab_Command_liftTermElabM___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
lean_object* l_Std_PersistentArray_mapMAux___at_Lean_Elab_Command_liftTermElabM___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_6;
x_6 = l_Std_PersistentArray_mapMAux___at_Lean_Elab_Command_liftTermElabM___spec__2(x_1, x_2, x_3, x_4, x_5);
lean_object* x_7;
x_7 = l_Std_PersistentArray_mapMAux___at_Lean_Elab_Command_liftTermElabM___spec__2(x_1, x_2, x_3, x_4, x_5, x_6);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_6;
return x_7;
}
}
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__5___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_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__5___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:
{
size_t x_8; size_t x_9; lean_object* x_10;
x_8 = lean_unbox_usize(x_5);
lean_dec(x_5);
size_t x_9; size_t x_10; lean_object* x_11;
x_9 = lean_unbox_usize(x_6);
lean_dec(x_6);
x_10 = l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__5(x_1, x_2, x_3, x_4, x_8, x_9, x_7);
x_10 = lean_unbox_usize(x_7);
lean_dec(x_7);
x_11 = l_Array_mapMUnsafe_map___at_Lean_Elab_Command_liftTermElabM___spec__5(x_1, x_2, x_3, x_4, x_5, x_9, x_10, x_8);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_10;
return x_11;
}
}
lean_object* l_Std_PersistentArray_mapM___at_Lean_Elab_Command_liftTermElabM___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
lean_object* l_Std_PersistentArray_mapM___at_Lean_Elab_Command_liftTermElabM___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_6;
x_6 = l_Std_PersistentArray_mapM___at_Lean_Elab_Command_liftTermElabM___spec__1(x_1, x_2, x_3, x_4, x_5);
lean_object* x_7;
x_7 = l_Std_PersistentArray_mapM___at_Lean_Elab_Command_liftTermElabM___spec__1(x_1, x_2, x_3, x_4, x_5, x_6);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_6;
return x_7;
}
}
lean_object* l_Lean_Elab_Command_liftTermElabM___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
@ -14619,7 +14630,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Elab_Command_modifyScope___closed__1;
x_2 = l_Lean_Elab_Command_modifyScope___closed__2;
x_3 = lean_unsigned_to_nat(396u);
x_3 = lean_unsigned_to_nat(398u);
x_4 = lean_unsigned_to_nat(16u);
x_5 = l_Lean_Syntax_strLitToAtom___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

4
stage0/stdlib/Lean/Elab/Declaration.c generated
View file

@ -381,7 +381,7 @@ extern lean_object* l_Lean_Parser_Command_constant___elambda__1___closed__1;
lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Command_mkDefViewOfConstant___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_withAutoBoundImplicitLocal___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_expandInitCmd___closed__5;
extern lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_process___lambda__1___closed__1;
extern lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_process___lambda__1___closed__2;
extern lean_object* l_Lean_Elab_checkNotAlreadyDeclared___rarg___lambda__1___closed__2;
lean_object* l_Lean_Elab_Command_expandBuiltinInitialize(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_getBetterRef(lean_object*, lean_object*);
@ -5760,7 +5760,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1098____closed__3;
x_2 = l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_process___lambda__1___closed__1;
x_2 = l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_process___lambda__1___closed__2;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}

2842
stage0/stdlib/Lean/Elab/Do.c generated
View file

File diff suppressed because it is too large Load diff

941
stage0/stdlib/Lean/Elab/InfoTree.c generated
View file

File diff suppressed because it is too large Load diff

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

@ -124,6 +124,7 @@ lean_object* l_Lean_Elab_Term_withDepElimPatterns(lean_object*);
lean_object* l_Array_extract___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_CtorApp_processExplicitArg___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_withPatternVars_loop___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getHead_x3f(lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_14562____closed__6;
lean_object* l_Lean_throwError___at___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_throwInvalidPattern___spec__1(lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_ToDepElimPattern_mkLocalDeclFor(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -22906,7 +22907,7 @@ lean_inc(x_10);
x_11 = l_List_isEmpty___rarg(x_10);
if (x_11 == 0)
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18;
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23;
lean_dec(x_2);
x_12 = l_Lean_Meta_Match_counterExamplesToMessageData(x_10);
x_13 = l_Lean_Elab_Term_reportMatcherResultErrors___closed__2;
@ -22917,39 +22918,159 @@ x_15 = l_Lean_KernelException_toMessageData___closed__15;
x_16 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_16, 0, x_14);
lean_ctor_set(x_16, 1, x_15);
x_17 = l_Lean_throwError___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1(x_16, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
x_17 = lean_ctor_get(x_7, 0);
lean_inc(x_17);
x_18 = lean_ctor_get(x_7, 1);
lean_inc(x_18);
x_19 = lean_ctor_get(x_7, 2);
lean_inc(x_19);
x_20 = lean_ctor_get(x_7, 3);
lean_inc(x_20);
x_21 = lean_ctor_get(x_7, 4);
lean_inc(x_21);
x_22 = lean_ctor_get(x_7, 5);
lean_inc(x_22);
lean_inc(x_20);
x_23 = l_Lean_Syntax_getHead_x3f(x_20);
if (lean_obj_tag(x_23) == 0)
{
lean_object* x_24; uint8_t x_25;
lean_dec(x_22);
lean_dec(x_21);
lean_dec(x_20);
lean_dec(x_19);
lean_dec(x_18);
lean_dec(x_17);
x_24 = l_Lean_throwError___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1(x_16, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
x_18 = !lean_is_exclusive(x_17);
if (x_18 == 0)
x_25 = !lean_is_exclusive(x_24);
if (x_25 == 0)
{
return x_17;
return x_24;
}
else
{
lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_19 = lean_ctor_get(x_17, 0);
x_20 = lean_ctor_get(x_17, 1);
lean_inc(x_20);
lean_inc(x_19);
lean_dec(x_17);
x_21 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_21, 0, x_19);
lean_ctor_set(x_21, 1, x_20);
return x_21;
lean_object* x_26; lean_object* x_27; lean_object* x_28;
x_26 = lean_ctor_get(x_24, 0);
x_27 = lean_ctor_get(x_24, 1);
lean_inc(x_27);
lean_inc(x_26);
lean_dec(x_24);
x_28 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_28, 0, x_26);
lean_ctor_set(x_28, 1, x_27);
return x_28;
}
}
else
{
lean_object* x_22; lean_object* x_23;
uint8_t x_29;
x_29 = !lean_is_exclusive(x_7);
if (x_29 == 0)
{
lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; uint8_t x_39;
x_30 = lean_ctor_get(x_7, 5);
lean_dec(x_30);
x_31 = lean_ctor_get(x_7, 4);
lean_dec(x_31);
x_32 = lean_ctor_get(x_7, 3);
lean_dec(x_32);
x_33 = lean_ctor_get(x_7, 2);
lean_dec(x_33);
x_34 = lean_ctor_get(x_7, 1);
lean_dec(x_34);
x_35 = lean_ctor_get(x_7, 0);
lean_dec(x_35);
x_36 = lean_ctor_get(x_23, 0);
lean_inc(x_36);
lean_dec(x_23);
x_37 = l_Lean_replaceRef(x_36, x_20);
lean_dec(x_20);
lean_dec(x_36);
lean_ctor_set(x_7, 3, x_37);
x_38 = l_Lean_throwError___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1(x_16, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
x_39 = !lean_is_exclusive(x_38);
if (x_39 == 0)
{
return x_38;
}
else
{
lean_object* x_40; lean_object* x_41; lean_object* x_42;
x_40 = lean_ctor_get(x_38, 0);
x_41 = lean_ctor_get(x_38, 1);
lean_inc(x_41);
lean_inc(x_40);
lean_dec(x_38);
x_42 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_42, 0, x_40);
lean_ctor_set(x_42, 1, x_41);
return x_42;
}
}
else
{
lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50;
lean_dec(x_7);
x_43 = lean_ctor_get(x_23, 0);
lean_inc(x_43);
lean_dec(x_23);
x_44 = l_Lean_replaceRef(x_43, x_20);
lean_dec(x_20);
lean_dec(x_43);
x_45 = lean_alloc_ctor(0, 6, 0);
lean_ctor_set(x_45, 0, x_17);
lean_ctor_set(x_45, 1, x_18);
lean_ctor_set(x_45, 2, x_19);
lean_ctor_set(x_45, 3, x_44);
lean_ctor_set(x_45, 4, x_21);
lean_ctor_set(x_45, 5, x_22);
x_46 = l_Lean_throwError___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1(x_16, x_3, x_4, x_5, x_6, x_45, x_8, x_9);
lean_dec(x_8);
lean_dec(x_45);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
x_47 = lean_ctor_get(x_46, 0);
lean_inc(x_47);
x_48 = lean_ctor_get(x_46, 1);
lean_inc(x_48);
if (lean_is_exclusive(x_46)) {
lean_ctor_release(x_46, 0);
lean_ctor_release(x_46, 1);
x_49 = x_46;
} else {
lean_dec_ref(x_46);
x_49 = lean_box(0);
}
if (lean_is_scalar(x_49)) {
x_50 = lean_alloc_ctor(1, 2, 0);
} else {
x_50 = x_49;
}
lean_ctor_set(x_50, 0, x_47);
lean_ctor_set(x_50, 1, x_48);
return x_50;
}
}
}
else
{
lean_object* x_51; lean_object* x_52;
lean_dec(x_10);
x_22 = lean_box(0);
x_23 = l_Lean_Elab_Term_reportMatcherResultErrors___lambda__1(x_2, x_1, x_22, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
x_51 = lean_box(0);
x_52 = l_Lean_Elab_Term_reportMatcherResultErrors___lambda__1(x_2, x_1, x_51, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
lean_dec(x_2);
return x_23;
return x_52;
}
}
}

1884
stage0/stdlib/Lean/Elab/Quotation.c generated
View file

File diff suppressed because it is too large Load diff

4
stage0/stdlib/Lean/Elab/StructInst.c generated
View file

@ -41,6 +41,7 @@ lean_object* l_Lean_Elab_Term_StructInst_Struct_modifyFieldsM(lean_object*);
lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_getStructName_match__1(lean_object*);
lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_elabStruct_match__4___rarg(lean_object*, lean_object*, lean_object*);
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__4;
lean_object* l_Std_fmt___at_Lean_Position_instToFormatPosition___spec__1(lean_object*);
lean_object* l_Lean_Meta_mkForallFVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_foldlM___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_elabStruct___spec__3___closed__4;
@ -158,7 +159,6 @@ lean_object* lean_array_get_size(lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_expandStructInstExpectedType(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_elabStructInstAux___closed__4;
lean_object* l_Lean_Elab_Term_StructInst_Struct_setFields(lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__4;
lean_object* l_Std_HashMap_toList___rarg(lean_object*);
lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_elabModifyOp___closed__18;
lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_groupFields___lambda__1(lean_object*);
@ -5830,7 +5830,7 @@ x_3 = lean_ctor_get(x_2, 1);
lean_inc(x_3);
x_4 = l_Lean_Elab_Term_StructInst_formatField___closed__2;
x_5 = l_Std_Format_joinSep___at_Lean_Elab_Term_StructInst_formatField___spec__1(x_3, x_4);
x_6 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__4;
x_6 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__4;
x_7 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_7, 0, x_5);
lean_ctor_set(x_7, 1, x_6);

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

@ -63,7 +63,6 @@ lean_object* l_Lean_registerTraceClass(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_instMonadLogTermElabM___closed__2;
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_isExplicitApp___boxed(lean_object*);
lean_object* l_ReaderT_read___at_Lean_Elab_Term_instMonadLogTermElabM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__1;
lean_object* l_Lean_stringToMessageData(lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Term_throwMVarError___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_evalExpr___rarg___closed__2;
@ -119,7 +118,6 @@ lean_object* l_Lean_Elab_Term_setLevelNames(lean_object*, lean_object*, lean_obj
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_ppGoal___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_getFVarLocalDecl_x21___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__4;
lean_object* l_Lean_Elab_Term_getFVarLocalDecl_x21_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_append___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___closed__2;
@ -144,7 +142,6 @@ lean_object* l_Lean_getConstInfo___at_Lean_Elab_Term_mkConst___spec__1___boxed(l
uint8_t l_Lean_Elab_isValidAutoBoundImplicitName(lean_object*);
lean_object* l_Lean_Elab_Term_resolveLocalName_loop___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_tryPostponeIfNoneOrMVar_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__2;
extern lean_object* l_Lean_Parser_Term_ensureExpectedType___elambda__1___closed__2;
lean_object* l_Lean_Meta_mkAppM(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_levelMVarToParam___closed__1;
@ -156,6 +153,7 @@ lean_object* l_Lean_Elab_log___at___private_Lean_Elab_Term_0__Lean_Elab_Term_exc
lean_object* l___regBuiltin_Lean_Elab_Term_elabEnsureTypeOf___closed__1;
lean_object* l_Lean_Elab_Term_elabNumLit___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_addAutoBoundImplicits_match__2___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_addTermInfo___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_mkFreshTypeMVarFor___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_type___elambda__1___closed__2;
@ -276,7 +274,6 @@ lean_object* l_Lean_Elab_Term_instInhabitedTermElabResult___closed__1;
extern lean_object* l_Lean_Expr_getAppArgs___closed__1;
lean_object* l_Lean_Elab_Term_registerCustomErrorIfMVar___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwKernelException___at_Lean_Elab_Term_evalExpr___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_CheckAssignment_addAssignmentInfo___rarg___closed__3;
lean_object* l_Lean_Elab_Term_instMonadMacroAdapterTermElabM___closed__3;
lean_object* l_Lean_Elab_Term_elabTypeWithAutoBoundImplicit_loop_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Level_elabLevel(lean_object*, lean_object*, lean_object*);
@ -348,6 +345,7 @@ lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_isExplicit___boxed(lea
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_addAutoBoundImplicits___spec__5(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImplicitLambda_match__1(lean_object*);
lean_object* l_Lean_Elab_Term_ensureHasType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_6266____closed__1;
extern lean_object* l_Lean_throwUnknownConstant___rarg___closed__2;
lean_object* l_Lean_throwError___at_Lean_Elab_Term_throwTypeMismatchError___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_instInhabitedException___closed__1;
@ -369,6 +367,7 @@ lean_object* l_Lean_Elab_Term_liftMetaM(lean_object*);
extern lean_object* l_Lean_Elab_throwAbortCommand___rarg___closed__1;
lean_object* l_Lean_Elab_Term_saveAllState___boxed(lean_object*);
lean_object* l_List_map___at_Lean_Elab_Term_resolveId_x3f___spec__3(lean_object*);
lean_object* l_Lean_Elab_Term_LVal_getRef___boxed(lean_object*);
lean_object* l_Lean_Elab_Term_instInhabitedTermElabM___closed__1;
extern lean_object* l_Lean_Json_Parser_anyCore___rarg___closed__6;
lean_object* l_Std_PersistentArray_forInAux___at_Lean_Elab_Term_addAutoBoundImplicits___spec__3___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -406,6 +405,7 @@ lean_object* l_Std_PersistentArray_forMAux___at_Lean_Elab_Term_instMetaEvalTermE
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_addAutoBoundImplicits___spec__1___closed__4;
lean_object* l_Lean_Syntax_isCharLit_x3f(lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_8246____closed__1;
lean_object* l_Lean_Elab_Term_elabTermEnsuringType(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___closed__5;
@ -469,6 +469,7 @@ lean_object* l_Lean_Elab_Term_elabProp___rarg(lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImplicitLambdaAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_logException___at___private_Lean_Elab_Term_0__Lean_Elab_Term_exceptionToSorry___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_isStrLit_x3f(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__3;
lean_object* l_Lean_Elab_logAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_exceptionToSorry___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_mkTypeMismatchError___closed__1;
lean_object* l_Lean_Elab_Term_tryPostponeIfHasMVars_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -579,8 +580,8 @@ lean_object* l_Lean_Elab_Term_mkTypeMismatchError_match__1___rarg(lean_object*,
lean_object* l___regBuiltin_Lean_Elab_Term_elabCharLit(lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabOptLevel___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFnsAux_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_6167_(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577_(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_6266_(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633_(lean_object*);
lean_object* l_Lean_mkAuxName___at_Lean_Elab_Term_mkAuxName___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_setElabConfig(lean_object*);
lean_object* l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__4;
@ -589,8 +590,8 @@ lean_object* l_Lean_Elab_Term_liftLevelM___rarg(lean_object*, lean_object*, lean
extern lean_object* l_myMacro____x40_Init_Notation___hyg_12458____closed__12;
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_848_(lean_object*);
lean_object* l_Std_PersistentArray_forMAux___at_Lean_Elab_Term_instMetaEvalTermElabM___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_6167____closed__1;
lean_object* l_Lean_Meta_whnfD___at_Lean_Elab_Term_evalExpr___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__5;
lean_object* l_Lean_Syntax_getId(lean_object*);
extern lean_object* l_Lean_Parser_Tactic_letrec___closed__1;
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux_match__2(lean_object*);
@ -688,6 +689,7 @@ lean_object* l_Lean_Meta_withLCtx___at_Lean_Elab_Term_elabSyntheticHole___spec__
lean_object* l_Lean_ResolveName_resolveGlobalName(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Term_evalExpr___spec__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Term_mkConst___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_pushInfoTree___at_Lean_Elab_Term_addTermInfo___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_bind___at_Lean_Elab_Term_instMonadLogTermElabM___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_forMAux___at_Lean_Elab_Term_instMetaEvalTermElabM___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_isLetRecAuxMVar___closed__6;
@ -719,6 +721,7 @@ lean_object* l_Lean_InternalExceptionId_getName(lean_object*, lean_object*);
lean_object* l_Lean_MetavarContext_getDelayedRoot(lean_object*, lean_object*);
extern lean_object* l_Lean_NameSet_empty;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_instMetaEvalTermElabM___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_LVal_getRef(lean_object*);
lean_object* l_Lean_Elab_Term_withAutoBoundImplicitLocal(lean_object*);
lean_object* l_Lean_Elab_Term_elabSyntheticHole___closed__4;
extern lean_object* l_Lean_Parser_Term_cdot___elambda__1___closed__2;
@ -821,6 +824,7 @@ lean_object* l_Lean_Elab_Term_elabRawNatLit_match__1(lean_object*);
lean_object* l_Lean_Elab_Term_elabBadCDot___rarg___closed__3;
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryLiftAndCoe___closed__3;
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImplicitLambdaAux___closed__1;
extern lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_CheckAssignment_addAssignmentInfo___closed__3;
extern lean_object* l_Lean_resolveGlobalConstNoOverload___rarg___lambda__1___closed__2;
lean_object* l___regBuiltin_Lean_Elab_Term_elabNumLit___closed__1;
extern lean_object* l_Array_foldlMUnsafe_fold___at_Lean_withNestedTraces___spec__5___closed__1;
@ -833,6 +837,7 @@ lean_object* l_Lean_Meta_getLocalDecl(lean_object*, lean_object*, lean_object*,
extern lean_object* l_Lean_Elab_postponeExceptionId;
lean_object* l_Lean_Elab_throwPostpone___at_Lean_Elab_Term_tryPostpone___spec__1___rarg(lean_object*);
lean_object* lean_environment_main_module(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__1;
lean_object* l_Lean_Elab_Term_mkTermElabAttributeUnsafe___closed__9;
lean_object* l___private_Lean_Elab_InfoTree_0__Lean_Elab_getResetInfoTrees___at_Lean_Elab_Term_withMacroExpansion___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_addAutoBoundImplicits_match__1___boxed(lean_object*, lean_object*);
@ -841,12 +846,12 @@ extern lean_object* l_Lean_resetTraceState___rarg___lambda__1___closed__1;
lean_object* l_List_map___at_Lean_MessageData_instCoeListExprMessageData___spec__1(lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Term_throwTypeMismatchError___spec__1(lean_object*);
lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__2;
lean_object* l_Lean_Elab_Term_elabScientificLit(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_instMonadInfoTreeTermElabM___closed__1;
uint8_t l_Lean_Expr_isMVar(lean_object*);
lean_object* l_Lean_Elab_Term_mkFreshIdent___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_addAutoBoundImplicits___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_8147____closed__1;
lean_object* l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Term_elabDoubleQuotedName___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__6;
lean_object* l_Lean_Elab_Term_logUnassignedUsingErrorInfos___closed__1;
@ -896,6 +901,7 @@ lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImplicitLambda___b
lean_object* l_Lean_Elab_Term_applyAttributes(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabNumLit_match__1(lean_object*);
lean_object* l_Lean_Elab_Term_resolveId_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_addTermInfo(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_panic_fn(lean_object*, lean_object*);
lean_object* l_Lean_Meta_withLocalDecl___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImplicitLambda___spec__1___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_metavar_ctx_assign_level(lean_object*, lean_object*, lean_object*);
@ -923,6 +929,7 @@ lean_object* l_Lean_Elab_logAt___at_Lean_Elab_Term_traceAtCmdPos___spec__3___box
lean_object* l_Std_HashMapImp_find_x3f___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFns___spec__5(lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_compileDecl___at_Lean_Elab_Term_evalExpr___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__4;
lean_object* l_Lean_Elab_Term_mkAuxName_match__1(lean_object*);
lean_object* l_Lean_Elab_Term_tryPostponeIfMVar___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImplicitLambda___lambda__1(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -994,11 +1001,11 @@ lean_object* l_Lean_Meta_withLCtx___at_Lean_Elab_Term_elabSyntheticHole___spec__
lean_object* l_Lean_Elab_Term_withFreshMacroScope___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_TermElabM_toIO_match__1(lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isNone(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__3;
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryCoeSort___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_inferType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_InfoTree_0__Lean_Elab_getResetInfoTrees___at_Lean_Elab_Term_withMacroExpansion___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabDoubleQuotedName_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_LVal_getRef_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_evalExpr___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Term_resolveId_x3f___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_instInhabitedMessageData___closed__1;
@ -1087,7 +1094,7 @@ lean_object* l_IO_println___at_Lean_instEval___spec__1(lean_object*, lean_object
lean_object* l_Lean_Elab_Term_logUnassignedUsingErrorInfos_match__2___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_throwErrorIfErrors(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_NameSet_contains(lean_object*, lean_object*);
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_8147_(lean_object*);
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_8246_(lean_object*);
lean_object* l_Lean_Elab_Term_elabByTactic_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_addAutoBoundImplicits(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_withAutoBoundImplicitLocal___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1153,6 +1160,7 @@ lean_object* l_Lean_Elab_Term_throwMVarError(lean_object*);
lean_object* l_Lean_Elab_Term_elabDoubleQuotedName___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_instMetaEvalTermElabM___spec__12___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Term_resolveId_x3f___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_pushInfoTree___at_Lean_Elab_Term_addTermInfo___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_instMetaEvalTermElabM___spec__10___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_tryPostponeIfHasMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_find_x3f___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFns___spec__2(lean_object*, lean_object*);
@ -1219,6 +1227,7 @@ lean_object* l_Lean_Elab_Term_MVarErrorInfo_logError___closed__8;
uint8_t l_Lean_LocalContext_isSubPrefixOf(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabSyntheticHole___closed__3;
lean_object* l_Lean_Syntax_formatStxAux(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_LVal_getRef_match__1(lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryPureCoe_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabBadCDot___rarg___closed__1;
lean_object* l_Lean_Meta_isType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1273,7 +1282,6 @@ lean_object* l_Lean_Meta_whnfD___at_Lean_Elab_Term_evalExpr___spec__3(lean_objec
extern lean_object* l_Lean_Elab_instInhabitedInfoState___closed__1;
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___closed__1;
uint8_t l_Lean_Syntax_isIdent(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__5;
lean_object* l_ReaderT_bind___at_Lean_Elab_Term_instMonadLogTermElabM___spec__2(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Elab_Term_Context_mayPostpone___default;
@ -4184,42 +4192,120 @@ x_2 = l_Lean_Elab_Term_mkTermElabAttributeUnsafe(x_1);
return x_2;
}
}
lean_object* l_Lean_Elab_Term_LVal_getRef_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
switch (lean_obj_tag(x_1)) {
case 0:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7;
lean_dec(x_4);
lean_dec(x_3);
x_5 = lean_ctor_get(x_1, 0);
lean_inc(x_5);
x_6 = lean_ctor_get(x_1, 1);
lean_inc(x_6);
lean_dec(x_1);
x_7 = lean_apply_2(x_2, x_5, x_6);
return x_7;
}
case 1:
{
lean_object* x_8; lean_object* x_9; lean_object* x_10;
lean_dec(x_4);
lean_dec(x_2);
x_8 = lean_ctor_get(x_1, 0);
lean_inc(x_8);
x_9 = lean_ctor_get(x_1, 1);
lean_inc(x_9);
lean_dec(x_1);
x_10 = lean_apply_2(x_3, x_8, x_9);
return x_10;
}
default:
{
lean_object* x_11; lean_object* x_12; lean_object* x_13;
lean_dec(x_3);
lean_dec(x_2);
x_11 = lean_ctor_get(x_1, 0);
lean_inc(x_11);
x_12 = lean_ctor_get(x_1, 1);
lean_inc(x_12);
lean_dec(x_1);
x_13 = lean_apply_2(x_4, x_11, x_12);
return x_13;
}
}
}
}
lean_object* l_Lean_Elab_Term_LVal_getRef_match__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Term_LVal_getRef_match__1___rarg), 4, 0);
return x_2;
}
}
lean_object* l_Lean_Elab_Term_LVal_getRef(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
return x_2;
}
}
lean_object* l_Lean_Elab_Term_LVal_getRef___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Elab_Term_LVal_getRef(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* l_Lean_Elab_Term_instToStringLVal_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
switch (lean_obj_tag(x_1)) {
case 0:
{
lean_object* x_5; lean_object* x_6;
lean_object* x_5; lean_object* x_6; lean_object* x_7;
lean_dec(x_4);
lean_dec(x_3);
x_5 = lean_ctor_get(x_1, 0);
lean_inc(x_5);
x_6 = lean_ctor_get(x_1, 1);
lean_inc(x_6);
lean_dec(x_1);
x_6 = lean_apply_1(x_2, x_5);
return x_6;
x_7 = lean_apply_2(x_2, x_5, x_6);
return x_7;
}
case 1:
{
lean_object* x_7; lean_object* x_8;
lean_object* x_8; lean_object* x_9; lean_object* x_10;
lean_dec(x_4);
lean_dec(x_2);
x_7 = lean_ctor_get(x_1, 0);
lean_inc(x_7);
x_8 = lean_ctor_get(x_1, 0);
lean_inc(x_8);
x_9 = lean_ctor_get(x_1, 1);
lean_inc(x_9);
lean_dec(x_1);
x_8 = lean_apply_1(x_3, x_7);
return x_8;
x_10 = lean_apply_2(x_3, x_8, x_9);
return x_10;
}
default:
{
lean_object* x_9; lean_object* x_10;
lean_object* x_11; lean_object* x_12; lean_object* x_13;
lean_dec(x_3);
lean_dec(x_2);
x_9 = lean_ctor_get(x_1, 0);
lean_inc(x_9);
x_11 = lean_ctor_get(x_1, 0);
lean_inc(x_11);
x_12 = lean_ctor_get(x_1, 1);
lean_inc(x_12);
lean_dec(x_1);
x_10 = lean_apply_1(x_4, x_9);
return x_10;
x_13 = lean_apply_2(x_4, x_11, x_12);
return x_13;
}
}
}
@ -4239,7 +4325,7 @@ switch (lean_obj_tag(x_1)) {
case 0:
{
lean_object* x_2; lean_object* x_3;
x_2 = lean_ctor_get(x_1, 0);
x_2 = lean_ctor_get(x_1, 1);
lean_inc(x_2);
lean_dec(x_1);
x_3 = l_Nat_repr(x_2);
@ -4248,7 +4334,7 @@ return x_3;
case 1:
{
lean_object* x_4;
x_4 = lean_ctor_get(x_1, 0);
x_4 = lean_ctor_get(x_1, 1);
lean_inc(x_4);
lean_dec(x_1);
return x_4;
@ -4256,7 +4342,7 @@ return x_4;
default:
{
lean_object* x_5; lean_object* x_6; uint8_t x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_5 = lean_ctor_get(x_1, 0);
x_5 = lean_ctor_get(x_1, 1);
lean_inc(x_5);
lean_dec(x_1);
x_6 = lean_box(0);
@ -10538,7 +10624,7 @@ x_42 = l_Lean_KernelException_toMessageData___closed__15;
x_43 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_43, 0, x_42);
lean_ctor_set(x_43, 1, x_41);
x_44 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_CheckAssignment_addAssignmentInfo___rarg___closed__3;
x_44 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_CheckAssignment_addAssignmentInfo___closed__3;
x_45 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_45, 0, x_43);
lean_ctor_set(x_45, 1, x_44);
@ -10571,7 +10657,7 @@ x_54 = l_Lean_KernelException_toMessageData___closed__15;
x_55 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_55, 0, x_54);
lean_ctor_set(x_55, 1, x_53);
x_56 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_CheckAssignment_addAssignmentInfo___rarg___closed__3;
x_56 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_CheckAssignment_addAssignmentInfo___closed__3;
x_57 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_57, 0, x_55);
lean_ctor_set(x_57, 1, x_56);
@ -11382,7 +11468,7 @@ x_1 = lean_unsigned_to_nat(16u);
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__1() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__1() {
_start:
{
lean_object* x_1;
@ -11390,17 +11476,17 @@ x_1 = lean_mk_string("maxCoeSize");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__2() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__1;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__3() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
@ -11410,7 +11496,7 @@ lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__4() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__4() {
_start:
{
lean_object* x_1;
@ -11418,13 +11504,13 @@ x_1 = lean_mk_string("maximum number of instances used to construct an automatic
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__5() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__3;
x_1 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__3;
x_2 = l_Lean_instInhabitedParserDescr___closed__1;
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__4;
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__4;
x_4 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -11432,12 +11518,12 @@ lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577_(lean_object* x_1) {
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__2;
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__5;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__2;
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__5;
x_4 = lean_register_option(x_2, x_3, x_1);
return x_4;
}
@ -11446,7 +11532,7 @@ lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_getCoeMaxSize(lean_obj
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__2;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__2;
x_3 = l_Lean_Elab_Term_maxCoeSizeDefault;
x_4 = l_Lean_KVMap_getNat(x_1, x_2, x_3);
return x_4;
@ -26869,6 +26955,303 @@ x_14 = l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux(x_1, x_12, x_13,
return x_14;
}
}
lean_object* l_Lean_Elab_pushInfoTree___at_Lean_Elab_Term_addTermInfo___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; uint8_t x_14;
x_9 = lean_st_ref_get(x_7, x_8);
x_10 = lean_ctor_get(x_9, 1);
lean_inc(x_10);
lean_dec(x_9);
x_11 = lean_st_ref_get(x_3, x_10);
x_12 = lean_ctor_get(x_11, 0);
lean_inc(x_12);
x_13 = lean_ctor_get(x_12, 5);
lean_inc(x_13);
lean_dec(x_12);
x_14 = lean_ctor_get_uint8(x_13, sizeof(void*)*2);
lean_dec(x_13);
if (x_14 == 0)
{
uint8_t x_15;
lean_dec(x_1);
x_15 = !lean_is_exclusive(x_11);
if (x_15 == 0)
{
lean_object* x_16; lean_object* x_17;
x_16 = lean_ctor_get(x_11, 0);
lean_dec(x_16);
x_17 = lean_box(0);
lean_ctor_set(x_11, 0, x_17);
return x_11;
}
else
{
lean_object* x_18; lean_object* x_19; lean_object* x_20;
x_18 = lean_ctor_get(x_11, 1);
lean_inc(x_18);
lean_dec(x_11);
x_19 = lean_box(0);
x_20 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_20, 0, x_19);
lean_ctor_set(x_20, 1, x_18);
return x_20;
}
}
else
{
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; uint8_t x_28;
x_21 = lean_ctor_get(x_11, 1);
lean_inc(x_21);
lean_dec(x_11);
x_22 = lean_st_ref_get(x_7, x_21);
x_23 = lean_ctor_get(x_22, 1);
lean_inc(x_23);
lean_dec(x_22);
x_24 = lean_st_ref_take(x_3, x_23);
x_25 = lean_ctor_get(x_24, 0);
lean_inc(x_25);
x_26 = lean_ctor_get(x_25, 5);
lean_inc(x_26);
x_27 = lean_ctor_get(x_24, 1);
lean_inc(x_27);
lean_dec(x_24);
x_28 = !lean_is_exclusive(x_25);
if (x_28 == 0)
{
lean_object* x_29; uint8_t x_30;
x_29 = lean_ctor_get(x_25, 5);
lean_dec(x_29);
x_30 = !lean_is_exclusive(x_26);
if (x_30 == 0)
{
lean_object* x_31; lean_object* x_32; lean_object* x_33; uint8_t x_34;
x_31 = lean_ctor_get(x_26, 1);
x_32 = l_Std_PersistentArray_push___rarg(x_31, x_1);
lean_ctor_set(x_26, 1, x_32);
x_33 = lean_st_ref_set(x_3, x_25, x_27);
x_34 = !lean_is_exclusive(x_33);
if (x_34 == 0)
{
lean_object* x_35; lean_object* x_36;
x_35 = lean_ctor_get(x_33, 0);
lean_dec(x_35);
x_36 = lean_box(0);
lean_ctor_set(x_33, 0, x_36);
return x_33;
}
else
{
lean_object* x_37; lean_object* x_38; lean_object* x_39;
x_37 = lean_ctor_get(x_33, 1);
lean_inc(x_37);
lean_dec(x_33);
x_38 = lean_box(0);
x_39 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_39, 0, x_38);
lean_ctor_set(x_39, 1, x_37);
return x_39;
}
}
else
{
uint8_t x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49;
x_40 = lean_ctor_get_uint8(x_26, sizeof(void*)*2);
x_41 = lean_ctor_get(x_26, 0);
x_42 = lean_ctor_get(x_26, 1);
lean_inc(x_42);
lean_inc(x_41);
lean_dec(x_26);
x_43 = l_Std_PersistentArray_push___rarg(x_42, x_1);
x_44 = lean_alloc_ctor(0, 2, 1);
lean_ctor_set(x_44, 0, x_41);
lean_ctor_set(x_44, 1, x_43);
lean_ctor_set_uint8(x_44, sizeof(void*)*2, x_40);
lean_ctor_set(x_25, 5, x_44);
x_45 = lean_st_ref_set(x_3, x_25, x_27);
x_46 = lean_ctor_get(x_45, 1);
lean_inc(x_46);
if (lean_is_exclusive(x_45)) {
lean_ctor_release(x_45, 0);
lean_ctor_release(x_45, 1);
x_47 = x_45;
} else {
lean_dec_ref(x_45);
x_47 = lean_box(0);
}
x_48 = lean_box(0);
if (lean_is_scalar(x_47)) {
x_49 = lean_alloc_ctor(0, 2, 0);
} else {
x_49 = x_47;
}
lean_ctor_set(x_49, 0, x_48);
lean_ctor_set(x_49, 1, x_46);
return x_49;
}
}
else
{
lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; uint8_t x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66;
x_50 = lean_ctor_get(x_25, 0);
x_51 = lean_ctor_get(x_25, 1);
x_52 = lean_ctor_get(x_25, 2);
x_53 = lean_ctor_get(x_25, 3);
x_54 = lean_ctor_get(x_25, 4);
lean_inc(x_54);
lean_inc(x_53);
lean_inc(x_52);
lean_inc(x_51);
lean_inc(x_50);
lean_dec(x_25);
x_55 = lean_ctor_get_uint8(x_26, sizeof(void*)*2);
x_56 = lean_ctor_get(x_26, 0);
lean_inc(x_56);
x_57 = lean_ctor_get(x_26, 1);
lean_inc(x_57);
if (lean_is_exclusive(x_26)) {
lean_ctor_release(x_26, 0);
lean_ctor_release(x_26, 1);
x_58 = x_26;
} else {
lean_dec_ref(x_26);
x_58 = lean_box(0);
}
x_59 = l_Std_PersistentArray_push___rarg(x_57, x_1);
if (lean_is_scalar(x_58)) {
x_60 = lean_alloc_ctor(0, 2, 1);
} else {
x_60 = x_58;
}
lean_ctor_set(x_60, 0, x_56);
lean_ctor_set(x_60, 1, x_59);
lean_ctor_set_uint8(x_60, sizeof(void*)*2, x_55);
x_61 = lean_alloc_ctor(0, 6, 0);
lean_ctor_set(x_61, 0, x_50);
lean_ctor_set(x_61, 1, x_51);
lean_ctor_set(x_61, 2, x_52);
lean_ctor_set(x_61, 3, x_53);
lean_ctor_set(x_61, 4, x_54);
lean_ctor_set(x_61, 5, x_60);
x_62 = lean_st_ref_set(x_3, x_61, x_27);
x_63 = lean_ctor_get(x_62, 1);
lean_inc(x_63);
if (lean_is_exclusive(x_62)) {
lean_ctor_release(x_62, 0);
lean_ctor_release(x_62, 1);
x_64 = x_62;
} else {
lean_dec_ref(x_62);
x_64 = lean_box(0);
}
x_65 = lean_box(0);
if (lean_is_scalar(x_64)) {
x_66 = lean_alloc_ctor(0, 2, 0);
} else {
x_66 = x_64;
}
lean_ctor_set(x_66, 0, x_65);
lean_ctor_set(x_66, 1, x_63);
return x_66;
}
}
}
}
lean_object* l_Lean_Elab_Term_addTermInfo(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
_start:
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; uint8_t x_15;
x_10 = lean_st_ref_get(x_8, x_9);
x_11 = lean_ctor_get(x_10, 1);
lean_inc(x_11);
lean_dec(x_10);
x_12 = lean_st_ref_get(x_4, x_11);
x_13 = lean_ctor_get(x_12, 0);
lean_inc(x_13);
x_14 = lean_ctor_get(x_13, 5);
lean_inc(x_14);
lean_dec(x_13);
x_15 = lean_ctor_get_uint8(x_14, sizeof(void*)*2);
lean_dec(x_14);
if (x_15 == 0)
{
uint8_t x_16;
lean_dec(x_2);
lean_dec(x_1);
x_16 = !lean_is_exclusive(x_12);
if (x_16 == 0)
{
lean_object* x_17; lean_object* x_18;
x_17 = lean_ctor_get(x_12, 0);
lean_dec(x_17);
x_18 = lean_box(0);
lean_ctor_set(x_12, 0, x_18);
return x_12;
}
else
{
lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_19 = lean_ctor_get(x_12, 1);
lean_inc(x_19);
lean_dec(x_12);
x_20 = lean_box(0);
x_21 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_19);
return x_21;
}
}
else
{
lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28;
x_22 = lean_ctor_get(x_12, 1);
lean_inc(x_22);
lean_dec(x_12);
x_23 = lean_ctor_get(x_5, 1);
lean_inc(x_23);
x_24 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_24, 0, x_23);
lean_ctor_set(x_24, 1, x_2);
lean_ctor_set(x_24, 2, x_1);
x_25 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_25, 0, x_24);
x_26 = l_Std_PersistentArray_empty___closed__1;
x_27 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_27, 0, x_25);
lean_ctor_set(x_27, 1, x_26);
x_28 = l_Lean_Elab_pushInfoTree___at_Lean_Elab_Term_addTermInfo___spec__1(x_27, x_3, x_4, x_5, x_6, x_7, x_8, x_22);
return x_28;
}
}
}
lean_object* l_Lean_Elab_pushInfoTree___at_Lean_Elab_Term_addTermInfo___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
lean_object* x_9;
x_9 = l_Lean_Elab_pushInfoTree___at_Lean_Elab_Term_addTermInfo___spec__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
return x_9;
}
}
lean_object* l_Lean_Elab_Term_addTermInfo___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
_start:
{
lean_object* x_10;
x_10 = l_Lean_Elab_Term_addTermInfo(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
return x_10;
}
}
lean_object* l_Lean_Elab_Term_mkTermInfo_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
@ -30689,7 +31072,7 @@ lean_dec(x_3);
return x_9;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_6167____closed__1() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_6266____closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -30699,11 +31082,11 @@ x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_6167_(lean_object* x_1) {
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_6266_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_6167____closed__1;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_6266____closed__1;
x_3 = l_Lean_registerTraceClass(x_2, x_1);
return x_3;
}
@ -30874,7 +31257,7 @@ lean_object* x_97; lean_object* x_98; lean_object* x_99; lean_object* x_100; lea
x_97 = lean_ctor_get(x_91, 1);
lean_inc(x_97);
lean_dec(x_91);
x_98 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_6167____closed__1;
x_98 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_6266____closed__1;
x_99 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__2(x_98, x_2, x_3, x_4, x_5, x_6, x_7, x_97);
x_100 = lean_ctor_get(x_99, 0);
lean_inc(x_100);
@ -30916,7 +31299,7 @@ lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean
x_53 = lean_ctor_get(x_47, 1);
lean_inc(x_53);
lean_dec(x_47);
x_54 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_6167____closed__1;
x_54 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_6266____closed__1;
x_55 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__2(x_54, x_2, x_3, x_4, x_5, x_6, x_7, x_53);
x_56 = lean_ctor_get(x_55, 0);
lean_inc(x_56);
@ -30997,7 +31380,7 @@ x_41 = l_Lean_KernelException_toMessageData___closed__15;
x_42 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_42, 0, x_40);
lean_ctor_set(x_42, 1, x_41);
x_43 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_6167____closed__1;
x_43 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_6266____closed__1;
x_44 = l_Lean_addTrace___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__1(x_43, x_42, x_2, x_3, x_4, x_5, x_6, x_7, x_36);
x_45 = lean_ctor_get(x_44, 1);
lean_inc(x_45);
@ -31059,7 +31442,7 @@ x_79 = l_Lean_KernelException_toMessageData___closed__15;
x_80 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_80, 0, x_78);
lean_ctor_set(x_80, 1, x_79);
x_81 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_6167____closed__1;
x_81 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_6266____closed__1;
x_82 = l_Lean_addTrace___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__1(x_81, x_80, x_2, x_3, x_4, x_5, x_6, x_7, x_61);
x_83 = lean_ctor_get(x_82, 1);
lean_inc(x_83);
@ -41322,7 +41705,7 @@ lean_dec(x_1);
return x_10;
}
}
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_8147____closed__1() {
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_8246____closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -41332,7 +41715,7 @@ x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_8147_(lean_object* x_1) {
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_8246_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -41344,7 +41727,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
lean_dec(x_3);
x_5 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_8147____closed__1;
x_5 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_8246____closed__1;
x_6 = l_Lean_registerTraceClass(x_5, x_4);
if (lean_obj_tag(x_6) == 0)
{
@ -41666,17 +42049,17 @@ l_Lean_Elab_Term_synthesizeInstMVarCore___closed__6 = _init_l_Lean_Elab_Term_syn
lean_mark_persistent(l_Lean_Elab_Term_synthesizeInstMVarCore___closed__6);
l_Lean_Elab_Term_maxCoeSizeDefault = _init_l_Lean_Elab_Term_maxCoeSizeDefault();
lean_mark_persistent(l_Lean_Elab_Term_maxCoeSizeDefault);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__1();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__1);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__2();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__2);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__3 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__3();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__3);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__4 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__4();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__4);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__5 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__5();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577____closed__5);
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2577_(lean_io_mk_world());
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__1();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__1);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__2();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__2);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__3 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__3();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__3);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__4 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__4();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__4);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__5 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__5();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633____closed__5);
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_2633_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_Term_tryCoeThunk_x3f_match__1___rarg___closed__1 = _init_l_Lean_Elab_Term_tryCoeThunk_x3f_match__1___rarg___closed__1();
@ -41793,9 +42176,9 @@ l_Lean_Elab_Term_mkAuxName___closed__2 = _init_l_Lean_Elab_Term_mkAuxName___clos
lean_mark_persistent(l_Lean_Elab_Term_mkAuxName___closed__2);
l_Lean_Elab_Term_mkAuxName___closed__3 = _init_l_Lean_Elab_Term_mkAuxName___closed__3();
lean_mark_persistent(l_Lean_Elab_Term_mkAuxName___closed__3);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_6167____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_6167____closed__1();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_6167____closed__1);
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_6167_(lean_io_mk_world());
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_6266____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_6266____closed__1();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_6266____closed__1);
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_6266_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_Term_isLetRecAuxMVar___closed__1 = _init_l_Lean_Elab_Term_isLetRecAuxMVar___closed__1();
@ -41989,9 +42372,9 @@ l_Lean_Elab_Term_evalExpr___rarg___closed__3 = _init_l_Lean_Elab_Term_evalExpr__
lean_mark_persistent(l_Lean_Elab_Term_evalExpr___rarg___closed__3);
l_Lean_Elab_Term_evalExpr___rarg___closed__4 = _init_l_Lean_Elab_Term_evalExpr___rarg___closed__4();
lean_mark_persistent(l_Lean_Elab_Term_evalExpr___rarg___closed__4);
l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_8147____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_8147____closed__1();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_8147____closed__1);
res = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_8147_(lean_io_mk_world());
l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_8246____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_8246____closed__1();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_8246____closed__1);
res = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_8246_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));

4
stage0/stdlib/Lean/Expr.c generated
View file

@ -487,10 +487,10 @@ lean_object* lean_expr_update_proj(lean_object*, lean_object*);
lean_object* l_Lean_Expr_setPPExplicit___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Level_instantiateParams___at_Lean_Expr_instantiateLevelParamsArray___spec__3(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_looseBVarRange(lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__20;
lean_object* l_Lean_Expr_bvarIdx_x21(lean_object*);
lean_object* l_Lean_Expr_updateProj_x21___closed__2;
lean_object* l_Lean_Expr_constName_x21_match__1___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__20;
lean_object* l_Lean_Expr_consumeMData_match__1(lean_object*);
lean_object* l_Lean_Expr_bindingBody_x21_match__1(lean_object*);
lean_object* l_Lean_Expr_setAppPPExplicit(lean_object*);
@ -3388,7 +3388,7 @@ return x_12;
default:
{
lean_object* x_13;
x_13 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__20;
x_13 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__20;
return x_13;
}
}

5484
stage0/stdlib/Lean/Meta/ExprDefEq.c generated
View file

File diff suppressed because it is too large Load diff

2390
stage0/stdlib/Lean/Meta/Match/Match.c generated
View file

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

1586
stage0/stdlib/Lean/Parser/Transform.c generated
View file

File diff suppressed because it is too large Load diff

4
stage0/stdlib/Lean/PrettyPrinter/Delaborator/Basic.c generated
View file

@ -195,9 +195,9 @@ lean_object* l_Lean_PrettyPrinter_Delaborator_failure___boxed(lean_object*, lean
extern lean_object* l_Lean_Meta_synthInstance_x3f___lambda__2___closed__4;
lean_object* l_Lean_getPPCoercions___boxed(lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_withAppFn___rarg___closed__4;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__20;
lean_object* l_Lean_registerInternalExceptionId(lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_mkAppUnexpanderAttribute___closed__4;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__20;
lean_object* l_Lean_PrettyPrinter_Delaborator_mkDelabAttribute___closed__11;
lean_object* l_Lean_PrettyPrinter_delab(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Lean_Meta_WHNF_0__Lean_Meta_whnfEasyCases___closed__1;
@ -2111,7 +2111,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_5890____closed__20;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6168____closed__20;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}