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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2021-03-30 13:32:06 -07:00
parent 9f9529467e
commit 687ce2fe67
42 changed files with 5741 additions and 5107 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
stage0/src/Init/Data/Repr.lean generated
View file

@ -244,3 +244,5 @@ instance : ReprAtom UInt16 := ⟨⟩
instance : ReprAtom UInt32 := ⟨⟩
instance : ReprAtom UInt64 := ⟨⟩
instance : ReprAtom USize := ⟨⟩
deriving instance Repr for Lean.SourceInfo

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

@ -166,6 +166,11 @@ partial def getTailInfo? : Syntax → Option SourceInfo
def getTailInfo (stx : Syntax) : SourceInfo :=
stx.getTailInfo?.getD SourceInfo.none
def getTrailingSize (stx : Syntax) : Nat :=
match stx.getTailInfo? with
| some (SourceInfo.original (trailing := trailing) ..) => trailing.bsize
| _ => 0
@[specialize] private partial def updateLast {α} [Inhabited α] (a : Array α) (f : α → Option α) (i : Nat) : Option (Array α) :=
if i == 0 then
none

2
stage0/src/Init/Prelude.lean generated
View file

@ -1764,7 +1764,7 @@ partial def getTailPos? (stx : Syntax) (originalOnly := false) : Option String.P
| node _ args, _ =>
let rec loop (i : Nat) : Option String.Pos :=
match decide (Less i args.size) with
| true => match getTailPos? (args.get! ((args.size.sub i).sub 1)) with
| true => match getTailPos? (args.get! ((args.size.sub i).sub 1)) originalOnly with
| some info => some info
| none => loop (hAdd i 1)
| false => none

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

@ -391,7 +391,8 @@ private def expandMatchAltsIntoMatchAux (matchAlts : Syntax) (matchTactic : Bool
`(match $[$discrs:term],* with $matchAlts:matchAlts)
| n+1, discrs => withFreshMacroScope do
let x ← `(x)
let body ← expandMatchAltsIntoMatchAux matchAlts matchTactic n (discrs.push x)
let d ← `(@$x:ident) -- See comment below
let body ← expandMatchAltsIntoMatchAux matchAlts matchTactic n (discrs.push d)
if matchTactic then
`(tactic| intro $x:term; $body:tactic)
else
@ -407,17 +408,31 @@ private def expandMatchAltsIntoMatchAux (matchAlts : Syntax) (matchTactic : Bool
expands into (for tactic == false)
```
fun x_1 x_2 =>
match x_1, x_2 with
match @x_1, @x_2 with
| 0, true => alt_1
| i, _ => alt_2
```
and (for tactic == true)
```
intro x_1; intro x_2;
match x_1, x_2 with
match @x_1, @x_2 with
| 0, true => alt_1
| i, _ => alt_2
```
Remark: we add `@` to make sure we don't consume implicit arguments, and to make the behavior consistent with `fun`.
Example:
```
inductive T : Type 1 :=
| mkT : (forall {a : Type}, a -> a) -> T
def makeT (f : forall {a : Type}, a -> a) : T :=
mkT f
def makeT' : (forall {a : Type}, a -> a) -> T
| f => mkT f
```
The two definitions should be elaborated without errors and be equivalent.
-/
def expandMatchAltsIntoMatch (ref : Syntax) (matchAlts : Syntax) (tactic := false) : MacroM Syntax :=
withRef ref <| expandMatchAltsIntoMatchAux matchAlts tactic (getMatchAltsNumPatterns matchAlts) #[]
@ -466,7 +481,8 @@ def expandMatchAltsWhereDecls (matchAltsWhereDecls : Syntax) : MacroM Syntax :=
expandWhereDeclsOpt whereDeclsOpt matchStx
| n+1 => withFreshMacroScope do
let x ← `(x)
let body ← loop n (discrs.push x)
let d ← `(@$x:ident) -- See comment at `expandMatchAltsIntoMatch`
let body ← loop n (discrs.push d)
`(@fun $x => $body)
loop (getMatchAltsNumPatterns matchAlts) #[]

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

@ -76,6 +76,16 @@ inductive InfoTree where
| hole (mvarId : MVarId) -- The elaborator creates holes (aka metavariables) for tactics and postponed terms
deriving Inhabited
partial def InfoTree.findInfo? (p : Info → Bool) (t : InfoTree) : Option InfoTree :=
match t with
| context _ t => findInfo? p t
| node i ts =>
if p i then
some t
else
ts.findSome? (findInfo? p)
| _ => none
structure InfoState where
enabled : Bool := false
assignment : PersistentHashMap MVarId InfoTree := {} -- map from holeId to InfoTree

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

@ -34,10 +34,6 @@ private def expandSimpleMatch (stx discr lhsVar rhs : Syntax) (expectedType? : O
let newStx ← `(let $lhsVar := $discr; $rhs)
withMacroExpansion stx newStx <| elabTerm newStx expectedType?
private def expandSimpleMatchWithType (stx discr lhsVar type rhs : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
let newStx ← `(let $lhsVar : $type := $discr; $rhs)
withMacroExpansion stx newStx <| elabTerm newStx expectedType?
private def elabDiscrsWitMatchType (discrStxs : Array Syntax) (matchType : Expr) (expectedType : Expr) : TermElabM (Array Expr × Bool) := do
let mut discrs := #[]
let mut i := 0
@ -68,10 +64,19 @@ private def mkUserNameFor (e : Expr) : TermElabM Name := do
def isAuxDiscrName (n : Name) : Bool :=
n.hasMacroScopes && n.eraseMacroScopes == `_discr
/- We treat `@x` as atomic to avoid unnecessary extra local declarations from being
inserted into the local context. Recall that `expandMatchAltsIntoMatch` uses `@` modifier.
Thus this is kind of discriminant is quite common. -/
def isAtomicDiscr? (discr : Syntax) : TermElabM (Option Expr) := do
match discr with
| `($x:ident) => isLocalIdent? x
| `(@$x:ident) => isLocalIdent? x
| _ => return none
-- See expandNonAtomicDiscrs?
private def elabAtomicDiscr (discr : Syntax) : TermElabM Expr := do
let term := discr[1]
match (← isLocalIdent? term) with
match (← isAtomicDiscr? term) with
| some e@(Expr.fvar fvarId _) =>
let localDecl ← getLocalDecl fvarId
if !isAuxDiscrName localDecl.userName then
@ -959,7 +964,7 @@ private def expandNonAtomicDiscrs? (matchStx : Syntax) : TermElabM (Option Synta
let matchOptType := getMatchOptType matchStx;
if matchOptType.isNone then do
let discrs := getDiscrs matchStx;
let allLocal ← discrs.allM fun discr => Option.isSome <$> isLocalIdent? discr[1]
let allLocal ← discrs.allM fun discr => Option.isSome <$> isAtomicDiscr? discr[1]
if allLocal then
return none
else
@ -981,7 +986,7 @@ private def expandNonAtomicDiscrs? (matchStx : Syntax) : TermElabM (Option Synta
let discrNew := discr.setArg 1 d;
let r ← loop discrs (discrsNew.push discrNew) foundFVars
`(let _discr := $term; $r)
match (← isLocalIdent? term) with
match (← isAtomicDiscr? term) with
| some x => if x.isFVar then loop discrs (discrsNew.push discr) (foundFVars.insert x.fvarId!) else addAux
| none => addAux
return some (← loop discrs.toList #[] {})
@ -1001,7 +1006,7 @@ private def tryPostponeIfDiscrTypeIsMVar (matchStx : Syntax) : TermElabM Unit :=
let discrs := getDiscrs matchStx
for discr in discrs do
let term := discr[1]
match (← isLocalIdent? term) with
match (← isAtomicDiscr? term) with
| none => throwErrorAt discr "unexpected discriminant" -- see `expandNonAtomicDiscrs?
| some d =>
let dType ← inferType d
@ -1077,8 +1082,6 @@ where
match stx with
| `(match $discr:term with | $y:ident => $rhs:term) =>
if (← isPatternVar y) then expandSimpleMatch stx discr y rhs expectedType? else elabMatchDefault stx expectedType?
| `(match $discr:term : $type with | $y:ident => $rhs:term) =>
if (← isPatternVar y) then expandSimpleMatchWithType stx discr y type rhs expectedType? else elabMatchDefault stx expectedType?
| _ => elabMatchDefault stx expectedType?
where
elabMatchDefault (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do

30
stage0/src/Lean/Elab/Tactic/Basic.lean generated
View file

@ -169,6 +169,17 @@ mutual
end
/-
Save the current tactic state for a token `stx`.
This method is a no-op if `stx` has no position information.
We use this method to save the tactic state at punctuation such as `;`
-/
def saveTacticInfoForToken (stx : Syntax) : TacticM Unit := do
unless stx.getPos?.isNone do
let mctxBefore ← getMCtx
let goalsBefore ← getGoals
withInfoContext (pure ()) (mkTacticInfo mctxBefore goalsBefore stx)
/- Elaborate `x` with `stx` on the macro stack -/
@[inline]
def withMacroExpansion {α} (beforeStx afterStx : Syntax) (x : TacticM α) : TacticM α :=
@ -342,17 +353,28 @@ def tagUntaggedGoals (parentTag : Name) (newSuffix : Name) (newGoals : List MVar
idx := idx + 1
pure mctx
@[builtinTactic seq1] def evalSeq1 : Tactic := fun stx =>
stx[0].getSepArgs.forM evalTactic
@[builtinTactic seq1] def evalSeq1 : Tactic := fun stx => do
let args := stx[0].getArgs
for i in [:args.size] do
if i % 2 == 0 then
evalTactic args[i]
else
saveTacticInfoForToken args[i] -- add `TacticInfo` node for `;`
@[builtinTactic paren] def evalParen : Tactic := fun stx =>
evalTactic stx[1]
/- Evaluate `many (group (tactic >> optional ";")) -/
private def evalManyTacticOptSemi (stx : Syntax) : TacticM Unit := do
stx.forArgsM fun seqElem => do
evalTactic seqElem[0]
saveTacticInfoForToken seqElem[1] -- add TacticInfo node for `;`
@[builtinTactic tacticSeq1Indented] def evalTacticSeq1Indented : Tactic := fun stx =>
stx[0].forArgsM fun seqElem => evalTactic seqElem[0]
evalManyTacticOptSemi stx[0]
@[builtinTactic tacticSeqBracketed] def evalTacticSeqBracketed : Tactic := fun stx =>
withRef stx[2] <| focusAndDone <| stx[1].forArgsM fun seqElem => evalTactic seqElem[0]
withRef stx[2] <| focusAndDone <| evalManyTacticOptSemi stx[1]
@[builtinTactic Parser.Tactic.focus] def evalFocus : Tactic := fun stx =>
focus <| evalTactic stx[1]

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

@ -430,9 +430,11 @@ section RequestHandling
withWaitFindSnap doc (fun s => s.endPos > hoverPos)
(notFoundX := return none) fun snap => do
for t in snap.toCmdState.infoState.trees do
if let some (ci, ti) := t.goalsAt? hoverPos then
let ci := { ci with mctx := ti.mctxAfter }
let goals ← ci.runMetaM {} <| ti.goalsAfter.mapM (fun g => Meta.withPPInaccessibleNames (Meta.ppGoal g))
if let rs@(_ :: _) := t.goalsAt? hoverPos then
let goals ← List.join <$> rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter } =>
let ci := if useAfter then { ci with mctx := ti.mctxAfter } else { ci with mctx := ti.mctxBefore }
let goals := if useAfter then ti.goalsAfter else ti.goalsBefore
ci.runMetaM {} <| goals.mapM (fun g => Meta.withPPInaccessibleNames (Meta.ppGoal g))
let md :=
if goals.isEmpty then
"no goals"
@ -574,13 +576,14 @@ section RequestHandling
highlightId (stx : Syntax) : ReaderT SemanticTokensContext (StateT SemanticTokensState IO) _ := do
if let (some pos, some tailPos) := (stx.getPos?, stx.getTailPos?) then
for t in (← read).infoState.trees do
for (ci, i) in t.deepestNodes (fun i => match i.pos? with
| some ipos => pos <= ipos && ipos < tailPos
| _ => false) do
if let Elab.Info.ofTermInfo ti := i then
match ti.expr with
| Expr.fvar .. => addToken ti.stx SemanticTokenType.variable
| _ => if ti.stx.getPos?.get! > pos then addToken ti.stx SemanticTokenType.property
for ti in t.deepestNodes (fun
| _, i@(Elab.Info.ofTermInfo ti) => match i.pos? with
| some ipos => if pos <= ipos && ipos < tailPos then some ti else none
| _ => none
| _, _ => none) do
match ti.expr with
| Expr.fvar .. => addToken ti.stx SemanticTokenType.variable
| _ => if ti.stx.getPos?.get! > pos then addToken ti.stx SemanticTokenType.property
highlightKeyword stx := do
if let Syntax.atom info val := stx then
if val.bsize > 0 && val[0].isAlpha then

55
stage0/src/Lean/Server/InfoUtils.lean generated
View file

@ -13,7 +13,7 @@ namespace Lean.Elab
/--
For every branch, find the deepest node in that branch matching `p`
with a surrounding context (the innermost one) and return all of them. -/
partial def InfoTree.deepestNodes (p : Info → Bool) : InfoTree → List (ContextInfo × Info) :=
partial def InfoTree.deepestNodes (p : ContextInfo → Info → Option α) : InfoTree → List α :=
go none
where go ctx?
| context ctx t => go ctx t
@ -22,9 +22,11 @@ where go ctx?
let ccs := cs.map (go ctx?)
let cs := ccs.join
if !cs.isEmpty then cs
else match ctx?, p i with
| some ctx, true => [(ctx, i)]
| _, _ => []
else match ctx? with
| some ctx => match p ctx i with
| some a => [a]
| _ => []
| _ => []
| _ => []
def Info.stx : Info → Syntax
@ -41,7 +43,7 @@ def Info.tailPos? (i : Info) : Option String.Pos :=
i.stx.getTailPos? (originalOnly := true)
def InfoTree.smallestInfo? (p : Info → Bool) (t : InfoTree) : Option (ContextInfo × Info) :=
let ts := t.deepestNodes p
let ts := t.deepestNodes fun ctx i => if p i then some (ctx, i) else none
let infos := ts.map fun (ci, i) =>
let diff := i.tailPos?.get! - i.pos?.get!
@ -103,27 +105,28 @@ def Info.fmtHover? (ci : ContextInfo) (i : Info) : IO (Option Format) := do
| _ => return none
/-- Return a flattened list of smallest-in-span tactic info nodes, sorted by position. -/
partial def InfoTree.smallestTacticStates (t : InfoTree) : Array (String.Pos × ContextInfo × TacticInfo) :=
let ts := tacticLeaves t
let ts := ts.filterMap fun
| (ci, i@(Info.ofTacticInfo ti)) => some (i.pos?.get!, ci, ti)
| _ => none
ts.toArray.qsort fun a b => a.1 < b.1
where tacticLeaves t :=
t.deepestNodes fun
| i@(Info.ofTacticInfo _) => i.pos?.isSome ∧ i.tailPos?.isSome
| _ => false
structure GoalsAtResult where
ctxInfo : ContextInfo
tacticInfo : TacticInfo
useAfter : Bool
partial def InfoTree.goalsAt? (t : InfoTree) (hoverPos : String.Pos) : Option (ContextInfo × TacticInfo) :=
let ts := t.smallestTacticStates
-- The extent of a tactic state is (pos, pos of next tactic)
let extents := ts.mapIdx fun i (p, _, ti) =>
(p, if h : (i.val+1) < ts.size then
ts.get ⟨i.val+1, h⟩ |>.1
else
ti.stx.getTailPos?.get!)
let idx? := extents.findIdx? fun (p, tp) => p ≤ hoverPos ∧ hoverPos < tp
idx?.map fun idx => ts.get! idx |> fun (_, ci, ti) => (ci, ti)
/-
Try to retrieve `TacticInfo` for `hoverPos`.
We retrieve the `TacticInfo` `info`, if there is a node of the form `node (ofTacticInfo info) children` s.t.
- If `hoverPos <= headPos && hoverPos < endPos + getTrailingSize` and
- None of the `children` can provide satisfy the condition above. That is, for composite tactics such as
`induction`, we always give preference for information stored in nested (children) tactics.
Moreover, we instruct the LSP server to use the state after the tactic execution If hoverPos >= endPos
-/
partial def InfoTree.goalsAt? (t : InfoTree) (hoverPos : String.Pos) : List GoalsAtResult := do
t.deepestNodes fun
| ctx, i@(Info.ofTacticInfo ti) => OptionM.run do
let (some pos, some tailPos) ← pure (i.pos?, i.tailPos?)
| failure
let trailSize := i.stx.getTrailingSize
guard <| pos ≤ hoverPos ∧ hoverPos < tailPos + trailSize
return { ctxInfo := ctx, tacticInfo := ti, useAfter := hoverPos >= tailPos }
| _, _ => none
end Lean.Elab

489
stage0/stdlib/Init/Data/Repr.c generated
View file

@ -25,6 +25,7 @@ lean_object* l_instReprIterator(lean_object*, lean_object*);
lean_object* l_instReprPUnit___closed__2;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_1346____closed__7;
lean_object* l_instReprOption___rarg___closed__1;
lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__13;
lean_object* l_instReprOption___rarg(lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_div(lean_object*, lean_object*);
lean_object* l_instReprSigma___rarg___closed__2;
@ -40,6 +41,7 @@ extern lean_object* l_Std_Format_defWidth;
lean_object* l_instReprProd(lean_object*, lean_object*);
lean_object* l_Char_repr(uint32_t);
lean_object* l_instReprDecidable___rarg___closed__3;
lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__5;
lean_object* l_instReprProd___rarg___closed__2;
lean_object* l_instReprChar(uint32_t, lean_object*);
lean_object* l_instReprProd___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -48,6 +50,7 @@ extern lean_object* l_Lean_instInhabitedParserDescr___closed__1;
lean_object* l_instReprPUnit___boxed(lean_object*, lean_object*);
lean_object* l_Nat_toSuperDigitsAux_match__1(lean_object*);
lean_object* l_instReprSigma___rarg___closed__1;
lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__7;
lean_object* l_instReprUSize(size_t, lean_object*);
lean_object* l_instReprNat(lean_object*, lean_object*);
lean_object* l_instReprBool___closed__1;
@ -70,7 +73,9 @@ extern lean_object* l_Std_Format_sbracket___closed__4;
lean_object* l_Std_Format_joinSep___at_instReprProd___spec__1(lean_object*, lean_object*);
lean_object* l_String_quote___closed__1;
lean_object* l_String_quote___boxed(lean_object*);
lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348_(lean_object*, lean_object*);
extern lean_object* l_Std_Format_paren___closed__2;
lean_object* l_instReprSourceInfo;
lean_object* lean_string_utf8_byte_size(lean_object*);
lean_object* l_instReprProd___rarg___closed__1;
lean_object* l_instReprDecidable___rarg___closed__4;
@ -78,15 +83,18 @@ lean_object* l_instReprBool___closed__2;
lean_object* l_String_quote___lambda__1___boxed(lean_object*, lean_object*);
lean_object* l_instReprId___rarg___boxed(lean_object*);
lean_object* l_Std_Format_joinSep___at_instReprList___spec__1(lean_object*);
lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348__match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_instReprAtomNat;
lean_object* l_instReprSum___rarg___closed__2;
lean_object* l_String_quote___closed__3;
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_instReprBool_match__1___rarg(uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_instReprAtomUInt16;
lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__3;
lean_object* l_instReprBool___closed__4;
lean_object* l_Char_quoteCore___closed__1;
lean_object* l_Char_quoteCore___boxed(lean_object*);
extern lean_object* l_Int_Int_pow___closed__1;
lean_object* l_instReprOption___rarg___closed__3;
lean_object* l_instReprDecidable_match__1___rarg(uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_reprStr___rarg(lean_object*, lean_object*);
@ -100,6 +108,7 @@ lean_object* l_instReprDecidable(lean_object*);
lean_object* l_instReprFin___boxed(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_reprArg___rarg(lean_object*, lean_object*);
lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__10;
lean_object* l_instReprTuple(lean_object*);
lean_object* l_instReprSubstring___boxed(lean_object*, lean_object*);
lean_object* l_instReprString(lean_object*, lean_object*);
@ -113,6 +122,8 @@ lean_object* l_instReprIterator___closed__1;
lean_object* l_instReprList___rarg___closed__1;
lean_object* l_instReprIterator___boxed(lean_object*, lean_object*);
lean_object* l_Std_Format_joinSep___at_instReprList___spec__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348__match__1(lean_object*);
lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__12;
lean_object* l_instReprInt(lean_object*, lean_object*);
lean_object* l_repr___rarg(lean_object*, lean_object*);
lean_object* l_instReprAtomUSize;
@ -163,7 +174,9 @@ lean_object* l_instReprSubstring(lean_object*, lean_object*);
lean_object* l_instReprDecidable_match__1(lean_object*, lean_object*);
lean_object* l_Char_quoteCore___closed__3;
lean_object* l_instReprULift___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__11;
extern lean_object* l_term_x2d_____closed__3;
lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__9;
uint8_t l_UInt32_decEq(uint32_t, uint32_t);
extern lean_object* l_term_x5b___x5d___closed__5;
lean_object* l_instReprString___boxed(lean_object*, lean_object*);
@ -204,8 +217,11 @@ lean_object* l_instReprULift___rarg___closed__2;
lean_object* l_instReprSigma(lean_object*, lean_object*);
lean_object* lean_uint64_to_nat(uint64_t);
lean_object* l_instReprULift___rarg___closed__1;
lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__1;
lean_object* l_instReprDecidable_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_instReprSigma___rarg___closed__4;
lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__2;
lean_object* lean_string_length(lean_object*);
lean_object* l_instReprTupleProd_match__1___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_Format_sbracket___closed__2;
@ -220,11 +236,14 @@ lean_object* l_instReprFin___rarg(lean_object*, lean_object*);
lean_object* lean_uint16_to_nat(uint16_t);
lean_object* l_repr(lean_object*);
lean_object* lean_usize_to_nat(size_t);
lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__6;
lean_object* l_Nat_toDigitsCore_match__1(lean_object*);
lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__8;
lean_object* l_instReprOption___rarg___closed__4;
lean_object* l_Char_quoteCore(uint32_t);
lean_object* l_instReprOption(lean_object*);
lean_object* l_instReprSigma___rarg___closed__6;
lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____boxed(lean_object*, lean_object*);
lean_object* l_instReprChar___boxed(lean_object*, lean_object*);
lean_object* lean_uint32_to_nat(uint32_t);
lean_object* l_instReprList__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -244,6 +263,7 @@ lean_object* l_instReprSum___rarg(lean_object*, lean_object*, lean_object*, lean
lean_object* l_instReprOption_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_reprArg(lean_object*);
lean_object* l_Repr_addAppParen(lean_object*, lean_object*);
lean_object* l_instReprSourceInfo___closed__1;
lean_object* l_instReprNat___boxed(lean_object*, lean_object*);
lean_object* l_repr___rarg(lean_object* x_1, lean_object* x_2) {
_start:
@ -2962,6 +2982,445 @@ x_1 = lean_box(0);
return x_1;
}
}
lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348__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_object* x_8;
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);
x_7 = lean_ctor_get(x_1, 2);
lean_inc(x_7);
lean_dec(x_1);
x_8 = lean_apply_3(x_2, x_5, x_6, x_7);
return x_8;
}
case 1:
{
lean_object* x_9; lean_object* x_10; lean_object* x_11;
lean_dec(x_4);
lean_dec(x_2);
x_9 = lean_ctor_get(x_1, 0);
lean_inc(x_9);
x_10 = lean_ctor_get(x_1, 1);
lean_inc(x_10);
lean_dec(x_1);
x_11 = lean_apply_2(x_3, x_9, x_10);
return x_11;
}
default:
{
lean_object* x_12; lean_object* x_13;
lean_dec(x_3);
lean_dec(x_2);
x_12 = lean_box(0);
x_13 = lean_apply_1(x_4, x_12);
return x_13;
}
}
}
}
lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348__match__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348__match__1___rarg), 4, 0);
return x_2;
}
}
static lean_object* _init_l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Lean.SourceInfo.original");
return x_1;
}
}
static lean_object* _init_l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__1;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__2;
x_2 = lean_box(1);
x_3 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(2u);
x_2 = lean_nat_to_int(x_1);
return x_2;
}
}
static lean_object* _init_l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Lean.SourceInfo.synthetic");
return x_1;
}
}
static lean_object* _init_l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__5;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__6;
x_2 = lean_box(1);
x_3 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__8() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Lean.SourceInfo.none");
return x_1;
}
}
static lean_object* _init_l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__8;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
x_2 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__9;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__11() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__10;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__12() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Int_Int_pow___closed__1;
x_2 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__9;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__13() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__12;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348_(lean_object* x_1, lean_object* x_2) {
_start:
{
switch (lean_obj_tag(x_1)) {
case 0:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7; lean_object* x_8; lean_object* x_9;
x_3 = lean_ctor_get(x_1, 0);
lean_inc(x_3);
x_4 = lean_ctor_get(x_1, 1);
lean_inc(x_4);
x_5 = lean_ctor_get(x_1, 2);
lean_inc(x_5);
lean_dec(x_1);
x_6 = lean_unsigned_to_nat(1024u);
x_7 = lean_nat_dec_le(x_6, x_2);
x_8 = l_Nat_repr(x_4);
x_9 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_9, 0, x_8);
if (x_7 == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; uint8_t x_34; lean_object* x_35; lean_object* x_36;
x_10 = lean_ctor_get(x_3, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_3, 1);
lean_inc(x_11);
x_12 = lean_ctor_get(x_3, 2);
lean_inc(x_12);
lean_dec(x_3);
x_13 = lean_string_utf8_extract(x_10, x_11, x_12);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_10);
x_14 = l_String_quote(x_13);
lean_dec(x_13);
x_15 = l_instReprSubstring___closed__1;
x_16 = lean_string_append(x_14, x_15);
x_17 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_17, 0, x_16);
x_18 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__3;
x_19 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_19, 0, x_18);
lean_ctor_set(x_19, 1, x_17);
x_20 = lean_box(1);
x_21 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_21, 0, x_19);
lean_ctor_set(x_21, 1, x_20);
x_22 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_22, 0, x_21);
lean_ctor_set(x_22, 1, x_9);
x_23 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_23, 0, x_22);
lean_ctor_set(x_23, 1, x_20);
x_24 = lean_ctor_get(x_5, 0);
lean_inc(x_24);
x_25 = lean_ctor_get(x_5, 1);
lean_inc(x_25);
x_26 = lean_ctor_get(x_5, 2);
lean_inc(x_26);
lean_dec(x_5);
x_27 = lean_string_utf8_extract(x_24, x_25, x_26);
lean_dec(x_26);
lean_dec(x_25);
lean_dec(x_24);
x_28 = l_String_quote(x_27);
lean_dec(x_27);
x_29 = lean_string_append(x_28, x_15);
x_30 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_30, 0, x_29);
x_31 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_31, 0, x_23);
lean_ctor_set(x_31, 1, x_30);
x_32 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
x_33 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_33, 0, x_32);
lean_ctor_set(x_33, 1, x_31);
x_34 = 0;
x_35 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_35, 0, x_33);
lean_ctor_set_uint8(x_35, sizeof(void*)*1, x_34);
x_36 = l_Repr_addAppParen(x_35, x_2);
return x_36;
}
else
{
lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; uint8_t x_61; lean_object* x_62; lean_object* x_63;
x_37 = lean_ctor_get(x_3, 0);
lean_inc(x_37);
x_38 = lean_ctor_get(x_3, 1);
lean_inc(x_38);
x_39 = lean_ctor_get(x_3, 2);
lean_inc(x_39);
lean_dec(x_3);
x_40 = lean_string_utf8_extract(x_37, x_38, x_39);
lean_dec(x_39);
lean_dec(x_38);
lean_dec(x_37);
x_41 = l_String_quote(x_40);
lean_dec(x_40);
x_42 = l_instReprSubstring___closed__1;
x_43 = lean_string_append(x_41, x_42);
x_44 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_44, 0, x_43);
x_45 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__3;
x_46 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_46, 0, x_45);
lean_ctor_set(x_46, 1, x_44);
x_47 = lean_box(1);
x_48 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_48, 0, x_46);
lean_ctor_set(x_48, 1, x_47);
x_49 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_49, 0, x_48);
lean_ctor_set(x_49, 1, x_9);
x_50 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_50, 0, x_49);
lean_ctor_set(x_50, 1, x_47);
x_51 = lean_ctor_get(x_5, 0);
lean_inc(x_51);
x_52 = lean_ctor_get(x_5, 1);
lean_inc(x_52);
x_53 = lean_ctor_get(x_5, 2);
lean_inc(x_53);
lean_dec(x_5);
x_54 = lean_string_utf8_extract(x_51, x_52, x_53);
lean_dec(x_53);
lean_dec(x_52);
lean_dec(x_51);
x_55 = l_String_quote(x_54);
lean_dec(x_54);
x_56 = lean_string_append(x_55, x_42);
x_57 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_57, 0, x_56);
x_58 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_58, 0, x_50);
lean_ctor_set(x_58, 1, x_57);
x_59 = l_Int_Int_pow___closed__1;
x_60 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_60, 0, x_59);
lean_ctor_set(x_60, 1, x_58);
x_61 = 0;
x_62 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_62, 0, x_60);
lean_ctor_set_uint8(x_62, sizeof(void*)*1, x_61);
x_63 = l_Repr_addAppParen(x_62, x_2);
return x_63;
}
}
case 1:
{
lean_object* x_64; lean_object* x_65; lean_object* x_66; uint8_t x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76;
x_64 = lean_ctor_get(x_1, 0);
lean_inc(x_64);
x_65 = lean_ctor_get(x_1, 1);
lean_inc(x_65);
lean_dec(x_1);
x_66 = lean_unsigned_to_nat(1024u);
x_67 = lean_nat_dec_le(x_66, x_2);
x_68 = l_Nat_repr(x_64);
x_69 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_69, 0, x_68);
x_70 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__7;
x_71 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_71, 0, x_70);
lean_ctor_set(x_71, 1, x_69);
x_72 = lean_box(1);
x_73 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_73, 0, x_71);
lean_ctor_set(x_73, 1, x_72);
x_74 = l_Nat_repr(x_65);
x_75 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_75, 0, x_74);
x_76 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_76, 0, x_73);
lean_ctor_set(x_76, 1, x_75);
if (x_67 == 0)
{
lean_object* x_77; lean_object* x_78; uint8_t x_79; lean_object* x_80; lean_object* x_81;
x_77 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
x_78 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_78, 0, x_77);
lean_ctor_set(x_78, 1, x_76);
x_79 = 0;
x_80 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_80, 0, x_78);
lean_ctor_set_uint8(x_80, sizeof(void*)*1, x_79);
x_81 = l_Repr_addAppParen(x_80, x_2);
return x_81;
}
else
{
lean_object* x_82; lean_object* x_83; uint8_t x_84; lean_object* x_85; lean_object* x_86;
x_82 = l_Int_Int_pow___closed__1;
x_83 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_83, 0, x_82);
lean_ctor_set(x_83, 1, x_76);
x_84 = 0;
x_85 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_85, 0, x_83);
lean_ctor_set_uint8(x_85, sizeof(void*)*1, x_84);
x_86 = l_Repr_addAppParen(x_85, x_2);
return x_86;
}
}
default:
{
lean_object* x_87; uint8_t x_88;
x_87 = lean_unsigned_to_nat(1024u);
x_88 = lean_nat_dec_le(x_87, x_2);
if (x_88 == 0)
{
lean_object* x_89; lean_object* x_90;
x_89 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__11;
x_90 = l_Repr_addAppParen(x_89, x_2);
return x_90;
}
else
{
lean_object* x_91; lean_object* x_92;
x_91 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__13;
x_92 = l_Repr_addAppParen(x_91, x_2);
return x_92;
}
}
}
}
}
lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348_(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
static lean_object* _init_l_instReprSourceInfo___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____boxed), 2, 0);
return x_1;
}
}
static lean_object* _init_l_instReprSourceInfo() {
_start:
{
lean_object* x_1;
x_1 = l_instReprSourceInfo___closed__1;
return x_1;
}
}
lean_object* initialize_Init_Data_Format_Basic(lean_object*);
lean_object* initialize_Init_Data_Int_Basic(lean_object*);
lean_object* initialize_Init_Data_Nat_Div(lean_object*);
@ -3099,6 +3558,36 @@ l_instReprAtomUInt64 = _init_l_instReprAtomUInt64();
lean_mark_persistent(l_instReprAtomUInt64);
l_instReprAtomUSize = _init_l_instReprAtomUSize();
lean_mark_persistent(l_instReprAtomUSize);
l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__1 = _init_l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__1();
lean_mark_persistent(l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__1);
l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__2 = _init_l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__2();
lean_mark_persistent(l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__2);
l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__3 = _init_l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__3();
lean_mark_persistent(l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__3);
l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4 = _init_l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4();
lean_mark_persistent(l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4);
l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__5 = _init_l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__5();
lean_mark_persistent(l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__5);
l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__6 = _init_l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__6();
lean_mark_persistent(l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__6);
l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__7 = _init_l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__7();
lean_mark_persistent(l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__7);
l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__8 = _init_l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__8();
lean_mark_persistent(l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__8);
l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__9 = _init_l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__9();
lean_mark_persistent(l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__9);
l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__10 = _init_l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__10();
lean_mark_persistent(l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__10);
l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__11 = _init_l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__11();
lean_mark_persistent(l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__11);
l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__12 = _init_l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__12();
lean_mark_persistent(l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__12);
l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__13 = _init_l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__13();
lean_mark_persistent(l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__13);
l_instReprSourceInfo___closed__1 = _init_l_instReprSourceInfo___closed__1();
lean_mark_persistent(l_instReprSourceInfo___closed__1);
l_instReprSourceInfo = _init_l_instReprSourceInfo();
lean_mark_persistent(l_instReprSourceInfo);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

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

File diff suppressed because it is too large Load diff

65
stage0/stdlib/Init/Prelude.c generated
View file

@ -430,7 +430,7 @@ lean_object* l_UInt32_ofNatCore___boxed(lean_object*, lean_object*);
lean_object* l_decEq(lean_object*);
lean_object* l_or___boxed(lean_object*, lean_object*);
lean_object* l_Lean_withRef___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getTailPos_x3f_loop___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getTailPos_x3f_loop___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_pred(lean_object*);
lean_object* l_instHAppend(lean_object*);
lean_object* l_throwThe(lean_object*, lean_object*);
@ -455,7 +455,7 @@ lean_object* l_List_set___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_EStateM_instMonadEStateM___closed__1;
lean_object* l_Array_appendCore_loop___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_instDecidableOr(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getTailPos_x3f_loop(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getTailPos_x3f_loop(uint8_t, lean_object*, lean_object*);
lean_object* l_Monad_seq___default(lean_object*);
lean_object* l_Monad_seqLeft___default___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_instMonadLiftT__1___rarg___boxed(lean_object*);
@ -9169,46 +9169,45 @@ x_10 = l_Lean_Syntax_getTailPos_x3f_match__1___rarg(x_1, x_9, x_3, x_4, x_5, x_6
return x_10;
}
}
lean_object* l_Lean_Syntax_getTailPos_x3f_loop(lean_object* x_1, lean_object* x_2) {
lean_object* l_Lean_Syntax_getTailPos_x3f_loop(uint8_t x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_3; uint8_t x_4;
x_3 = lean_array_get_size(x_1);
x_4 = lean_nat_dec_lt(x_2, x_3);
if (x_4 == 0)
lean_object* x_4; uint8_t x_5;
x_4 = lean_array_get_size(x_2);
x_5 = lean_nat_dec_lt(x_3, x_4);
if (x_5 == 0)
{
lean_object* x_5;
lean_object* x_6;
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_5 = lean_box(0);
return x_5;
x_6 = lean_box(0);
return x_6;
}
else
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12;
x_6 = lean_nat_sub(x_3, x_2);
lean_dec(x_3);
x_7 = lean_unsigned_to_nat(1u);
x_8 = lean_nat_sub(x_6, x_7);
lean_dec(x_6);
x_9 = l_Lean_instInhabitedSyntax;
x_10 = lean_array_get(x_9, x_1, x_8);
lean_dec(x_8);
x_11 = 0;
x_12 = l_Lean_Syntax_getTailPos_x3f(x_10, x_11);
lean_dec(x_10);
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_7 = lean_nat_sub(x_4, x_3);
lean_dec(x_4);
x_8 = lean_unsigned_to_nat(1u);
x_9 = lean_nat_sub(x_7, x_8);
lean_dec(x_7);
x_10 = l_Lean_instInhabitedSyntax;
x_11 = lean_array_get(x_10, x_2, x_9);
lean_dec(x_9);
x_12 = l_Lean_Syntax_getTailPos_x3f(x_11, x_1);
lean_dec(x_11);
if (lean_obj_tag(x_12) == 0)
{
lean_object* x_13;
x_13 = lean_nat_add(x_2, x_7);
lean_dec(x_2);
x_2 = x_13;
x_13 = lean_nat_add(x_3, x_8);
lean_dec(x_3);
x_3 = x_13;
goto _start;
}
else
{
uint8_t x_15;
lean_dec(x_2);
lean_dec(x_3);
x_15 = !lean_is_exclusive(x_12);
if (x_15 == 0)
{
@ -9243,7 +9242,7 @@ case 1:
lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = lean_ctor_get(x_1, 1);
x_5 = lean_unsigned_to_nat(0u);
x_6 = l_Lean_Syntax_getTailPos_x3f_loop(x_4, x_5);
x_6 = l_Lean_Syntax_getTailPos_x3f_loop(x_2, x_4, x_5);
return x_6;
}
case 2:
@ -9337,13 +9336,15 @@ return x_28;
}
}
}
lean_object* l_Lean_Syntax_getTailPos_x3f_loop___boxed(lean_object* x_1, lean_object* x_2) {
lean_object* l_Lean_Syntax_getTailPos_x3f_loop___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_Syntax_getTailPos_x3f_loop(x_1, x_2);
uint8_t x_4; lean_object* x_5;
x_4 = lean_unbox(x_1);
lean_dec(x_1);
return x_3;
x_5 = l_Lean_Syntax_getTailPos_x3f_loop(x_4, x_2, x_3);
lean_dec(x_2);
return x_5;
}
}
lean_object* l_Lean_Syntax_getTailPos_x3f___boxed(lean_object* x_1, lean_object* x_2) {

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

@ -192,7 +192,6 @@ lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatIRType___close
lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatParam_match__1___rarg(lean_object*, lean_object*);
lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatCtorInfo(lean_object*);
extern lean_object* l_instReprIterator___closed__3;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__4;
lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatParam(lean_object*);
lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatParam_match__1(lean_object*);
lean_object* l_Lean_IR_formatDecl___closed__4;
@ -218,6 +217,7 @@ lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatExpr___closed_
lean_object* l_Lean_IR_formatFnBodyHead___closed__4;
lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatCtorInfo_match__1___rarg(lean_object*, lean_object*);
lean_object* l_Lean_IR_formatFnBodyHead___closed__9;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__4;
lean_object* l_Lean_IR_formatAlt_match__1(lean_object*);
lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatIRType___closed__1;
lean_object* l_Lean_IR_formatFnBody_loop___closed__5;
@ -3588,7 +3588,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_6247____closed__4;
x_15 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____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);
@ -3681,7 +3681,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_6247____closed__4;
x_55 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____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);
@ -3789,7 +3789,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_6247____closed__4;
x_105 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____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);
@ -4141,7 +4141,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_6247____closed__4;
x_17 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____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);
@ -4291,7 +4291,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_6247____closed__4;
x_84 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____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);
@ -4427,7 +4427,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_6247____closed__4;
x_148 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____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

@ -72,7 +72,6 @@ lean_object* lean_nat_abs(lean_object*);
lean_object* l_Lean_instToFormatDataValue_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_Format_getUnicode___closed__1;
lean_object* l_Std_Format_getUnicode___boxed(lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__4;
lean_object* l_Std_Format_getUnicode___closed__2;
lean_object* l_Lean_KVMap_findCore(lean_object*, lean_object*);
lean_object* l_Lean_Option_register___at_Std_Format_initFn____x40_Lean_Data_Format___hyg_53____spec__1___boxed(lean_object*, lean_object*, lean_object*);
@ -84,6 +83,7 @@ extern lean_object* l_Std_Format_sbracket___closed__2;
lean_object* l_Std_Format_getWidth___closed__1;
lean_object* l_Std_Format_getWidth___boxed(lean_object*);
lean_object* l_Lean_instToFormatProdNameDataValue(lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__4;
lean_object* l_Std_Format_getWidth___closed__3;
lean_object* l_Std_Format_initFn____x40_Lean_Data_Format___hyg_25____closed__1;
static lean_object* _init_l_Std_Format_getWidth___closed__1() {
@ -865,7 +865,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_6247____closed__4;
x_7 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____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);
@ -1018,7 +1018,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_6247____closed__4;
x_11 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____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);
@ -1156,7 +1156,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_6247____closed__4;
x_55 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____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);

4
stage0/stdlib/Lean/Data/Lsp/Diagnostics.c generated
View file

@ -97,7 +97,6 @@ lean_object* l_Lean_Lsp_PublishDiagnosticsParams_version_x3f___default;
lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l_Lean_Lsp_msgToDiagnostic___closed__2;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
extern lean_object* l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__3;
lean_object* l_Lean_MessageData_toString(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_Diagnostics_0__Lean_Lsp_fromJsonDiagnostic____x40_Lean_Data_Lsp_Diagnostics___hyg_735____boxed(lean_object*);
lean_object* l_Lean_Lsp_instBEqDiagnostic;
@ -212,6 +211,7 @@ lean_object* l___private_Lean_Data_Lsp_Diagnostics_0__Lean_Lsp_beqDiagnosticRela
lean_object* l_Lean_Lsp_instToJsonDiagnosticSeverity___closed__6;
lean_object* l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_594____at___private_Lean_Data_Lsp_Diagnostics_0__Lean_Lsp_beqDiagnostic____x40_Lean_Data_Lsp_Diagnostics___hyg_543____spec__4___boxed(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_Diagnostics_0__Lean_Lsp_beqDiagnosticRelatedInformation____x40_Lean_Data_Lsp_Diagnostics___hyg_367__match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Diagnostics_0__Lean_Lsp_fromJsonDiagnostic____x40_Lean_Data_Lsp_Diagnostics___hyg_735____spec__3___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Lsp_instBEqDiagnosticRelatedInformation___closed__1;
lean_object* l_Lean_Lsp_instFromJsonDiagnosticTag_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -830,7 +830,7 @@ static lean_object* _init_l_Lean_Lsp_instToJsonDiagnosticSeverity___closed__3()
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__3;
x_1 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
x_2 = lean_unsigned_to_nat(0u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);

49
stage0/stdlib/Lean/Data/Lsp/LanguageFeatures.c generated
View file

@ -58,7 +58,6 @@ lean_object* l_Lean_Lsp_instToJsonDocumentSymbolAux___rarg(lean_object*);
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonRange____x40_Lean_Data_Lsp_Basic___hyg_395____spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__12;
lean_object* l_Lean_Lsp_SemanticTokenType_names___closed__6;
lean_object* l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__8;
lean_object* l_Lean_Lsp_instToJsonDocumentSymbol;
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_695____rarg___closed__2;
lean_object* l_Lean_Json_getStr_x3f(lean_object*);
@ -235,6 +234,7 @@ lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__60;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__47;
extern lean_object* l_Lean_JsonNumber_toString___closed__1;
lean_object* l_Lean_Lsp_instFromJsonSemanticTokensParams___closed__1;
extern lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__44;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_695____spec__2___rarg(lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_Lsp_instFromJsonSemanticTokensOptions;
@ -1210,17 +1210,8 @@ return x_2;
static lean_object* _init_l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(2u);
x_2 = lean_nat_to_int(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__3;
x_1 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
x_2 = lean_unsigned_to_nat(0u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -1228,17 +1219,17 @@ lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__5() {
static lean_object* _init_l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__4;
x_1 = l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__3;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__6() {
static lean_object* _init_l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2;
@ -1247,11 +1238,11 @@ x_2 = lean_nat_to_int(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__7() {
static lean_object* _init_l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__6;
x_1 = l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__5;
x_2 = lean_unsigned_to_nat(0u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -1259,11 +1250,11 @@ lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__8() {
static lean_object* _init_l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__7;
x_1 = l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__6;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
@ -1282,13 +1273,13 @@ return x_2;
case 1:
{
lean_object* x_3;
x_3 = l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__5;
x_3 = l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__4;
return x_3;
}
default:
{
lean_object* x_4;
x_4 = l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__8;
x_4 = l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__7;
return x_4;
}
}
@ -1344,7 +1335,7 @@ return x_9;
case 1:
{
lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_10 = l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__5;
x_10 = l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__4;
x_11 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_11, 0, x_1);
lean_ctor_set(x_11, 1, x_10);
@ -1356,7 +1347,7 @@ return x_12;
default:
{
lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_13 = l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__8;
x_13 = l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__7;
x_14 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_14, 0, x_1);
lean_ctor_set(x_14, 1, x_13);
@ -3122,13 +3113,13 @@ return x_2;
case 1:
{
lean_object* x_3;
x_3 = l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__5;
x_3 = l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__4;
return x_3;
}
case 2:
{
lean_object* x_4;
x_4 = l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__8;
x_4 = l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__7;
return x_4;
}
case 3:
@ -3481,14 +3472,14 @@ goto block_38;
case 1:
{
lean_object* x_40;
x_40 = l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__5;
x_40 = l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__4;
x_29 = x_40;
goto block_38;
}
case 2:
{
lean_object* x_41;
x_41 = l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__8;
x_41 = l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__7;
x_29 = x_41;
goto block_38;
}
@ -3864,14 +3855,14 @@ goto block_37;
case 1:
{
lean_object* x_39;
x_39 = l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__5;
x_39 = l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__4;
x_28 = x_39;
goto block_37;
}
case 2:
{
lean_object* x_40;
x_40 = l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__8;
x_40 = l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__7;
x_28 = x_40;
goto block_37;
}
@ -5367,8 +5358,6 @@ l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__6 = _init_l_Lean_Lsp_instTo
lean_mark_persistent(l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__6);
l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__7 = _init_l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__7();
lean_mark_persistent(l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__7);
l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__8 = _init_l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__8();
lean_mark_persistent(l_Lean_Lsp_instToJsonDocumentHighlightKind___closed__8);
l_Lean_Lsp_DocumentHighlight_kind_x3f___default = _init_l_Lean_Lsp_DocumentHighlight_kind_x3f___default();
lean_mark_persistent(l_Lean_Lsp_DocumentHighlight_kind_x3f___default);
l_Lean_Lsp_instToJsonDocumentHighlight___closed__1 = _init_l_Lean_Lsp_instToJsonDocumentHighlight___closed__1();

24
stage0/stdlib/Lean/Data/Lsp/TextSync.c generated
View file

@ -58,7 +58,6 @@ lean_object* l_Lean_Lsp_instToJsonDidCloseTextDocumentParams;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_TextSync_0__Lean_Lsp_toJsonTextDocumentSyncOptions____x40_Lean_Data_Lsp_TextSync___hyg_481_(lean_object*);
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_TextSync_0__Lean_Lsp_fromJsonSaveOptions____x40_Lean_Data_Lsp_TextSync___hyg_382____spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Lsp_instToJsonTextDocumentSyncKind___closed__7;
lean_object* l_Lean_Lsp_instToJsonTextDocumentSyncKind(uint8_t);
lean_object* l_Lean_Lsp_instFromJsonDidOpenTextDocumentParams;
extern lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentItem____x40_Lean_Data_Lsp_Basic___hyg_1155____closed__2;
@ -108,6 +107,7 @@ lean_object* l_Lean_Lsp_instToJsonTextDocumentSyncKind___closed__5;
lean_object* l_Lean_Lsp_instToJsonTextDocumentSyncOptions___closed__1;
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonTextDocumentRegistrationOptions____x40_Lean_Data_Lsp_Basic___hyg_1564____spec__1(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_TextSync_0__Lean_Lsp_toJsonDidOpenTextDocumentParams____x40_Lean_Data_Lsp_TextSync___hyg_64_(lean_object*);
extern lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
lean_object* l_Lean_Lsp_instFromJsonTextDocumentContentChangeEvent(lean_object*);
lean_object* l_Lean_Lsp_instFromJsonTextDocumentSyncKind_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Json_getBool_x3f(lean_object*);
@ -131,7 +131,6 @@ lean_object* l___private_Lean_Data_Lsp_TextSync_0__Lean_Lsp_toJsonTextDocumentSy
lean_object* l_Lean_Lsp_TextDocumentContentChangeEvent_hasToJson(lean_object*);
lean_object* l_Lean_Lsp_TextDocumentChangeRegistrationOptions_documentSelector_x3f___default;
lean_object* l_Lean_Lsp_instFromJsonSaveOptions;
lean_object* lean_nat_to_int(lean_object*);
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_TextSync_0__Lean_Lsp_fromJsonTextDocumentSyncOptions____x40_Lean_Data_Lsp_TextSync___hyg_537____spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonLocation____x40_Lean_Data_Lsp_Basic___hyg_544____spec__2(lean_object*, lean_object*);
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonTextDocumentEdit____x40_Lean_Data_Lsp_Basic___hyg_1104____spec__1(lean_object*, lean_object*);
@ -427,17 +426,8 @@ return x_2;
static lean_object* _init_l_Lean_Lsp_instToJsonTextDocumentSyncKind___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(2u);
x_2 = lean_nat_to_int(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Lsp_instToJsonTextDocumentSyncKind___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Lsp_instToJsonTextDocumentSyncKind___closed__5;
x_1 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
x_2 = lean_unsigned_to_nat(0u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -445,11 +435,11 @@ lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Lsp_instToJsonTextDocumentSyncKind___closed__7() {
static lean_object* _init_l_Lean_Lsp_instToJsonTextDocumentSyncKind___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Lsp_instToJsonTextDocumentSyncKind___closed__6;
x_1 = l_Lean_Lsp_instToJsonTextDocumentSyncKind___closed__5;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
@ -474,7 +464,7 @@ return x_3;
default:
{
lean_object* x_4;
x_4 = l_Lean_Lsp_instToJsonTextDocumentSyncKind___closed__7;
x_4 = l_Lean_Lsp_instToJsonTextDocumentSyncKind___closed__6;
return x_4;
}
}
@ -1692,7 +1682,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_change___closed__1;
x_2 = l_Lean_Lsp_instToJsonTextDocumentSyncKind___closed__7;
x_2 = l_Lean_Lsp_instToJsonTextDocumentSyncKind___closed__6;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -2092,8 +2082,6 @@ l_Lean_Lsp_instToJsonTextDocumentSyncKind___closed__5 = _init_l_Lean_Lsp_instToJ
lean_mark_persistent(l_Lean_Lsp_instToJsonTextDocumentSyncKind___closed__5);
l_Lean_Lsp_instToJsonTextDocumentSyncKind___closed__6 = _init_l_Lean_Lsp_instToJsonTextDocumentSyncKind___closed__6();
lean_mark_persistent(l_Lean_Lsp_instToJsonTextDocumentSyncKind___closed__6);
l_Lean_Lsp_instToJsonTextDocumentSyncKind___closed__7 = _init_l_Lean_Lsp_instToJsonTextDocumentSyncKind___closed__7();
lean_mark_persistent(l_Lean_Lsp_instToJsonTextDocumentSyncKind___closed__7);
l_Lean_Lsp_instToJsonDidOpenTextDocumentParams___closed__1 = _init_l_Lean_Lsp_instToJsonDidOpenTextDocumentParams___closed__1();
lean_mark_persistent(l_Lean_Lsp_instToJsonDidOpenTextDocumentParams___closed__1);
l_Lean_Lsp_instToJsonDidOpenTextDocumentParams = _init_l_Lean_Lsp_instToJsonDidOpenTextDocumentParams();

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

@ -58,29 +58,30 @@ lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*);
lean_object* l_Lean_FileMap_toPosition_loop___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_FileMap_ofString(lean_object*);
lean_object* l___private_Lean_Data_Position_0__Lean_reprPosition____x40_Lean_Data_Position___hyg_117____closed__2;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__29;
lean_object* l___private_Lean_Data_Position_0__Lean_reprPosition____x40_Lean_Data_Position___hyg_117____closed__5;
lean_object* l_Lean_FileMap_toPosition_toColumn___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_instDecidableEqPosition(lean_object*, lean_object*);
lean_object* l_Lean_Position_instToStringPosition(lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__28;
lean_object* l_Lean_FileMap_toPosition_loop(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_UInt32_decEq(uint32_t, uint32_t);
extern lean_object* l_term_x5b___x5d___closed__5;
lean_object* l___private_Lean_Data_Position_0__Lean_reprPosition____x40_Lean_Data_Position___hyg_117____closed__6;
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__29;
lean_object* l_Array_back___at_Lean_FileMap_toPosition___spec__1(lean_object*);
lean_object* l_Array_back___at_Lean_FileMap_toPosition___spec__2___boxed(lean_object*);
lean_object* l_Array_back___at_Lean_FileMap_toPosition___spec__2(lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__28;
lean_object* l_Lean_instDecidableEqPosition___boxed(lean_object*, lean_object*);
lean_object* l_Lean_instInhabitedFileMap___closed__1;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__4;
lean_object* l_Lean_Position_instToFormatPosition(lean_object*);
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_117_(lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__4;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__27;
lean_object* l___private_Lean_Data_Position_0__Lean_reprPosition____x40_Lean_Data_Position___hyg_117____closed__4;
extern lean_object* l_instReprSigma___rarg___closed__6;
uint8_t lean_string_utf8_at_end(lean_object*, lean_object*);
@ -88,7 +89,6 @@ lean_object* l_Lean_Position_lt___boxed(lean_object*, lean_object*);
lean_object* l_Lean_FileMap_toPosition___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Position_lt___closed__2;
lean_object* l_Lean_instInhabitedFileMap;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__27;
lean_object* l_Nat_decEq___boxed(lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_String_toFileMap(lean_object*);
@ -225,7 +225,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_117____closed__3;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__4;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____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);
@ -275,7 +275,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_6247____closed__4;
x_14 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____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);
@ -288,15 +288,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_6247____closed__28;
x_20 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__28;
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_6247____closed__29;
x_22 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__29;
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_6247____closed__27;
x_24 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__27;
x_25 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_25, 0, x_24);
lean_ctor_set(x_25, 1, x_23);

16
stage0/stdlib/Lean/Data/Trie.c generated
View file

@ -20,7 +20,6 @@ lean_object* l_Lean_Parser_Trie_insert_insertEmpty(lean_object*);
lean_object* l_Lean_Parser_Trie_find_x3f(lean_object*);
lean_object* l_Lean_Parser_Trie_insert_loop_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBNode_insert___at_Lean_Parser_Trie_insert_loop___spec__2___rarg(lean_object*, uint32_t, lean_object*);
lean_object* l_Std_RBNode_fold___at___private_Lean_Data_Trie_0__Lean_Parser_Trie_toStringAux___spec__1___rarg___closed__1;
lean_object* l___private_Lean_Data_Trie_0__Lean_Parser_Trie_updtAcc_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBNode_insert___at_Lean_Parser_Trie_insert_loop___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Trie_insert_loop___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -88,6 +87,7 @@ lean_object* l_Char_quote(uint32_t);
lean_object* l_Std_RBNode_ins___at_Lean_Parser_Trie_insert_loop___spec__3(lean_object*);
lean_object* l_Lean_Parser_Trie_find_x3f___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Std_RBNode_ins___at_Lean_Parser_Trie_insert_loop___spec__6___rarg___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
lean_object* l_Std_RBNode_insert___at_Lean_Parser_Trie_insert_loop___spec__5___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBNode_ins___at_Lean_Parser_Trie_insert_loop___spec__3___rarg(lean_object*, uint32_t, lean_object*);
lean_object* l_Std_RBNode_fold___at___private_Lean_Data_Trie_0__Lean_Parser_Trie_toStringAux___spec__1(lean_object*);
@ -96,7 +96,6 @@ lean_object* l_Std_RBNode_ins___at_Lean_Parser_Trie_insert_loop___spec__4(lean_o
lean_object* l_Std_RBNode_insert___at_Lean_Parser_Trie_insert_loop___spec__5(lean_object*);
lean_object* l_Std_RBNode_insert___at_Lean_Parser_Trie_insert_loop___spec__2(lean_object*);
uint8_t lean_string_utf8_at_end(lean_object*, lean_object*);
lean_object* lean_nat_to_int(lean_object*);
lean_object* l___private_Lean_Data_Trie_0__Lean_Parser_Trie_updtAcc___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Trie_find_x3f_loop___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Trie_insert(lean_object*);
@ -11052,15 +11051,6 @@ x_3 = lean_alloc_closure((void*)(l___private_Lean_Data_Trie_0__Lean_Parser_Trie_
return x_3;
}
}
static lean_object* _init_l_Std_RBNode_fold___at___private_Lean_Data_Trie_0__Lean_Parser_Trie_toStringAux___spec__1___rarg___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(2u);
x_2 = lean_nat_to_int(x_1);
return x_2;
}
}
lean_object* l_Std_RBNode_fold___at___private_Lean_Data_Trie_0__Lean_Parser_Trie_toStringAux___spec__1___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -11090,7 +11080,7 @@ x_11 = l___private_Lean_Data_Trie_0__Lean_Parser_Trie_toStringAux___rarg(x_5);
x_12 = lean_box(1);
x_13 = l_Std_Format_joinSep___at_instReprProd___spec__1(x_11, x_12);
lean_dec(x_11);
x_14 = l_Std_RBNode_fold___at___private_Lean_Data_Trie_0__Lean_Parser_Trie_toStringAux___spec__1___rarg___closed__1;
x_14 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
x_15 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_15, 0, x_14);
lean_ctor_set(x_15, 1, x_13);
@ -11176,8 +11166,6 @@ l_Lean_Parser_Trie_empty___closed__1 = _init_l_Lean_Parser_Trie_empty___closed__
lean_mark_persistent(l_Lean_Parser_Trie_empty___closed__1);
l_Lean_Parser_Trie_instEmptyCollectionTrie___closed__1 = _init_l_Lean_Parser_Trie_instEmptyCollectionTrie___closed__1();
lean_mark_persistent(l_Lean_Parser_Trie_instEmptyCollectionTrie___closed__1);
l_Std_RBNode_fold___at___private_Lean_Data_Trie_0__Lean_Parser_Trie_toStringAux___spec__1___rarg___closed__1 = _init_l_Std_RBNode_fold___at___private_Lean_Data_Trie_0__Lean_Parser_Trie_toStringAux___spec__1___rarg___closed__1();
lean_mark_persistent(l_Std_RBNode_fold___at___private_Lean_Data_Trie_0__Lean_Parser_Trie_toStringAux___spec__1___rarg___closed__1);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

104
stage0/stdlib/Lean/Declaration.c generated
View file

@ -174,6 +174,7 @@ lean_object* l_Lean_ConstantInfo_isUnsafe_match__1(lean_object*);
lean_object* l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__14;
lean_object* l_Lean_instInhabitedDeclaration;
lean_object* l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__5;
extern lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
lean_object* l_Lean_instInhabitedTheoremVal;
lean_object* lean_mk_opaque_val(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
lean_object* l_Lean_ConstantInfo_numLevelParams___boxed(lean_object*);
@ -181,7 +182,6 @@ lean_object* l_Lean_InductiveVal_nctors(lean_object*);
lean_object* l_Lean_ReducibilityHints_lt_match__1(lean_object*);
lean_object* l_List_foldlM___at_Lean_Declaration_forExprM___spec__4___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ConstantInfo_value_x21___closed__3;
lean_object* l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__19;
lean_object* l_Lean_Declaration_foldExprM___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_instInhabitedInductiveVal;
lean_object* l_Lean_ConstantInfo_isCtor_match__1(lean_object*);
@ -211,7 +211,6 @@ lean_object* l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Le
lean_object* l_Lean_instInhabitedOpaqueVal___closed__1;
lean_object* l_Lean_InductiveVal_isReflexiveEx___boxed(lean_object*);
uint32_t lean_reducibility_hints_get_height(lean_object*);
lean_object* lean_nat_to_int(lean_object*);
lean_object* l_Lean_mkInductiveValEx___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_ConstantInfo_isUnsafe___boxed(lean_object*);
lean_object* l_Lean_ConstantInfo_type___boxed(lean_object*);
@ -814,17 +813,8 @@ return x_2;
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(2u);
x_2 = lean_nat_to_int(x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__3;
x_1 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
x_2 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__2;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -832,11 +822,11 @@ lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__5() {
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__4() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__4;
x_1 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__3;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
@ -844,7 +834,7 @@ lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__6() {
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -856,11 +846,11 @@ lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__7() {
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__6() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__6;
x_1 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__5;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
@ -868,7 +858,7 @@ lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__8() {
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__7() {
_start:
{
lean_object* x_1;
@ -876,57 +866,57 @@ x_1 = lean_mk_string("Lean.DefinitionSafety.safe");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__9() {
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__8;
x_1 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__7;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__10() {
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__3;
x_2 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__9;
x_1 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
x_2 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__8;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__10() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__9;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__11() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__10;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__12() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Int_Int_pow___closed__1;
x_2 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__9;
x_2 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__8;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__13() {
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__12() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__12;
x_1 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__11;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
@ -934,7 +924,7 @@ lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__14() {
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__13() {
_start:
{
lean_object* x_1;
@ -942,33 +932,33 @@ x_1 = lean_mk_string("Lean.DefinitionSafety.partial");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__15() {
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__14() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__14;
x_1 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__13;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__16() {
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__15() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__3;
x_2 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__15;
x_1 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
x_2 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__14;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__17() {
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__16() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__16;
x_1 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__15;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
@ -976,23 +966,23 @@ lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__18() {
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__17() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Int_Int_pow___closed__1;
x_2 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__15;
x_2 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__14;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__19() {
static lean_object* _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__18() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__18;
x_1 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__17;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
@ -1012,14 +1002,14 @@ x_4 = lean_nat_dec_le(x_3, x_2);
if (x_4 == 0)
{
lean_object* x_5; lean_object* x_6;
x_5 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__5;
x_5 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__4;
x_6 = l_Repr_addAppParen(x_5, x_2);
return x_6;
}
else
{
lean_object* x_7; lean_object* x_8;
x_7 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__7;
x_7 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__6;
x_8 = l_Repr_addAppParen(x_7, x_2);
return x_8;
}
@ -1032,14 +1022,14 @@ x_10 = lean_nat_dec_le(x_9, x_2);
if (x_10 == 0)
{
lean_object* x_11; lean_object* x_12;
x_11 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__11;
x_11 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__10;
x_12 = l_Repr_addAppParen(x_11, x_2);
return x_12;
}
else
{
lean_object* x_13; lean_object* x_14;
x_13 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__13;
x_13 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__12;
x_14 = l_Repr_addAppParen(x_13, x_2);
return x_14;
}
@ -1052,14 +1042,14 @@ x_16 = lean_nat_dec_le(x_15, x_2);
if (x_16 == 0)
{
lean_object* x_17; lean_object* x_18;
x_17 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__17;
x_17 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__16;
x_18 = l_Repr_addAppParen(x_17, x_2);
return x_18;
}
else
{
lean_object* x_19; lean_object* x_20;
x_19 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__19;
x_19 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__18;
x_20 = l_Repr_addAppParen(x_19, x_2);
return x_20;
}
@ -3570,8 +3560,6 @@ l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaratio
lean_mark_persistent(l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__17);
l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__18 = _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__18();
lean_mark_persistent(l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__18);
l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__19 = _init_l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__19();
lean_mark_persistent(l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__19);
l_Lean_instReprDefinitionSafety___closed__1 = _init_l_Lean_instReprDefinitionSafety___closed__1();
lean_mark_persistent(l_Lean_instReprDefinitionSafety___closed__1);
l_Lean_instReprDefinitionSafety = _init_l_Lean_instReprDefinitionSafety();

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

@ -91,7 +91,6 @@ lean_object* l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRanges____
lean_object* l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRanges____x40_Lean_DeclarationRange___hyg_296____closed__1;
lean_object* l_Array_qpartition_loop___at_Lean_initFn____x40_Lean_DeclarationRange___hyg_340____spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_qpartition_loop___at_Lean_initFn____x40_Lean_DeclarationRange___hyg_340____spec__3___closed__1;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__29;
lean_object* l_Lean_declRangeExt___closed__1;
size_t lean_usize_of_nat(lean_object*);
lean_object* l___private_Lean_DeclarationRange_0__Lean_decEqDeclarationRange____x40_Lean_DeclarationRange___hyg_20____boxed(lean_object*, lean_object*);
@ -99,7 +98,6 @@ lean_object* l_Lean_findDeclarationRanges_x3f___rarg___lambda__2(lean_object*, l
lean_object* l_Lean_SimplePersistentEnvExtension_getState___rarg(lean_object*, lean_object*);
lean_object* l_Lean_findDeclarationRangesCore_x3f(lean_object*);
lean_object* l_Array_binSearchAux___at_Lean_findDeclarationRangesCore_x3f___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__28;
lean_object* l_Lean_initFn____x40_Lean_DeclarationRange___hyg_340____closed__2;
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
lean_object* l_List_redLength___rarg(lean_object*);
@ -115,6 +113,7 @@ uint8_t lean_nat_dec_le(lean_object*, lean_object*);
lean_object* l_Std_RBNode_find___at_Lean_findDeclarationRangesCore_x3f___spec__2___boxed(lean_object*, lean_object*);
lean_object* l_Lean_instReprDeclarationRanges;
lean_object* l_Lean_declRangeExt___closed__5;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__29;
lean_object* l_Lean_declRangeExt___closed__3;
extern lean_object* l_Lean_registerSimplePersistentEnvExtension___rarg___closed__1;
extern lean_object* l_Lean_EnvExtensionInterfaceUnsafe_instInhabitedExt___closed__2;
@ -123,11 +122,11 @@ lean_object* l_Lean_isRec___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_initFn____x40_Lean_DeclarationRange___hyg_340____spec__5(lean_object*, lean_object*);
lean_object* l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRanges____x40_Lean_DeclarationRange___hyg_296____closed__4;
lean_object* l_Lean_instInhabitedDeclarationRanges;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__28;
lean_object* l_Lean_Name_getPrefix(lean_object*);
lean_object* l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRange____x40_Lean_DeclarationRange___hyg_205____closed__4;
lean_object* l_Array_qsort_sort___at_Lean_initFn____x40_Lean_DeclarationRange___hyg_340____spec__2___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_instInhabitedName;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__4;
lean_object* l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRanges____x40_Lean_DeclarationRange___hyg_296____closed__5;
lean_object* l_Lean_Environment_getModuleIdxFor_x3f(lean_object*, lean_object*);
lean_object* l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRange____x40_Lean_DeclarationRange___hyg_205____closed__1;
@ -142,12 +141,13 @@ extern lean_object* l_Lean_instInhabitedPosition___closed__1;
lean_object* l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRange____x40_Lean_DeclarationRange___hyg_205_(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Position_0__Lean_reprPosition____x40_Lean_Data_Position___hyg_117_(lean_object*, lean_object*);
lean_object* l_Lean_declRangeExt___elambda__2___boxed(lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__4;
lean_object* l_EStateM_pure___rarg(lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__27;
lean_object* l_Lean_findDeclarationRangesCore_x3f___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_instReprDeclarationRange___closed__1;
lean_object* l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRanges____x40_Lean_DeclarationRange___hyg_296____closed__6;
lean_object* l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRange____x40_Lean_DeclarationRange___hyg_205____boxed(lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__27;
lean_object* l___private_Lean_DeclarationRange_0__Lean_reprDeclarationRanges____x40_Lean_DeclarationRange___hyg_296____closed__2;
extern lean_object* l_Array_qsort_sort___at_Lean_mkMapDeclarationExtension___spec__1___rarg___closed__1;
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
@ -322,7 +322,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_205____closed__3;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__4;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____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);
@ -407,7 +407,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_6247____closed__4;
x_14 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____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);
@ -460,15 +460,15 @@ lean_ctor_set(x_35, 0, x_34);
x_36 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_36, 0, x_32);
lean_ctor_set(x_36, 1, x_35);
x_37 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__28;
x_37 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__28;
x_38 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_38, 0, x_37);
lean_ctor_set(x_38, 1, x_36);
x_39 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__29;
x_39 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__29;
x_40 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_40, 0, x_38);
lean_ctor_set(x_40, 1, x_39);
x_41 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__27;
x_41 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__27;
x_42 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_42, 0, x_41);
lean_ctor_set(x_42, 1, x_40);
@ -558,7 +558,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_296____closed__3;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__4;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____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);
@ -607,7 +607,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_6247____closed__4;
x_14 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____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);
@ -618,15 +618,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_6247____closed__28;
x_19 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__28;
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_6247____closed__29;
x_21 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__29;
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_6247____closed__27;
x_23 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__27;
x_24 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_24, 0, x_23);
lean_ctor_set(x_24, 1, x_22);

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

File diff suppressed because it is too large Load diff

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

@ -34,6 +34,7 @@ lean_object* l_Lean_Elab_resolveGlobalConstNoOverloadWithInfo___rarg___lambda__3
lean_object* l_Lean_Elab_TacticInfo_format(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_withInfoContext_x27___rarg___lambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Elab_resolveGlobalConstNoOverloadWithInfo___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_InfoTree_findInfo_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_TermInfo_format___lambda__1___closed__2;
lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
lean_object* l_Lean_Elab_ContextInfo_toPPContext___boxed(lean_object*, lean_object*);
@ -52,6 +53,7 @@ lean_object* l_Lean_Elab_InfoTree_format_match__1(lean_object*);
extern lean_object* l_Array_empty___closed__1;
lean_object* l_Lean_Meta_ppExpr(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_ContextInfo_runMetaM___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_InfoTree_findInfo_x3f_match__1(lean_object*);
lean_object* l_Lean_Elab_withInfoContext_x27_match__1(lean_object*);
lean_object* lean_st_ref_get(lean_object*, lean_object*);
lean_object* l_Lean_Elab_enableInfoTree(lean_object*);
@ -116,8 +118,11 @@ lean_object* l_List_forIn_loop___at_Lean_Elab_resolveGlobalConstWithInfos___spec
lean_object* l_Lean_Elab_enableInfoTree___rarg(lean_object*, uint8_t);
lean_object* l_Lean_Elab_TacticInfo_format___closed__2;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_findSomeM_x3f___at_Lean_Elab_InfoTree_findInfo_x3f___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Elab_InfoTree_findInfo_x3f(lean_object*, lean_object*);
lean_object* l_List_forIn_loop___at_Lean_Elab_resolveGlobalConstWithInfos___spec__1___rarg___lambda__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_MessageData_toString(lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_InfoTree_findInfo_x3f___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_getInfoHoleIdAssignment_x3f___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_PersistentHashMap_insertAux___rarg___closed__3;
lean_object* lean_nat_sub(lean_object*, lean_object*);
@ -168,6 +173,7 @@ lean_object* l_Lean_Core_getMaxHeartbeats(lean_object*);
lean_object* l_Lean_Elab_instInhabitedContextInfo___closed__1;
lean_object* l_Lean_Elab_ContextInfo_toPPContext(lean_object*, lean_object*);
lean_object* l_Lean_Elab_InfoState_assignment___default;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_InfoTree_findInfo_x3f___spec__5(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_Elab_TermInfo_format___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_instMonadInfoTree___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_withInfoContext_x27_match__2___rarg(lean_object*, lean_object*, lean_object*);
@ -193,6 +199,7 @@ lean_object* l_Lean_Meta_ppExpr___boxed(lean_object*, lean_object*, lean_object*
lean_object* l_Lean_Elab_resolveGlobalConstNoOverloadWithInfo(lean_object*);
lean_object* l_Lean_Elab_assignInfoHoleId___rarg___lambda__2___closed__5;
extern lean_object* l_Lean_Unhygienic_run___rarg___closed__2;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_InfoTree_findInfo_x3f___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_ContextInfo_ppGoals___boxed(lean_object*, lean_object*, lean_object*);
size_t l_USize_mul(size_t, size_t);
lean_object* l_Lean_Elab_ContextInfo_ppGoals___closed__2;
@ -215,6 +222,7 @@ lean_object* l_Std_fmt___at_Lean_Level_PP_Result_format___spec__1(lean_object*);
lean_object* l_Lean_Elab_withInfoContext___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_term_x2d_____closed__3;
lean_object* l_Lean_Elab_resolveGlobalConstWithInfos___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_InfoTree_findInfo_x3f___spec__3(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_InfoTree_substitute___spec__3(lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_Elab_assignInfoHoleId___rarg___lambda__2___closed__2;
lean_object* l_Lean_Syntax_getPos_x3f(lean_object*, uint8_t);
@ -238,15 +246,18 @@ lean_object* l_Lean_Elab_MacroExpansionInfo_format___boxed(lean_object*, lean_ob
lean_object* l_Std_PersistentArray_get_x21___at_Lean_Elab_withInfoHole___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_assignInfoHoleId___rarg___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_InfoTree_format___closed__1;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_InfoTree_findInfo_x3f___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_instInhabitedInfo___closed__1;
lean_object* l_Lean_Elab_CommandInfo_format(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_assignInfoHoleId(lean_object*);
lean_object* lean_panic_fn(lean_object*, lean_object*);
lean_object* l_Lean_Elab_MacroExpansionInfo_format___closed__1;
lean_object* l_Std_PersistentArray_findSomeM_x3f___at_Lean_Elab_InfoTree_findInfo_x3f___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_List_forIn_loop___at_Lean_Elab_resolveGlobalConstWithInfos___spec__1___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_CommandInfo_format___closed__2;
lean_object* l_Std_PersistentArray_mapMAux___at_Lean_Elab_InfoTree_substitute___spec__2(lean_object*, lean_object*);
extern lean_object* l_Lean_instInhabitedExpr___closed__1;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_InfoTree_findInfo_x3f___spec__4(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l_List_mapM___at_Lean_Elab_InfoTree_format___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_instInhabitedMacroExpansionInfo;
lean_object* l_Lean_Elab_ContextInfo_ppGoals___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -267,13 +278,13 @@ lean_object* l_Lean_Elab_instInhabitedContextInfo;
lean_object* l_Lean_Json_pretty(lean_object*, lean_object*);
lean_object* l_Lean_ppTerm(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_mkInfoNode___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__4;
lean_object* l_Lean_Elab_withInfoTreeContext___rarg(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_Lean_Elab_mkInfoNode___rarg___lambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Elab_withInfoContext_x27___rarg___lambda__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_enableInfoTree___rarg___lambda__1___boxed(lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_find_x3f___at_Lean_Elab_InfoTree_substitute___spec__6___boxed(lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_findSomeMAux___at_Lean_Elab_InfoTree_findInfo_x3f___spec__2(lean_object*, lean_object*);
lean_object* l_Lean_Elab_instInhabitedInfoState;
lean_object* l___private_Lean_Elab_InfoTree_0__Lean_Elab_getResetInfoTrees___rarg___lambda__1(lean_object*);
lean_object* l_Lean_Syntax_getTailInfo(lean_object*);
@ -316,6 +327,7 @@ lean_object* l_Lean_Elab_TacticInfo_format___closed__3;
extern lean_object* l___private_Init_Data_Format_Basic_0__Std_Format_pushNewline___closed__1;
lean_object* l_Lean_Elab_InfoState_trees___default;
lean_object* lean_usize_to_nat(size_t);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__4;
lean_object* l_Lean_resolveGlobalConstNoOverload___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_ContextInfo_runMetaM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Elab_InfoState_enabled___default;
@ -326,6 +338,7 @@ lean_object* l_Lean_Elab_withInfoTreeContext___rarg___lambda__3(lean_object*, le
lean_object* l_Lean_Elab_withInfoTreeContext___rarg___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_withInfoTreeContext___rarg___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_instInhabitedPUnit;
extern lean_object* l_Array_findSomeM_x3f___rarg___closed__1;
lean_object* l_Lean_Elab_InfoTree_format_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_instInhabitedFieldInfo;
lean_object* l_Std_Format_nestD(lean_object*);
@ -337,6 +350,7 @@ lean_object* l_Lean_Elab_instInhabitedInfoState___closed__1;
extern lean_object* l_Std_PersistentArray_getAux___rarg___closed__1;
lean_object* l_Lean_Elab_FieldInfo_format(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_withInfoHole___rarg___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_findSomeMAux___at_Lean_Elab_InfoTree_findInfo_x3f___spec__2___boxed(lean_object*, lean_object*);
static lean_object* _init_l_Lean_Elab_ContextInfo_mctx___default() {
_start:
{
@ -533,6 +547,506 @@ x_1 = l_Lean_Elab_instInhabitedInfoTree___closed__1;
return x_1;
}
}
lean_object* l_Lean_Elab_InfoTree_findInfo_x3f_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_dec(x_3);
lean_dec(x_2);
x_11 = lean_apply_1(x_4, x_1);
return x_11;
}
}
}
}
lean_object* l_Lean_Elab_InfoTree_findInfo_x3f_match__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Elab_InfoTree_findInfo_x3f_match__1___rarg), 4, 0);
return x_2;
}
}
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_InfoTree_findInfo_x3f___spec__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, size_t x_4, size_t x_5, lean_object* x_6) {
_start:
{
uint8_t x_7;
x_7 = x_5 < x_4;
if (x_7 == 0)
{
lean_dec(x_1);
lean_inc(x_6);
return x_6;
}
else
{
lean_object* x_8; lean_object* x_9;
x_8 = lean_array_uget(x_3, x_5);
lean_inc(x_1);
x_9 = l_Std_PersistentArray_findSomeMAux___at_Lean_Elab_InfoTree_findInfo_x3f___spec__2(x_1, x_8);
lean_dec(x_8);
if (lean_obj_tag(x_9) == 0)
{
size_t x_10; size_t x_11;
x_10 = 1;
x_11 = x_5 + x_10;
{
size_t _tmp_4 = x_11;
lean_object* _tmp_5 = x_2;
x_5 = _tmp_4;
x_6 = _tmp_5;
}
goto _start;
}
else
{
uint8_t x_13;
lean_dec(x_1);
x_13 = !lean_is_exclusive(x_9);
if (x_13 == 0)
{
lean_object* x_14; lean_object* x_15;
x_14 = lean_box(0);
x_15 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_15, 0, x_9);
lean_ctor_set(x_15, 1, x_14);
return x_15;
}
else
{
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_16 = lean_ctor_get(x_9, 0);
lean_inc(x_16);
lean_dec(x_9);
x_17 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_17, 0, x_16);
x_18 = lean_box(0);
x_19 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_19, 0, x_17);
lean_ctor_set(x_19, 1, x_18);
return x_19;
}
}
}
}
}
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_InfoTree_findInfo_x3f___spec__4(lean_object* x_1, lean_object* x_2, lean_object* x_3, size_t x_4, size_t x_5, lean_object* x_6) {
_start:
{
uint8_t x_7;
x_7 = x_5 < x_4;
if (x_7 == 0)
{
lean_dec(x_1);
lean_inc(x_6);
return x_6;
}
else
{
lean_object* x_8; lean_object* x_9;
x_8 = lean_array_uget(x_3, x_5);
lean_inc(x_1);
x_9 = l_Lean_Elab_InfoTree_findInfo_x3f(x_1, x_8);
if (lean_obj_tag(x_9) == 0)
{
size_t x_10; size_t x_11;
x_10 = 1;
x_11 = x_5 + x_10;
{
size_t _tmp_4 = x_11;
lean_object* _tmp_5 = x_2;
x_5 = _tmp_4;
x_6 = _tmp_5;
}
goto _start;
}
else
{
uint8_t x_13;
lean_dec(x_1);
x_13 = !lean_is_exclusive(x_9);
if (x_13 == 0)
{
lean_object* x_14; lean_object* x_15;
x_14 = lean_box(0);
x_15 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_15, 0, x_9);
lean_ctor_set(x_15, 1, x_14);
return x_15;
}
else
{
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_16 = lean_ctor_get(x_9, 0);
lean_inc(x_16);
lean_dec(x_9);
x_17 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_17, 0, x_16);
x_18 = lean_box(0);
x_19 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_19, 0, x_17);
lean_ctor_set(x_19, 1, x_18);
return x_19;
}
}
}
}
}
lean_object* l_Std_PersistentArray_findSomeMAux___at_Lean_Elab_InfoTree_findInfo_x3f___spec__2(lean_object* x_1, lean_object* x_2) {
_start:
{
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; size_t x_6; size_t x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_3 = lean_ctor_get(x_2, 0);
x_4 = lean_box(0);
x_5 = lean_array_get_size(x_3);
x_6 = lean_usize_of_nat(x_5);
lean_dec(x_5);
x_7 = 0;
x_8 = l_Array_findSomeM_x3f___rarg___closed__1;
x_9 = l_Array_forInUnsafe_loop___at_Lean_Elab_InfoTree_findInfo_x3f___spec__3(x_1, x_8, x_3, x_6, x_7, x_8);
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
lean_dec(x_9);
if (lean_obj_tag(x_10) == 0)
{
return x_4;
}
else
{
uint8_t x_11;
x_11 = !lean_is_exclusive(x_10);
if (x_11 == 0)
{
return x_10;
}
else
{
lean_object* x_12; lean_object* x_13;
x_12 = lean_ctor_get(x_10, 0);
lean_inc(x_12);
lean_dec(x_10);
x_13 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_13, 0, x_12);
return x_13;
}
}
}
else
{
lean_object* x_14; 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;
x_14 = lean_ctor_get(x_2, 0);
x_15 = lean_box(0);
x_16 = lean_array_get_size(x_14);
x_17 = lean_usize_of_nat(x_16);
lean_dec(x_16);
x_18 = 0;
x_19 = l_Array_findSomeM_x3f___rarg___closed__1;
x_20 = l_Array_forInUnsafe_loop___at_Lean_Elab_InfoTree_findInfo_x3f___spec__4(x_1, x_19, x_14, x_17, x_18, x_19);
x_21 = lean_ctor_get(x_20, 0);
lean_inc(x_21);
lean_dec(x_20);
if (lean_obj_tag(x_21) == 0)
{
return x_15;
}
else
{
uint8_t x_22;
x_22 = !lean_is_exclusive(x_21);
if (x_22 == 0)
{
return x_21;
}
else
{
lean_object* x_23; lean_object* x_24;
x_23 = lean_ctor_get(x_21, 0);
lean_inc(x_23);
lean_dec(x_21);
x_24 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_24, 0, x_23);
return x_24;
}
}
}
}
}
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_InfoTree_findInfo_x3f___spec__5(lean_object* x_1, lean_object* x_2, lean_object* x_3, size_t x_4, size_t x_5, lean_object* x_6) {
_start:
{
uint8_t x_7;
x_7 = x_5 < x_4;
if (x_7 == 0)
{
lean_dec(x_1);
lean_inc(x_6);
return x_6;
}
else
{
lean_object* x_8; lean_object* x_9;
x_8 = lean_array_uget(x_3, x_5);
lean_inc(x_1);
x_9 = l_Lean_Elab_InfoTree_findInfo_x3f(x_1, x_8);
if (lean_obj_tag(x_9) == 0)
{
size_t x_10; size_t x_11;
x_10 = 1;
x_11 = x_5 + x_10;
{
size_t _tmp_4 = x_11;
lean_object* _tmp_5 = x_2;
x_5 = _tmp_4;
x_6 = _tmp_5;
}
goto _start;
}
else
{
uint8_t x_13;
lean_dec(x_1);
x_13 = !lean_is_exclusive(x_9);
if (x_13 == 0)
{
lean_object* x_14; lean_object* x_15;
x_14 = lean_box(0);
x_15 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_15, 0, x_9);
lean_ctor_set(x_15, 1, x_14);
return x_15;
}
else
{
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_16 = lean_ctor_get(x_9, 0);
lean_inc(x_16);
lean_dec(x_9);
x_17 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_17, 0, x_16);
x_18 = lean_box(0);
x_19 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_19, 0, x_17);
lean_ctor_set(x_19, 1, x_18);
return x_19;
}
}
}
}
}
lean_object* l_Std_PersistentArray_findSomeM_x3f___at_Lean_Elab_InfoTree_findInfo_x3f___spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4;
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_1);
x_4 = l_Std_PersistentArray_findSomeMAux___at_Lean_Elab_InfoTree_findInfo_x3f___spec__2(x_1, x_3);
if (lean_obj_tag(x_4) == 0)
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; size_t x_8; size_t x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_5 = lean_ctor_get(x_2, 1);
x_6 = lean_box(0);
x_7 = lean_array_get_size(x_5);
x_8 = lean_usize_of_nat(x_7);
lean_dec(x_7);
x_9 = 0;
x_10 = l_Array_findSomeM_x3f___rarg___closed__1;
x_11 = l_Array_forInUnsafe_loop___at_Lean_Elab_InfoTree_findInfo_x3f___spec__5(x_1, x_10, x_5, x_8, x_9, x_10);
x_12 = lean_ctor_get(x_11, 0);
lean_inc(x_12);
lean_dec(x_11);
if (lean_obj_tag(x_12) == 0)
{
return x_6;
}
else
{
uint8_t x_13;
x_13 = !lean_is_exclusive(x_12);
if (x_13 == 0)
{
return x_12;
}
else
{
lean_object* x_14; lean_object* x_15;
x_14 = lean_ctor_get(x_12, 0);
lean_inc(x_14);
lean_dec(x_12);
x_15 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_15, 0, x_14);
return x_15;
}
}
}
else
{
uint8_t x_16;
lean_dec(x_1);
x_16 = !lean_is_exclusive(x_4);
if (x_16 == 0)
{
return x_4;
}
else
{
lean_object* x_17; lean_object* x_18;
x_17 = lean_ctor_get(x_4, 0);
lean_inc(x_17);
lean_dec(x_4);
x_18 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_18, 0, x_17);
return x_18;
}
}
}
}
lean_object* l_Lean_Elab_InfoTree_findInfo_x3f(lean_object* x_1, lean_object* x_2) {
_start:
{
switch (lean_obj_tag(x_2)) {
case 0:
{
lean_object* x_3;
x_3 = lean_ctor_get(x_2, 1);
lean_inc(x_3);
lean_dec(x_2);
x_2 = x_3;
goto _start;
}
case 1:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8;
x_5 = lean_ctor_get(x_2, 0);
lean_inc(x_5);
x_6 = lean_ctor_get(x_2, 1);
lean_inc(x_6);
lean_inc(x_1);
x_7 = lean_apply_1(x_1, x_5);
x_8 = lean_unbox(x_7);
lean_dec(x_7);
if (x_8 == 0)
{
lean_object* x_9;
lean_dec(x_2);
x_9 = l_Std_PersistentArray_findSomeM_x3f___at_Lean_Elab_InfoTree_findInfo_x3f___spec__1(x_1, x_6);
lean_dec(x_6);
return x_9;
}
else
{
lean_object* x_10;
lean_dec(x_6);
lean_dec(x_1);
x_10 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_10, 0, x_2);
return x_10;
}
}
default:
{
lean_object* x_11;
lean_dec(x_2);
lean_dec(x_1);
x_11 = lean_box(0);
return x_11;
}
}
}
}
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_InfoTree_findInfo_x3f___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) {
_start:
{
size_t x_7; size_t x_8; lean_object* x_9;
x_7 = lean_unbox_usize(x_4);
lean_dec(x_4);
x_8 = lean_unbox_usize(x_5);
lean_dec(x_5);
x_9 = l_Array_forInUnsafe_loop___at_Lean_Elab_InfoTree_findInfo_x3f___spec__3(x_1, x_2, x_3, x_7, x_8, x_6);
lean_dec(x_6);
lean_dec(x_3);
lean_dec(x_2);
return x_9;
}
}
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_InfoTree_findInfo_x3f___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) {
_start:
{
size_t x_7; size_t x_8; lean_object* x_9;
x_7 = lean_unbox_usize(x_4);
lean_dec(x_4);
x_8 = lean_unbox_usize(x_5);
lean_dec(x_5);
x_9 = l_Array_forInUnsafe_loop___at_Lean_Elab_InfoTree_findInfo_x3f___spec__4(x_1, x_2, x_3, x_7, x_8, x_6);
lean_dec(x_6);
lean_dec(x_3);
lean_dec(x_2);
return x_9;
}
}
lean_object* l_Std_PersistentArray_findSomeMAux___at_Lean_Elab_InfoTree_findInfo_x3f___spec__2___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Std_PersistentArray_findSomeMAux___at_Lean_Elab_InfoTree_findInfo_x3f___spec__2(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_InfoTree_findInfo_x3f___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) {
_start:
{
size_t x_7; size_t x_8; lean_object* x_9;
x_7 = lean_unbox_usize(x_4);
lean_dec(x_4);
x_8 = lean_unbox_usize(x_5);
lean_dec(x_5);
x_9 = l_Array_forInUnsafe_loop___at_Lean_Elab_InfoTree_findInfo_x3f___spec__5(x_1, x_2, x_3, x_7, x_8, x_6);
lean_dec(x_6);
lean_dec(x_3);
lean_dec(x_2);
return x_9;
}
}
lean_object* l_Std_PersistentArray_findSomeM_x3f___at_Lean_Elab_InfoTree_findInfo_x3f___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Std_PersistentArray_findSomeM_x3f___at_Lean_Elab_InfoTree_findInfo_x3f___spec__1(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
static uint8_t _init_l_Lean_Elab_InfoState_enabled___default() {
_start:
{
@ -2146,7 +2660,7 @@ lean_ctor_set(x_21, 1, x_20);
x_22 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_22, 0, x_21);
lean_ctor_set(x_22, 1, x_11);
x_23 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__4;
x_23 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__4;
x_24 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_24, 0, x_22);
lean_ctor_set(x_24, 1, x_23);
@ -2193,7 +2707,7 @@ lean_ctor_set(x_39, 1, x_38);
x_40 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_40, 0, x_39);
lean_ctor_set(x_40, 1, x_11);
x_41 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__4;
x_41 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__4;
x_42 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_42, 0, x_40);
lean_ctor_set(x_42, 1, x_41);
@ -5894,7 +6408,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_assignInfoHoleId___rarg___lambda__2___closed__3;
x_2 = l_Lean_Elab_assignInfoHoleId___rarg___lambda__2___closed__4;
x_3 = lean_unsigned_to_nat(241u);
x_3 = lean_unsigned_to_nat(251u);
x_4 = lean_unsigned_to_nat(2u);
x_5 = l_Lean_Elab_assignInfoHoleId___rarg___lambda__2___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

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

File diff suppressed because it is too large Load diff

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

@ -350,7 +350,6 @@ lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHead
lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___closed__29;
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__20___lambda__3___closed__1;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__20;
lean_object* l_Lean_Elab_Term_Quotation_myMacro____x40_Lean_Elab_Quotation___hyg_3759____closed__24;
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__20___lambda__3___closed__6;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_13856____closed__9;
@ -453,6 +452,7 @@ extern lean_object* l_Lean_Elab_autoBoundImplicitLocal___closed__1;
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__20(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, 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_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__22___closed__17;
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__20___closed__20;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__20;
lean_object* l_Lean_Syntax_getId(lean_object*);
lean_object* l_Lean_Elab_addMacroStack___at_Lean_Elab_Term_instAddErrorMessageContextTermElabM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_deduplicate___lambda__1___closed__6;
@ -20761,7 +20761,7 @@ lean_ctor_set(x_46, 0, x_20);
lean_ctor_set(x_46, 1, x_45);
lean_inc(x_2);
x_47 = lean_array_push(x_2, x_46);
x_48 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__20;
x_48 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__20;
lean_inc(x_1);
x_49 = lean_name_mk_string(x_1, x_48);
lean_inc(x_2);
@ -21114,7 +21114,7 @@ lean_ctor_set(x_194, 0, x_20);
lean_ctor_set(x_194, 1, x_193);
lean_inc(x_2);
x_195 = lean_array_push(x_2, x_194);
x_196 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__20;
x_196 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__20;
lean_inc(x_1);
x_197 = lean_name_mk_string(x_1, x_196);
lean_inc(x_2);

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

@ -542,7 +542,6 @@ lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_reduceProjOf_x3f___boxed(
lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_expandNonAtomicExplicitSource___closed__1;
lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_instInhabitedName;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__4;
lean_object* l_List_mapM___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_expandParentFields___spec__2___closed__4;
lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_addMissingFields___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_getStructName_throwUnknownExpectedType___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -632,6 +631,7 @@ lean_object* l_Lean_Elab_Term_StructInst_instToFormatFieldLHS_match__1(lean_obje
lean_object* l_List_foldl___at_Lean_Elab_Term_StructInst_DefaultFields_getHierarchyDepth___spec__1___boxed(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_groupFields_match__2___rarg(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Elab_Term_StructInst_DefaultFields_State_progress___default;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__4;
lean_object* l_Lean_Elab_Term_StructInst_throwFailedToElabField(lean_object*);
lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_expandNonAtomicExplicitSource___closed__4;
lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_mkFieldMap_match__2(lean_object*);
@ -5602,7 +5602,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_6247____closed__4;
x_6 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____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);

942
stage0/stdlib/Lean/Elab/Tactic/Basic.c generated
View file

File diff suppressed because it is too large Load diff

4
stage0/stdlib/Lean/Elab/Tactic/Match.c generated
View file

@ -128,6 +128,7 @@ lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMe
lean_object* l_Lean_Elab_Tactic_evalEraseAuxDiscrs___rarg___closed__1;
lean_object* l_Lean_Elab_Tactic_evalEraseAuxDiscrs___boxed(lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_evalEraseAuxDiscrs___spec__5(lean_object*, size_t, size_t, lean_object*);
extern lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_7183____closed__1;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_14458____closed__13;
uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_14458____closed__8;
@ -144,7 +145,6 @@ lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Tactic_evalMatch_
lean_object* lean_usize_to_nat(size_t);
lean_object* l_Std_PersistentArray_foldlM___at_Lean_Elab_Tactic_evalEraseAuxDiscrs___spec__2___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Tactic_Match_0__Lean_Elab_Tactic_mkAuxiliaryMatchTerm(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_7228____closed__1;
lean_object* l_Lean_Elab_Tactic_evalEraseAuxDiscrs___rarg___closed__2;
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalEraseAuxDiscrs(lean_object*);
lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlMAux___at_Lean_Elab_Tactic_evalEraseAuxDiscrs___spec__4___boxed(lean_object*, lean_object*);
@ -1378,7 +1378,7 @@ lean_dec(x_183);
x_222 = lean_ctor_get(x_6, 0);
lean_inc(x_222);
lean_dec(x_6);
x_223 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_7228____closed__1;
x_223 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_7183____closed__1;
x_224 = l_Lean_Name_appendIndexAfter(x_223, x_222);
x_225 = l_Lean_Name_append(x_1, x_224);
x_226 = l_Lean_mkIdentFrom(x_30, x_225);

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

@ -235,7 +235,6 @@ lean_object* l_Lean_SimplePersistentEnvExtension_modifyState___rarg___boxed(lean
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_Environment_hasUnsafe___lambda__1___boxed(lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Environment_displayStats___spec__8(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*);
extern lean_object* l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__3;
lean_object* l_Nat_foldAux___at_Lean_mkModuleData___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_anyMUnsafe_any___at_Lean_mkMapDeclarationExtension___spec__8___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_take(lean_object*, lean_object*);
@ -569,6 +568,7 @@ lean_object* lean_mk_array(lean_object*, lean_object*);
lean_object* l_Lean_EnvExtensionInterfaceImp___closed__7;
lean_object* l_Lean_instInhabitedPersistentEnvExtensionState(lean_object*, lean_object*);
extern size_t l_Std_PersistentHashMap_insertAux___rarg___closed__2;
extern lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
lean_object* l_Lean_Environment_getNamespaceSet___boxed(lean_object*);
lean_object* l_Lean_PersistentEnvExtension_getState___rarg(lean_object*, lean_object*);
lean_object* l_Array_qpartition_loop___at_Lean_mkMapDeclarationExtension___spec__3___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -12126,7 +12126,7 @@ x_23 = l_Std_Format_isNil(x_22);
if (x_23 == 0)
{
lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30;
x_24 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__3;
x_24 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
x_25 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_25, 0, x_24);
lean_ctor_set(x_25, 1, x_22);

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

@ -253,7 +253,6 @@ lean_object* l_Lean_Expr_hasLooseBVarInExplicitDomain_match__1(lean_object*);
lean_object* l_Lean_Expr_letName_x21___closed__3;
lean_object* l_Lean_Expr_updateLambda_x21(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__20;
lean_object* l_Lean_Expr_isProj_match__1(lean_object*);
lean_object* l_Lean_Expr_updateForall_x21___closed__2;
lean_object* l_Lean_Expr_updateLambdaE_x21___closed__2;
@ -337,6 +336,7 @@ lean_object* l_Lean_Expr_hasMVarEx___boxed(lean_object*);
lean_object* l_Lean_mkAppRange___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_fvarId_x21___boxed(lean_object*);
lean_object* l_Lean_Expr_setAppPPExplicitForExposingMVars(lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__20;
lean_object* l_Lean_Expr_fvarId_x21___closed__1;
lean_object* l_Lean_Expr_updateConst_x21___closed__2;
lean_object* lean_expr_mk_bvar(lean_object*);
@ -2936,7 +2936,7 @@ return x_12;
default:
{
lean_object* x_13;
x_13 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__20;
x_13 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__20;
return x_13;
}
}

12
stage0/stdlib/Lean/Message.c generated
View file

@ -135,7 +135,6 @@ uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_MessageData_instantiateMVars_visit___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1940____closed__11;
lean_object* l_Std_PersistentArray_foldlM___at_Lean_MessageLog_getInfoMessages___spec__1(lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__3;
lean_object* l_Lean_MessageData_toString(lean_object*, lean_object*);
lean_object* l_Lean_Message_caption___default;
lean_object* l_Lean_MessageData_isNil_match__1(lean_object*);
@ -318,6 +317,7 @@ lean_object* l_Lean_KernelException_toMessageData___closed__12;
lean_object* l_Lean_MessageData_instCoeStringMessageData___closed__1;
lean_object* l_Lean_MessageLog_msgs___default;
lean_object* l_Lean_KernelException_toMessageData___closed__13;
extern lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
lean_object* l_Lean_mkErrorStringWithPos_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MessageLog_forM(lean_object*);
@ -2175,7 +2175,7 @@ static lean_object* _init_l_Lean_MessageData_formatAux___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__3;
x_1 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
x_2 = lean_box(0);
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -2701,7 +2701,7 @@ if (x_142 == 0)
{
lean_object* x_143; lean_object* x_144; lean_object* x_145;
x_143 = lean_ctor_get(x_141, 0);
x_144 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__3;
x_144 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
x_145 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_145, 0, x_144);
lean_ctor_set(x_145, 1, x_143);
@ -2716,7 +2716,7 @@ x_147 = lean_ctor_get(x_141, 1);
lean_inc(x_147);
lean_inc(x_146);
lean_dec(x_141);
x_148 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__3;
x_148 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
x_149 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_149, 0, x_148);
lean_ctor_set(x_149, 1, x_146);
@ -3287,7 +3287,7 @@ if (x_292 == 0)
{
lean_object* x_293; lean_object* x_294; lean_object* x_295;
x_293 = lean_ctor_get(x_291, 0);
x_294 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__3;
x_294 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
x_295 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_295, 0, x_294);
lean_ctor_set(x_295, 1, x_293);
@ -3302,7 +3302,7 @@ x_297 = lean_ctor_get(x_291, 1);
lean_inc(x_297);
lean_inc(x_296);
lean_dec(x_291);
x_298 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__3;
x_298 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
x_299 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_299, 0, x_298);
lean_ctor_set(x_299, 1, x_296);

4
stage0/stdlib/Lean/Meta/AppBuilder.c generated
View file

@ -162,6 +162,7 @@ lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l_Lean_addTrace___at_Lean_Meta_isLevelDefEqAux___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkEqMP___closed__1;
lean_object* l_Lean_Meta_mkEqMP___closed__2;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__24;
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkAppMFinal(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Util_Trace_0__Lean_getResetTraces___at___private_Lean_Meta_LevelDefEq_0__Lean_Meta_processPostponedStep___spec__6___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkHEqTrans_match__1(lean_object*);
@ -210,7 +211,6 @@ lean_object* lean_array_to_list(lean_object*, lean_object*);
lean_object* l_Lean_Meta_throwAppTypeMismatch___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkDecideProof(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkEqOfHEq_match__1(lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__24;
uint8_t l_Lean_Expr_isAppOfArity(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_instInhabitedExpr;
lean_object* l_Lean_Meta_mkEqSymm___closed__5;
@ -11390,7 +11390,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_mkDecIsTrue___closed__2;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__24;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__24;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}

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

@ -344,6 +344,7 @@ lean_object* l_Lean_Meta_instantiateMVars(lean_object*, lean_object*, lean_objec
lean_object* l___private_Lean_MetavarContext_0__Lean_MetavarContext_DependsOn_dep_visit___at_Lean_Meta_ToHide_hasInaccessibleNameDep___spec__15___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_mk_array(lean_object*, lean_object*);
lean_object* l_Lean_Meta_ppGoal___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
lean_object* l_Array_anyMUnsafe_any___at_Lean_Meta_ToHide_hasVisibleDep___spec__14___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withPPInaccessibleNames(lean_object*);
uint8_t l_Array_anyMUnsafe_any___at_Lean_Meta_ToHide_hasVisibleDep___spec__27(lean_object*, lean_object*, size_t, size_t);
@ -369,7 +370,6 @@ lean_object* l___private_Lean_Meta_PPGoal_0__Lean_Meta_addLine(lean_object*);
uint8_t l_Std_PersistentArray_anyM___at_Lean_Meta_ToHide_hasInaccessibleNameDep___spec__24(lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withLocalContextImp___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MetavarContext_getDecl(lean_object*, lean_object*);
extern lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__3;
uint8_t l_Array_anyMUnsafe_any___at_Lean_Meta_ToHide_hasVisibleDep___spec__21(lean_object*, lean_object*, size_t, size_t);
lean_object* l_Std_PersistentArray_anyMAux___at_Lean_Meta_ToHide_hasVisibleDep___spec__25___boxed(lean_object*, lean_object*);
uint8_t l_Array_anyMUnsafe_any___at_Lean_Meta_ToHide_hasInaccessibleNameDep___spec__14(lean_object*, lean_object*, size_t, size_t);
@ -20805,7 +20805,7 @@ lean_inc(x_26);
lean_inc(x_26);
x_27 = lean_alloc_closure((void*)(l_Lean_Meta_ToHide_collect), 6, 1);
lean_closure_set(x_27, 0, x_26);
x_28 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__3;
x_28 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
x_29 = lean_box(x_19);
lean_inc(x_24);
x_30 = lean_alloc_closure((void*)(l_Lean_Meta_ppGoal___lambda__1___boxed), 11, 5);
@ -20874,7 +20874,7 @@ lean_inc(x_49);
lean_inc(x_49);
x_50 = lean_alloc_closure((void*)(l_Lean_Meta_ToHide_collect), 6, 1);
lean_closure_set(x_50, 0, x_49);
x_51 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__3;
x_51 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
x_52 = lean_box(x_42);
lean_inc(x_47);
x_53 = lean_alloc_closure((void*)(l_Lean_Meta_ppGoal___lambda__1___boxed), 11, 5);

32
stage0/stdlib/Lean/Meta/Tactic/ElimInfo.c generated
View file

@ -107,7 +107,6 @@ extern lean_object* l_Lean_instInhabitedExpr;
lean_object* l___private_Lean_Meta_Tactic_ElimInfo_0__Lean_Meta_reprElimAltInfo____x40_Lean_Meta_Tactic_ElimInfo___hyg_7_(lean_object*, lean_object*);
extern lean_object* l_Lean_KernelException_toMessageData___closed__15;
lean_object* l___private_Lean_Meta_Tactic_ElimInfo_0__Lean_Meta_reprElimAltInfo____x40_Lean_Meta_Tactic_ElimInfo___hyg_7____closed__5;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__29;
lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_getElimInfo___spec__6(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
lean_object* l___private_Lean_Meta_Tactic_ElimInfo_0__Lean_Meta_reprElimAltInfo____x40_Lean_Meta_Tactic_ElimInfo___hyg_7____closed__6;
@ -123,7 +122,6 @@ lean_object* l_Lean_Meta_withNewMCtxDepth___at_Lean_Meta_addImplicitTargets___sp
lean_object* l_Lean_Meta_addImplicitTargets_collect___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Array_anyMUnsafe_any___at_Lean_Meta_getElimInfo___spec__10(lean_object*, size_t, size_t);
lean_object* l_Lean_LocalDecl_type(lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__28;
lean_object* l_Array_anyMUnsafe_any___at_Lean_Meta_getElimInfo___spec__10___boxed(lean_object*, lean_object*, lean_object*);
uint8_t l_Array_contains___at_Lean_Meta_addImplicitTargets_collect___spec__1(lean_object*, lean_object*);
lean_object* l_Array_indexOfAux___at_Lean_Meta_getElimInfo___spec__3(lean_object*, lean_object*, lean_object*);
@ -136,6 +134,7 @@ lean_object* l_Lean_Meta_getLocalDecl(lean_object*, lean_object*, lean_object*,
uint8_t lean_expr_eqv(lean_object*, lean_object*);
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
lean_object* l_Lean_Meta_getElimInfo___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__29;
uint8_t l_Lean_BinderInfo_isExplicit(uint8_t);
lean_object* l_Std_Format_joinSep___at___private_Lean_Meta_Tactic_ElimInfo_0__Lean_Meta_reprElimInfo____x40_Lean_Meta_Tactic_ElimInfo___hyg_67____spec__2(lean_object*, lean_object*);
lean_object* l_Lean_Meta_instReprElimAltInfo;
@ -145,11 +144,11 @@ lean_object* l_Lean_Meta_getElimInfo_match__1___rarg(lean_object*, lean_object*,
lean_object* l_Lean_Meta_addImplicitTargets_collect___lambda__2___closed__2;
lean_object* l_Lean_Meta_getElimInfo___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getElimInfo_match__1___boxed(lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__28;
lean_object* l_Lean_Meta_getElimInfo___lambda__1___closed__1;
uint8_t l_Lean_Expr_isFVar(lean_object*);
lean_object* l_Lean_Meta_addImplicitTargets___lambda__1___boxed__const__1;
lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__4;
lean_object* l_Std_Range_forIn_loop___at_Lean_Meta_getElimInfo___spec__9___lambda__1___boxed(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_Lean_Meta_isExprDefEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -169,6 +168,8 @@ lean_object* l_Lean_Expr_getAppFn(lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_addImplicitTargets___spec__1(size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_instReprElimAltInfo___closed__1;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__4;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__27;
lean_object* l_Lean_indentExpr(lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_addImplicitTargets___spec__2(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_repr___at___private_Lean_Meta_Tactic_ElimInfo_0__Lean_Meta_reprElimInfo____x40_Lean_Meta_Tactic_ElimInfo___hyg_67____spec__1(lean_object*);
@ -177,7 +178,6 @@ extern lean_object* l_Array_instReprArray___rarg___closed__3;
lean_object* l_Lean_Meta_addImplicitTargets_collect(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_Meta_ElimInfo_targetsPos___default;
uint8_t l_Lean_Expr_isSort(lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__27;
lean_object* l_Lean_Meta_getElimInfo_match__2___rarg(lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
uint8_t l_Array_contains___at_Lean_Meta_getElimInfo___spec__7(lean_object*, lean_object*);
@ -217,7 +217,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_Tactic_ElimInfo_0__Lean_Meta_reprElimAltInfo____x40_Lean_Meta_Tactic_ElimInfo___hyg_7____closed__3;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__4;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____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);
@ -272,7 +272,7 @@ x_15 = l___private_Lean_Meta_Tactic_ElimInfo_0__Lean_Meta_reprElimAltInfo____x40
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_6247____closed__4;
x_17 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____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);
@ -285,15 +285,15 @@ lean_ctor_set(x_21, 0, x_20);
x_22 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_22, 0, x_18);
lean_ctor_set(x_22, 1, x_21);
x_23 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__28;
x_23 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__28;
x_24 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_24, 0, x_23);
lean_ctor_set(x_24, 1, x_22);
x_25 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__29;
x_25 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__29;
x_26 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_26, 0, x_24);
lean_ctor_set(x_26, 1, x_25);
x_27 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__27;
x_27 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__27;
x_28 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_28, 0, x_27);
lean_ctor_set(x_28, 1, x_26);
@ -540,7 +540,7 @@ x_15 = l___private_Lean_Meta_Tactic_ElimInfo_0__Lean_Meta_reprElimInfo____x40_Le
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_6247____closed__4;
x_17 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____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);
@ -654,15 +654,15 @@ lean_ctor_set_uint8(x_52, sizeof(void*)*1, x_51);
x_53 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_53, 0, x_41);
lean_ctor_set(x_53, 1, x_52);
x_54 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__28;
x_54 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__28;
x_55 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_55, 0, x_54);
lean_ctor_set(x_55, 1, x_53);
x_56 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__29;
x_56 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__29;
x_57 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_57, 0, x_55);
lean_ctor_set(x_57, 1, x_56);
x_58 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__27;
x_58 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__27;
x_59 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_59, 0, x_58);
lean_ctor_set(x_59, 1, x_57);
@ -680,15 +680,15 @@ x_62 = l_Array_instReprArray___rarg___closed__5;
x_63 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_63, 0, x_41);
lean_ctor_set(x_63, 1, x_62);
x_64 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__28;
x_64 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__28;
x_65 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_65, 0, x_64);
lean_ctor_set(x_65, 1, x_63);
x_66 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__29;
x_66 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__29;
x_67 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_67, 0, x_65);
lean_ctor_set(x_67, 1, x_66);
x_68 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__27;
x_68 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__27;
x_69 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_69, 0, x_68);
lean_ctor_set(x_69, 1, x_67);

38
stage0/stdlib/Lean/Meta/Tactic/Simp/CongrLemmas.c generated
View file

@ -219,7 +219,6 @@ lean_object* l_Lean_Expr_withAppAux___at_Lean_Meta_mkCongrLemma___spec__12(lean_
extern lean_object* l_instReprList___rarg___closed__2;
lean_object* l_Std_PersistentHashMap_foldlMAux___at___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemmas____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_117____spec__13___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_withAppAux___at_Lean_Meta_mkCongrLemma___spec__11___lambda__1___closed__1;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__29;
lean_object* l_Lean_Meta_mkCongrLemma_match__3(lean_object*);
lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_249____closed__4;
lean_object* l_Lean_SMap_fold___at___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemmas____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_117____spec__2___rarg(lean_object*, lean_object*, lean_object*);
@ -234,7 +233,6 @@ lean_object* l_Std_HashMapImp_find_x3f___at_Lean_Meta_CongrLemmas_get___spec__5_
lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkCongrLemma___spec__4(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_CongrLemmas_lemmas___default;
lean_object* l_Std_Format_joinSep___at___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemma____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_21____spec__2(lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__28;
lean_object* l_Std_PersistentHashMap_insertAux_traverse___at_Lean_Meta_addCongrLemmaEntry___spec__4(size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Expr_FindImpl_initCache;
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemmas____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_117____spec__14___rarg(lean_object*, lean_object*, size_t, size_t, lean_object*);
@ -255,6 +253,7 @@ uint8_t lean_nat_dec_le(lean_object*, lean_object*);
uint8_t l_USize_decLe(size_t, size_t);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkCongrLemma___spec__8___lambda__3___closed__2;
lean_object* l_Lean_Meta_addCongrLemma___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__29;
lean_object* l___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemma____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_21____closed__2;
uint8_t l_Lean_BinderInfo_isExplicit(uint8_t);
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemmas____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_117____spec__14___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -269,6 +268,7 @@ lean_object* l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addCongrLemma___spec__
lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_1457____lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getCongrLemmas(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_1457____closed__3;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__28;
lean_object* l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addCongrLemma___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_instInhabitedPersistentEnvExtension___closed__5;
lean_object* l___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemmas____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_117_(lean_object*, lean_object*);
@ -284,7 +284,6 @@ lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_1
lean_object* l_Std_HashMapImp_insert___at_Lean_Meta_addCongrLemmaEntry___spec__6(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_isFVar(lean_object*);
lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__4;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_7613____closed__4;
lean_object* l_Std_PersistentHashMap_foldlMAux___at___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemmas____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_117____spec__5___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemma____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_21____closed__4;
@ -330,7 +329,9 @@ lean_object* l_List_map___at_Lean_mkConstWithLevelParams___spec__1(lean_object*)
lean_object* l_Std_HashMapImp_moveEntries___at_Lean_Meta_addCongrLemmaEntry___spec__9(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_foldlM___at___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemmas____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_117____spec__12___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_usize_to_nat(size_t);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__4;
lean_object* l___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemmas____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_117____closed__8;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__27;
lean_object* l_Lean_indentExpr(lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkCongrLemma___spec__8___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* l_Array_forInUnsafe_loop___at_Lean_Meta_mkCongrLemma___spec__8___lambda__5___closed__1;
@ -354,7 +355,6 @@ uint8_t l_Lean_Expr_isSort(lean_object*);
lean_object* l_Std_PersistentHashMap_foldlM___at___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemmas____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_117____spec__4___rarg___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_Format_paren___closed__3;
lean_object* l_Lean_ScopedEnvExtension_getState___at_Lean_Meta_getCongrLemmas___spec__1___boxed(lean_object*, lean_object*);
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__27;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkCongrLemma___spec__5___closed__6;
lean_object* l_Lean_Expr_withAppAux___at_Lean_Meta_mkCongrLemma___spec__11___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_mkCollisionNode___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -477,7 +477,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemma____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_21____closed__3;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__4;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____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);
@ -568,7 +568,7 @@ x_15 = l___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemma
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_6247____closed__4;
x_17 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____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);
@ -649,15 +649,15 @@ lean_ctor_set(x_52, 1, x_17);
x_53 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_53, 0, x_52);
lean_ctor_set(x_53, 1, x_35);
x_54 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__28;
x_54 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__28;
x_55 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_55, 0, x_54);
lean_ctor_set(x_55, 1, x_53);
x_56 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__29;
x_56 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__29;
x_57 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_57, 0, x_55);
lean_ctor_set(x_57, 1, x_56);
x_58 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__27;
x_58 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__27;
x_59 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_59, 0, x_58);
lean_ctor_set(x_59, 1, x_57);
@ -691,15 +691,15 @@ lean_ctor_set(x_68, 1, x_17);
x_69 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_69, 0, x_68);
lean_ctor_set(x_69, 1, x_35);
x_70 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__28;
x_70 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__28;
x_71 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_71, 0, x_70);
lean_ctor_set(x_71, 1, x_69);
x_72 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__29;
x_72 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__29;
x_73 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_73, 0, x_71);
lean_ctor_set(x_73, 1, x_72);
x_74 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__27;
x_74 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__27;
x_75 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_75, 0, x_74);
lean_ctor_set(x_75, 1, x_73);
@ -1633,7 +1633,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemmas____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_117____closed__3;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__4;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____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);
@ -1666,7 +1666,7 @@ static lean_object* _init_l___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__28;
x_1 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__28;
x_2 = l___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemmas____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_117____closed__6;
x_3 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -1679,7 +1679,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemmas____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_117____closed__7;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__29;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__29;
x_3 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -1690,7 +1690,7 @@ static lean_object* _init_l___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__27;
x_1 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__27;
x_2 = l___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemmas____x40_Lean_Meta_Tactic_Simp_CongrLemmas___hyg_117____closed__8;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -1752,15 +1752,15 @@ x_19 = l___private_Lean_Meta_Tactic_Simp_CongrLemmas_0__Lean_Meta_reprCongrLemma
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_6247____closed__28;
x_21 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__28;
x_22 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_22, 0, x_21);
lean_ctor_set(x_22, 1, x_20);
x_23 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__29;
x_23 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__29;
x_24 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_24, 0, x_22);
lean_ctor_set(x_24, 1, x_23);
x_25 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__27;
x_25 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__27;
x_26 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_26, 0, x_25);
lean_ctor_set(x_26, 1, x_24);

150
stage0/stdlib/Lean/Meta/TransparencyMode.c generated
View file

@ -48,10 +48,10 @@ lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparenc
lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__6;
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_beqTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_11__match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__25;
lean_object* l_Lean_Meta_TransparencyMode_lt_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Meta_TransparencyMode_lt(uint8_t, uint8_t);
lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__15;
extern lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59__match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__18;
lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__22;
@ -62,7 +62,6 @@ lean_object* l_Lean_Meta_TransparencyMode_hash___boxed(lean_object*);
lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__3;
lean_object* l_Lean_Meta_instBEqTransparencyMode;
lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__7;
lean_object* lean_nat_to_int(lean_object*);
lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__24;
lean_object* l_Lean_Meta_TransparencyMode_lt_match__1___rarg(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Repr_addAppParen(lean_object*, lean_object*);
@ -399,17 +398,8 @@ return x_2;
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(2u);
x_2 = lean_nat_to_int(x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__3;
x_1 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
x_2 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__2;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -417,11 +407,11 @@ lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__5() {
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__4() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__4;
x_1 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__3;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
@ -429,7 +419,7 @@ lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__6() {
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -441,11 +431,11 @@ lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__7() {
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__6() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__6;
x_1 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__5;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
@ -453,7 +443,7 @@ lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__8() {
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__7() {
_start:
{
lean_object* x_1;
@ -461,57 +451,57 @@ x_1 = lean_mk_string("Lean.Meta.TransparencyMode.default");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__9() {
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__8;
x_1 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__7;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__10() {
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__3;
x_2 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__9;
x_1 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
x_2 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__8;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__10() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__9;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__11() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__10;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__12() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Int_Int_pow___closed__1;
x_2 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__9;
x_2 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__8;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__13() {
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__12() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__12;
x_1 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__11;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
@ -519,7 +509,7 @@ lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__14() {
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__13() {
_start:
{
lean_object* x_1;
@ -527,57 +517,57 @@ x_1 = lean_mk_string("Lean.Meta.TransparencyMode.reducible");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__15() {
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__14() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__14;
x_1 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__13;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__16() {
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__15() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__3;
x_2 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__15;
x_1 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
x_2 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__14;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__16() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__15;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__17() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__16;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__18() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Int_Int_pow___closed__1;
x_2 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__15;
x_2 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__14;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__19() {
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__18() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__18;
x_1 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__17;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
@ -585,7 +575,7 @@ lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__20() {
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__19() {
_start:
{
lean_object* x_1;
@ -593,33 +583,33 @@ x_1 = lean_mk_string("Lean.Meta.TransparencyMode.instances");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__21() {
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__20() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__20;
x_1 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__19;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__22() {
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__21() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__3;
x_2 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__21;
x_1 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
x_2 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__20;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__23() {
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__22() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__22;
x_1 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__21;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
@ -627,23 +617,23 @@ lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__24() {
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__23() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Int_Int_pow___closed__1;
x_2 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__21;
x_2 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__20;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__25() {
static lean_object* _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__24() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__24;
x_1 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__23;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
@ -663,14 +653,14 @@ x_4 = lean_nat_dec_le(x_3, x_2);
if (x_4 == 0)
{
lean_object* x_5; lean_object* x_6;
x_5 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__5;
x_5 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__4;
x_6 = l_Repr_addAppParen(x_5, x_2);
return x_6;
}
else
{
lean_object* x_7; lean_object* x_8;
x_7 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__7;
x_7 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__6;
x_8 = l_Repr_addAppParen(x_7, x_2);
return x_8;
}
@ -683,14 +673,14 @@ x_10 = lean_nat_dec_le(x_9, x_2);
if (x_10 == 0)
{
lean_object* x_11; lean_object* x_12;
x_11 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__11;
x_11 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__10;
x_12 = l_Repr_addAppParen(x_11, x_2);
return x_12;
}
else
{
lean_object* x_13; lean_object* x_14;
x_13 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__13;
x_13 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__12;
x_14 = l_Repr_addAppParen(x_13, x_2);
return x_14;
}
@ -703,14 +693,14 @@ x_16 = lean_nat_dec_le(x_15, x_2);
if (x_16 == 0)
{
lean_object* x_17; lean_object* x_18;
x_17 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__17;
x_17 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__16;
x_18 = l_Repr_addAppParen(x_17, x_2);
return x_18;
}
else
{
lean_object* x_19; lean_object* x_20;
x_19 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__19;
x_19 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__18;
x_20 = l_Repr_addAppParen(x_19, x_2);
return x_20;
}
@ -723,14 +713,14 @@ x_22 = lean_nat_dec_le(x_21, x_2);
if (x_22 == 0)
{
lean_object* x_23; lean_object* x_24;
x_23 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__23;
x_23 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__22;
x_24 = l_Repr_addAppParen(x_23, x_2);
return x_24;
}
else
{
lean_object* x_25; lean_object* x_26;
x_25 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__25;
x_25 = l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__24;
x_26 = l_Repr_addAppParen(x_25, x_2);
return x_26;
}
@ -1149,8 +1139,6 @@ l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_
lean_mark_persistent(l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__23);
l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__24 = _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__24();
lean_mark_persistent(l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__24);
l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__25 = _init_l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__25();
lean_mark_persistent(l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__25);
l_Lean_Meta_instReprTransparencyMode___closed__1 = _init_l_Lean_Meta_instReprTransparencyMode___closed__1();
lean_mark_persistent(l_Lean_Meta_instReprTransparencyMode___closed__1);
l_Lean_Meta_instReprTransparencyMode = _init_l_Lean_Meta_instReprTransparencyMode();

12
stage0/stdlib/Lean/Parser/Tactic.c generated
View file

@ -146,6 +146,7 @@ lean_object* l_Lean_Parser_Tactic_eraseAuxDiscrs___elambda__1___closed__3;
lean_object* l___regBuiltin_Lean_Parser_Tactic_decide_parenthesizer___closed__1;
lean_object* l_Lean_Parser_nonReservedSymbolInfo(lean_object*, uint8_t);
lean_object* l_Lean_Parser_Tactic_nativeDecide___closed__2;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__24;
lean_object* l_Lean_Parser_Tactic_nativeDecide_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Tactic_introMatch___elambda__1___closed__5;
lean_object* l_Lean_Parser_Tactic_match___elambda__1___closed__2;
@ -180,7 +181,6 @@ lean_object* l_Lean_Parser_Tactic_match___elambda__1___closed__5;
lean_object* l___regBuiltin_Lean_Parser_Tactic_unknown_formatter___closed__1;
lean_object* l_Lean_Parser_Tactic_match_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Tactic_eraseAuxDiscrs_parenthesizer___closed__2;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__24;
extern lean_object* l_Lean_PrettyPrinter_formatterAttribute;
lean_object* l_Lean_Parser_Tactic_match___closed__8;
lean_object* l_Lean_Parser_Tactic_match_parenthesizer___closed__1;
@ -2573,7 +2573,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_intro___closed__2;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__24;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__24;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -2592,7 +2592,7 @@ static lean_object* _init_l_Lean_Parser_Tactic_decide___elambda__1___closed__3()
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4;
x_1 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__24;
x_1 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__24;
x_2 = l_Lean_Parser_Tactic_decide___elambda__1___closed__2;
x_3 = 1;
x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
@ -2603,7 +2603,7 @@ static lean_object* _init_l_Lean_Parser_Tactic_decide___elambda__1___closed__4()
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__24;
x_1 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__24;
x_2 = l_String_trim(x_1);
return x_2;
}
@ -2774,7 +2774,7 @@ static lean_object* _init_l_Lean_Parser_Tactic_decide_formatter___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__24;
x_1 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__24;
x_2 = l_Lean_Parser_Tactic_decide___elambda__1___closed__2;
x_3 = 1;
x_4 = lean_box(x_3);
@ -2789,7 +2789,7 @@ static lean_object* _init_l_Lean_Parser_Tactic_decide_formatter___closed__2() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__24;
x_1 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__24;
x_2 = 0;
x_3 = lean_box(x_2);
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_nonReservedSymbol_formatter___boxed), 7, 2);

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

@ -1395,7 +1395,6 @@ lean_object* l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__1;
lean_object* l_Lean_Parser_Level_quot___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_dbgTrace;
lean_object* l_Lean_Parser_Term_dynamicQuot_formatter___closed__5;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__20;
lean_object* l_Lean_Parser_Term_match_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Term_emptyC___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_type___elambda__1___closed__15;
@ -1981,6 +1980,7 @@ lean_object* l_Lean_Parser_Term_typeSpec_formatter___closed__1;
lean_object* l_Lean_Parser_Term_nomatch___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_explicitBinder___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_haveDecl_parenthesizer___closed__9;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__20;
lean_object* l_Lean_Parser_Term_have___elambda__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_stateRefT___elambda__1(lean_object*, lean_object*);
lean_object* l___regBuiltinParser_Lean_Parser_Term_type(lean_object*);
@ -40638,7 +40638,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_myMacro____x40_Init_Notation___hyg_2278____closed__2;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__20;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__20;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}

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

@ -128,7 +128,6 @@ lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l_Lean_pp_notation;
lean_object* l_Lean_PrettyPrinter_Delaborator_withBindingDomain___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_pp_all;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6247____closed__20;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
extern lean_object* l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___lambda__2___closed__4;
lean_object* l_Lean_PrettyPrinter_Delaborator_annotateCurPos(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -171,6 +170,7 @@ lean_object* l_Lean_PrettyPrinter_Delaborator_liftMetaM___rarg___boxed(lean_obje
uint8_t l_Lean_PrettyPrinter_Delaborator_getUnusedName_bodyUsesSuggestion(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_mkDelabAttribute(lean_object*);
extern lean_object* l_Lean_Elab_autoBoundImplicitLocal___closed__1;
extern lean_object* l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__20;
lean_object* l_Lean_PrettyPrinter_Delaborator_delab___closed__2;
lean_object* l_Lean_PrettyPrinter_Delaborator_instOrElseDelabM___closed__1;
lean_object* l_Lean_PrettyPrinter_Delaborator_instAlternativeDelabM___closed__2;
@ -2918,7 +2918,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_6247____closed__20;
x_2 = l___private_Init_Meta_0__Lean_Meta_Simp_reprConfig____x40_Init_Meta___hyg_6282____closed__20;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}

8
stage0/stdlib/Lean/ReducibilityAttrs.c generated
View file

@ -69,7 +69,6 @@ lean_object* l___private_Lean_ReducibilityAttrs_0__Lean_reprReducibilityStatus__
lean_object* l_Lean_initFn____x40_Lean_ReducibilityAttrs___hyg_88____closed__6;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
uint8_t l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_117_(uint8_t, uint8_t);
extern lean_object* l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__3;
lean_object* l_List_map___at_Lean_initFn____x40_Lean_ReducibilityAttrs___hyg_88____spec__7___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* lean_array_swap(lean_object*, lean_object*, lean_object*);
@ -145,6 +144,7 @@ lean_object* l_List_map___at_Lean_initFn____x40_Lean_ReducibilityAttrs___hyg_88_
lean_object* l_Lean_initFn____x40_Lean_ReducibilityAttrs___hyg_88____closed__3;
lean_object* l_Lean_initFn____x40_Lean_ReducibilityAttrs___hyg_88____closed__5;
lean_object* l_Lean_getReducibilityStatusImp_match__1___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
lean_object* l_Lean_PersistentEnvExtension_getState___rarg(lean_object*, lean_object*);
lean_object* l_Lean_instReprReducibilityStatus;
lean_object* l_Lean_registerEnumAttributes___at_Lean_initFn____x40_Lean_ReducibilityAttrs___hyg_88____spec__1(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
@ -251,7 +251,7 @@ static lean_object* _init_l___private_Lean_ReducibilityAttrs_0__Lean_reprReducib
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__3;
x_1 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
x_2 = l___private_Lean_ReducibilityAttrs_0__Lean_reprReducibilityStatus____x40_Lean_ReducibilityAttrs___hyg_11____closed__2;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -317,7 +317,7 @@ static lean_object* _init_l___private_Lean_ReducibilityAttrs_0__Lean_reprReducib
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__3;
x_1 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
x_2 = l___private_Lean_ReducibilityAttrs_0__Lean_reprReducibilityStatus____x40_Lean_ReducibilityAttrs___hyg_11____closed__8;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -383,7 +383,7 @@ static lean_object* _init_l___private_Lean_ReducibilityAttrs_0__Lean_reprReducib
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Declaration_0__Lean_reprDefinitionSafety____x40_Lean_Declaration___hyg_197____closed__3;
x_1 = l___private_Init_Data_Repr_0__reprSourceInfo____x40_Init_Data_Repr___hyg_1348____closed__4;
x_2 = l___private_Lean_ReducibilityAttrs_0__Lean_reprReducibilityStatus____x40_Lean_ReducibilityAttrs___hyg_11____closed__14;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);

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

File diff suppressed because it is too large Load diff

1455
stage0/stdlib/Lean/Server/InfoUtils.c generated
View file

File diff suppressed because it is too large Load diff