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-09-02 17:30:50 -07:00
parent d7537f252a
commit 120b0200c2
33 changed files with 11191 additions and 9912 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
stage0/src/Init/Conv.lean generated
View file

@ -16,17 +16,28 @@ syntax convSeq1Indented := withPosition((group(colGe conv ";"?))+)
syntax convSeqBracketed := "{" (group(conv ";"?))+ "}"
syntax convSeq := convSeq1Indented <|> convSeqBracketed
syntax (name := conv) "conv " (" at " ident)? (" in " term)? " => " convSeq : tactic
syntax (name := skip) "skip " : conv
syntax (name := lhs) "lhs" : conv
syntax (name := rhs) "rhs" : conv
syntax (name := whnf) "whnf" : conv
syntax (name := congr) "congr" : conv
syntax (name := arg) "arg " num : conv
syntax (name := trace) "trace" : conv
syntax (name := funext) "funext" ident* : conv
syntax (name := change) "change " term : conv
syntax (name := rewrite) "rewrite " rwRuleSeq : conv
syntax (name := simp) "simp " ("(" &"config" " := " term ")")? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? : conv
syntax (name := nestedTactic) "tactic " tacticSeq : conv
syntax (name := nestedConv) convSeqBracketed : conv
syntax (name := paren) "(" convSeq ")" : conv
/-- `· conv` focuses on the main conv goal and tries to solve it using `s` -/
macro dot:("·" <|> ".") s:convSeq : conv => `({%$dot ($s:convSeq) })
syntax (name := conv) "conv " (" at " ident)? (" in " term)? " => " convSeq : tactic
macro "rw " s:rwRuleSeq : conv => `(rewrite $s:rwRuleSeq)
macro "args" : conv => `(congr)
macro "left" : conv => `(lhs)
macro "right" : conv => `(rhs)
end Lean.Parser.Tactic.Conv

10
stage0/src/Init/Data/Nat/Div.lean generated
View file

@ -16,12 +16,12 @@ private def div.F (x : Nat) (f : ∀ x₁, x₁ < x → Nat → Nat) (y : Nat) :
@[extern "lean_nat_div"]
protected def div (a b : @& Nat) : Nat :=
WellFounded.fix ltWf div.F a b
WellFounded.fix lt_wf div.F a b
instance : Div Nat := ⟨Nat.div⟩
private theorem div_eq_aux (x y : Nat) : x / y = if h : 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0 :=
congrFun (WellFounded.fix_eq ltWf div.F x) y
congrFun (WellFounded.fix_eq lt_wf div.F x) y
theorem div_eq (x y : Nat) : x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0 :=
dif_eq_if (0 < y ∧ y ≤ x) ((x - y) / y + 1) 0 ▸ div_eq_aux x y
@ -39,19 +39,19 @@ theorem div.inductionOn.{u}
(ind : ∀ x y, 0 < y ∧ y ≤ x → motive (x - y) y → motive x y)
(base : ∀ x y, ¬(0 < y ∧ y ≤ x) → motive x y)
: motive x y :=
WellFounded.fix Nat.ltWf (div.induction.F motive ind base) x y
WellFounded.fix Nat.lt_wf (div.induction.F motive ind base) x y
private def mod.F (x : Nat) (f : ∀ x₁, x₁ < x → Nat → Nat) (y : Nat) : Nat :=
if h : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma h) y else x
@[extern "lean_nat_mod"]
protected def mod (a b : @& Nat) : Nat :=
WellFounded.fix ltWf mod.F a b
WellFounded.fix lt_wf mod.F a b
instance : Mod Nat := ⟨Nat.mod⟩
private theorem mod_eq_aux (x y : Nat) : x % y = if h : 0 < y ∧ y ≤ x then (x - y) % y else x :=
congrFun (WellFounded.fix_eq ltWf mod.F x) y
congrFun (WellFounded.fix_eq lt_wf mod.F x) y
theorem mod_eq (x y : Nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x :=
dif_eq_if (0 < y ∧ y ≤ x) ((x - y) % y) x ▸ mod_eq_aux x y

2
stage0/src/Init/Data/Nat/Gcd.lean generated
View file

@ -15,7 +15,7 @@ private def gcdF (x : Nat) : (∀ x₁, x₁ < x → Nat → Nat) → Nat → Na
@[extern "lean_nat_gcd"]
def gcd (a b : @& Nat) : Nat :=
WellFounded.fix ltWf gcdF a b
WellFounded.fix lt_wf gcdF a b
@[simp] theorem gcd_zero_left (y : Nat) : gcd 0 y = y :=
rfl

4
stage0/src/Init/WF.lean generated
View file

@ -144,7 +144,7 @@ def wf (h : WellFounded r) : WellFounded (TC r) :=
end TC
-- less-than is well-founded
def Nat.ltWf : WellFounded Nat.lt := by
def Nat.lt_wf : WellFounded Nat.lt := by
apply WellFounded.intro
intro n
induction n with
@ -164,7 +164,7 @@ def measure {α : Sort u} : (α → Nat) → α → α → Prop :=
InvImage (fun a b => a < b)
def measureWf {α : Sort u} (f : α → Nat) : WellFounded (measure f) :=
InvImage.wf f Nat.ltWf
InvImage.wf f Nat.lt_wf
def sizeofMeasure (α : Sort u) [SizeOf α] : α → α → Prop :=
measure sizeOf

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

@ -78,7 +78,6 @@ structure TacticInfo extends ElabInfo where
goalsBefore : List MVarId
mctxAfter : MetavarContext
goalsAfter : List MVarId
inConv : Bool
deriving Inhabited
structure MacroExpansionInfo where
@ -189,17 +188,17 @@ def FieldInfo.format (ctx : ContextInfo) (info : FieldInfo) : IO Format := do
ctx.runMetaM info.lctx do
return f!"{info.fieldName} : {← Meta.ppExpr (← Meta.inferType info.val)} := {← Meta.ppExpr info.val} @ {formatStxRange ctx info.stx}"
def ContextInfo.ppGoals (ctx : ContextInfo) (goals : List MVarId) (inConv : Bool) : IO Format :=
def ContextInfo.ppGoals (ctx : ContextInfo) (goals : List MVarId) : IO Format :=
if goals.isEmpty then
return "no goals"
else
ctx.runMetaM {} (return Std.Format.prefixJoin "\n" (← goals.mapM (Meta.ppGoal . inConv)))
ctx.runMetaM {} (return Std.Format.prefixJoin "\n" (← goals.mapM (Meta.ppGoal .)))
def TacticInfo.format (ctx : ContextInfo) (info : TacticInfo) : IO Format := do
let ctxB := { ctx with mctx := info.mctxBefore }
let ctxA := { ctx with mctx := info.mctxAfter }
let goalsBefore ← ctxB.ppGoals info.goalsBefore info.inConv
let goalsAfter ← ctxA.ppGoals info.goalsAfter info.inConv
let goalsBefore ← ctxB.ppGoals info.goalsBefore
let goalsAfter ← ctxA.ppGoals info.goalsAfter
return f!"Tactic @ {formatElabInfo ctx info.toElabInfo}\n{info.stx}\nbefore {goalsBefore}\nafter {goalsAfter}"
def MacroExpansionInfo.format (ctx : ContextInfo) (info : MacroExpansionInfo) : IO Format := do

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

@ -195,7 +195,6 @@ elab_stx_quot Parser.Term.attr.quot
elab_stx_quot Parser.Term.prio.quot
elab_stx_quot Parser.Term.doElem.quot
elab_stx_quot Parser.Term.dynamicQuot
elab_stx_quot Parser.Term.conv.quot
/- match -/

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

@ -39,8 +39,6 @@ structure Context where
main : MVarId
-- declaration name of the executing elaborator, used by `mkTacticInfo` to persist it in the info tree
elaborator : Name
-- `true` when in `conv` tactic mode. This flag is only used to pretty print the goals showing just the left-hand-side
inConv : Bool := false
structure State where
goals : List MVarId
@ -121,7 +119,6 @@ def mkTacticInfo (mctxBefore : MetavarContext) (goalsBefore : List MVarId) (stx
stx := stx
mctxAfter := (← getMCtx)
goalsAfter := (← getUnsolvedGoals)
inConv := (← read).inConv
}
def mkInitialTacticInfo (stx : Syntax) : TacticM (TacticM Info) := do

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

@ -11,10 +11,10 @@ import Lean.Elab.Tactic.BuiltinTactic
namespace Lean.Elab.Tactic.Conv
open Meta
def mkConvGoalFor (lhs : Expr) : TacticM (Expr × Expr) := do
def mkConvGoalFor (lhs : Expr) : MetaM (Expr × Expr) := do
let lhsType ← inferType lhs
let rhs ← mkFreshExprMVar lhsType
let targetNew ← mkEq lhs rhs
let targetNew := mkLHSGoal (← mkEq lhs rhs)
let newGoal ← mkFreshExprSyntheticOpaqueMVar targetNew
return (rhs, newGoal)
@ -23,7 +23,7 @@ def convert (lhs : Expr) (conv : TacticM Unit) : TacticM (Expr × Expr) := do
let savedGoals ← getGoals
try
setGoals [newGoal.mvarId!]
withReader (fun ctx => { ctx with inConv := true }) conv
conv
pruneSolvedGoals
for mvarId in (← getGoals) do
try
@ -35,11 +35,14 @@ def convert (lhs : Expr) (conv : TacticM Unit) : TacticM (Expr × Expr) := do
setGoals savedGoals
return (← instantiateMVars rhs, ← instantiateMVars newGoal)
def getLhsRhs : TacticM (Expr × Expr) :=
withMainContext do
let some (_, lhs, rhs) ← matchEq? (← getMainTarget) | throwError "invalid 'conv' goal"
def getLhsRhsCore (mvarId : MVarId) : MetaM (Expr × Expr) :=
withMVarContext mvarId do
let some (_, lhs, rhs) ← matchEq? (← getMVarType mvarId) | throwError "invalid 'conv' goal"
return (lhs, rhs)
def getLhsRhs : TacticM (Expr × Expr) := do
getLhsRhsCore (← getMainGoal)
def getLhs : TacticM Expr :=
return (← getLhsRhs).1
@ -49,7 +52,7 @@ def getRhs : TacticM Expr :=
/-- `⊢ lhs = rhs` ~~> `⊢ lhs' = rhs` using `h : lhs = lhs'`. -/
def updateLhs (lhs' : Expr) (h : Expr) : TacticM Unit := do
let rhs ← getRhs
let newGoal ← mkFreshExprSyntheticOpaqueMVar (← mkEq lhs' rhs)
let newGoal ← mkFreshExprSyntheticOpaqueMVar (mkLHSGoal (← mkEq lhs' rhs))
assignExprMVar (← getMainGoal) (← mkEqTrans h newGoal)
replaceMainGoal [newGoal.mvarId!]
@ -57,7 +60,7 @@ def updateLhs (lhs' : Expr) (h : Expr) : TacticM Unit := do
def changeLhs (lhs' : Expr) : TacticM Unit := do
let rhs ← getRhs
liftMetaTactic1 fun mvarId => do
replaceTargetDefEq mvarId (← mkEq lhs' rhs)
replaceTargetDefEq mvarId (mkLHSGoal (← mkEq lhs' rhs))
@[builtinTactic Lean.Parser.Tactic.Conv.skip] def evalSkip : Tactic := fun stx => do
liftMetaTactic1 fun mvarId => do

24
stage0/src/Lean/Elab/Tactic/Conv/Congr.lean generated
View file

@ -9,9 +9,9 @@ import Lean.Elab.Tactic.Conv.Basic
namespace Lean.Elab.Tactic.Conv
open Meta
@[builtinTactic Lean.Parser.Tactic.Conv.congr] def evalCongr : Tactic := fun stx => do
withMainContext do
let (lhs, rhs) ← getLhsRhs
def congr (mvarId : MVarId) : MetaM (List MVarId) :=
withMVarContext mvarId do
let (lhs, rhs) ← getLhsRhsCore mvarId
unless lhs.isApp do
throwError "invalid 'congr' conv tactic, application expected{indentD lhs}"
lhs.withApp fun f args => do
@ -35,7 +35,21 @@ open Meta
i := i + 1
let proof ← r.getProof
assignExprMVar rhs.mvarId! r.expr
assignExprMVar (← getMainGoal) proof
replaceMainGoal newGoals.toList
assignExprMVar mvarId proof
return newGoals.toList
@[builtinTactic Lean.Parser.Tactic.Conv.congr] def evalCongr : Tactic := fun stx => do
replaceMainGoal (← congr (← getMainGoal))
@[builtinTactic Lean.Parser.Tactic.Conv.lhs] def evalLhs : Tactic := fun stx => do
let [mvarId₁, mvarId₂] ← congr (← getMainGoal) | throwError "invalid 'lhs' conv tactic, binary application expected"
applyRefl mvarId₂
replaceMainGoal [mvarId₁]
@[builtinTactic Lean.Parser.Tactic.Conv.rhs] def evalRhs : Tactic := fun stx => do
let [mvarId₁, mvarId₂] ← congr (← getMainGoal) | throwError "invalid 'rhs' conv tactic, binary application expected"
applyRefl mvarId₁
replaceMainGoal [mvarId₂]
end Lean.Elab.Tactic.Conv

16
stage0/src/Lean/Expr.lean generated
View file

@ -1038,6 +1038,22 @@ def annotation? (kind : Name) (e : Expr) : Option Expr :=
| Expr.mdata d b _ => if d.size == 1 && d.getBool kind false then some b else none
| _ => none
/--
Annotate `e` with the LHS annotation. The delaborator displays
expressions of the form `lhs = rhs` as `lhs` when they have this annotation.
-/
def mkLHSGoal (e : Expr) : Expr :=
mkAnnotation `_lhsGoal e
def isLHSGoal? (e : Expr) : Option Expr :=
match annotation? `_lhsGoal e with
| none => none
| some e =>
if e.isAppOfArity `Eq 3 then
some e.appFn!.appArg!
else
none
def mkFreshFVarId {m : Type → Type} [Monad m] [MonadNameGenerator m] : m FVarId :=
mkFreshId

17
stage0/src/Lean/Meta/PPGoal.lean generated
View file

@ -144,20 +144,7 @@ end ToHide
private def addLine (fmt : Format) : Format :=
if fmt.isNil then fmt else fmt ++ Format.line
/--
Return the target type for the given goal.
If `inConv == true` and target type is an equality, then return the left-hand-side only. -/
def getGoalTarget (mvarDecl : MetavarDecl) (inConv : Bool) : MetaM Expr := do
let target ← instantiateMVars mvarDecl.type
if inConv then
if let some (_, lhs, _) ← matchEq? target then
instantiateMVars lhs
else
return target
else
return target
def ppGoal (mvarId : MVarId) (inConv := false) : MetaM Format := do
def ppGoal (mvarId : MVarId) : MetaM Format := do
match (← getMCtx).findDecl? mvarId with
| none => pure "unknown goal"
| some mvarDecl => do
@ -214,7 +201,7 @@ def ppGoal (mvarId : MVarId) (inConv := false) : MetaM Format := do
ppVars varNames prevType? fmt localDecl
let fmt ← pushPending varNames type? fmt
let fmt := addLine fmt
let typeFmt ← ppExpr (← getGoalTarget mvarDecl inConv)
let typeFmt ← ppExpr (← instantiateMVars mvarDecl.type)
let fmt := fmt ++ "⊢ " ++ Format.nest indent typeFmt
match mvarDecl.userName with
| Name.anonymous => pure fmt

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

@ -245,7 +245,6 @@ def bracketedBinderF := bracketedBinder -- no default arg
@[builtinTermParser] def bracketedBinder.quot : Parser := leading_parser "`(bracketedBinder|" >> incQuotDepth (evalInsideQuot ``bracketedBinderF bracketedBinder) >> ")"
@[builtinTermParser] def matchDiscr.quot : Parser := leading_parser "`(matchDiscr|" >> incQuotDepth (evalInsideQuot ``matchDiscr matchDiscr) >> ")"
@[builtinTermParser] def attr.quot : Parser := leading_parser "`(attr|" >> incQuotDepth attrParser >> ")"
@[builtinTermParser] def conv.quot : Parser := leading_parser "`(conv|" >> incQuotDepth convParser >> ")"
@[builtinTermParser] def panic := leading_parser:leadPrec "panic! " >> termParser
@[builtinTermParser] def unreachable := leading_parser:leadPrec "unreachable!"

2
stage0/src/Lean/PrettyPrinter/Delaborator/Builtins.lean generated
View file

@ -446,6 +446,8 @@ def delabMData : Delab := do
`(.($s)) -- We only include the inaccessible annotation when we are delaborating patterns
else
return s
else if let some _ := isLHSGoal? (← getExpr) then
withMDataExpr <| withAppFn <| withAppArg <| delab
else
withMDataOptions delab

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

@ -148,7 +148,7 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio
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 (Widget.goalToInteractive g ti.inConv))
ci.runMetaM {} <| goals.mapM (fun g => Meta.withPPInaccessibleNames (Widget.goalToInteractive g))
return some { goals := goals.toArray }
return none
@ -182,7 +182,7 @@ partial def getInteractiveTermGoal (p : Lsp.PlainTermGoalParams)
-- for binders, hide the last hypothesis (the binder itself)
let lctx' := if ti.isBinder then i.lctx.pop else i.lctx
let goal ← ci.runMetaM lctx' do
Meta.withPPInaccessibleNames <| Widget.goalToInteractive (← Meta.mkFreshExprMVar ty).mvarId! (inConv := false)
Meta.withPPInaccessibleNames <| Widget.goalToInteractive (← Meta.mkFreshExprMVar ty).mvarId!
let range := if let some r := i.range? then r.toLspRange text else ⟨p.position, p.position⟩
return some { goal with range }
return none

4
stage0/src/Lean/Widget/InteractiveGoal.lean generated
View file

@ -66,7 +66,7 @@ structure InteractiveGoals where
open Meta in
/-- A variant of `Meta.ppGoal` which preserves subexpression information for interactivity. -/
def goalToInteractive (mvarId : MVarId) (inConv : Bool) : MetaM InteractiveGoal := do
def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
let some mvarDecl ← (← getMCtx).findDecl? mvarId
| throwError "unknown goal {mvarId}"
let ppAuxDecls := pp.auxDecls.get (← getOptions)
@ -118,7 +118,7 @@ def goalToInteractive (mvarId : MVarId) (inConv : Bool) : MetaM InteractiveGoal
else
ppVars varNames prevType? hyps localDecl
let hyps ← pushPending varNames type? hyps
let goalTp ← getGoalTarget mvarDecl inConv
let goalTp ← instantiateMVars mvarDecl.type
let goalFmt ← exprToInteractive goalTp
let userName? := match mvarDecl.userName with
| Name.anonymous => none

3473
stage0/stdlib/Init/Conv.c generated
View file

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

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

@ -202,7 +202,6 @@ lean_object* l_Lean_Elab_Term_Quotation_mkTuple_match__1(lean_object*);
static lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__2;
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__9___closed__18;
static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3210____closed__5;
static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__1;
static lean_object* l_Lean_Elab_Term_Quotation_myMacro____x40_Lean_Elab_Quotation___hyg_2895____closed__43;
lean_object* l_Array_toSubarray___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3190____closed__1;
@ -287,11 +286,9 @@ lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compile
lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__17___boxed(lean_object**);
static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__23___closed__5;
static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___closed__11;
static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__5;
lean_object* l_Lean_Elab_Term_Quotation_resolveSectionVariable_loop_match__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__12___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3235_(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240_(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3205_(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3220_(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3210_(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -548,7 +545,6 @@ static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_
static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3175____closed__14;
lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_floatOutAntiquotTerms___spec__2___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__15___closed__6;
static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__3;
lean_object* l_Function_comp___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_getCurrMacroScope(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_deduplicate_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -589,7 +585,7 @@ static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_
lean_object* l_Std_RBNode_find___at___private_Lean_Hygiene_0__Lean_sanitizeSyntaxAux___spec__2(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__24(lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___spec__7___closed__5;
lean_object* l_Lean_Elab_Term_Quotation_initFn____x40_Lean_Elab_Quotation___hyg_9735_(lean_object*);
lean_object* l_Lean_Elab_Term_Quotation_initFn____x40_Lean_Elab_Quotation___hyg_9730_(lean_object*);
lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__9___lambda__3___closed__24;
static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___closed__3;
@ -735,7 +731,6 @@ lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Q
lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3205_(lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3185_(lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3190_(lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240_(lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3235_(lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3225_(lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3220_(lean_object*);
@ -861,7 +856,6 @@ static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean
extern lean_object* l_Lean_instInhabitedName;
static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_floatOutAntiquotTerms___lambda__2___closed__11;
static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___closed__5;
static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__4;
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___spec__9___boxed(lean_object**);
static lean_object* l_Lean_Elab_Term_Quotation_myMacro____x40_Lean_Elab_Quotation___hyg_2895____closed__55;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___spec__10(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*, size_t, size_t, lean_object*);
@ -1072,7 +1066,6 @@ lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_floatOu
static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__11___closed__3;
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__9___closed__7;
static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__2;
static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__10___closed__13;
lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__4(lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3190____closed__2;
@ -13797,73 +13790,6 @@ x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
lean_object* l_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240_(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
_start:
{
lean_object* x_10; lean_object* x_11;
x_10 = l_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3175____closed__1;
x_11 = l_Lean_Elab_Term_adaptExpander(x_10, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
return x_11;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("conv");
return x_1;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_floatOutAntiquotTerms___lambda__2___closed__6;
x_2 = l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__2;
x_2 = l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3175____closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3175____closed__12;
x_2 = lean_unsigned_to_nat(3240u);
x_3 = lean_name_mk_numeral(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240_), 9, 0);
return x_1;
}
}
lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_2 = l_Lean_Elab_Term_termElabAttribute;
x_3 = l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__3;
x_4 = l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__4;
x_5 = l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__5;
x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_noOpMatchAdaptPats_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
@ -30975,7 +30901,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getSepFromSplice___closed__2;
x_2 = l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___lambda__3___closed__5;
x_3 = lean_unsigned_to_nat(497u);
x_3 = lean_unsigned_to_nat(496u);
x_4 = lean_unsigned_to_nat(12u);
x_5 = l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getSepFromSplice___closed__4;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -33854,7 +33780,7 @@ x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
lean_object* l_Lean_Elab_Term_Quotation_initFn____x40_Lean_Elab_Quotation___hyg_9735_(lean_object* x_1) {
lean_object* l_Lean_Elab_Term_Quotation_initFn____x40_Lean_Elab_Quotation___hyg_9730_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -34868,19 +34794,6 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lea
res = l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3235_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__1 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__1);
l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__2 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__2();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__2);
l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__3 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__3();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__3);
l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__4 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__4();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__4);
l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__5 = _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__5();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240____closed__5);
res = l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3240_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_noOpMatchAdaptPats___lambda__1___closed__1 = _init_l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_noOpMatchAdaptPats___lambda__1___closed__1();
lean_mark_persistent(l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_noOpMatchAdaptPats___lambda__1___closed__1);
l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_noOpMatchAdaptPats___lambda__1___closed__2 = _init_l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_noOpMatchAdaptPats___lambda__1___closed__2();
@ -35364,7 +35277,7 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchSyntax___c
res = l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchSyntax(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = l_Lean_Elab_Term_Quotation_initFn____x40_Lean_Elab_Quotation___hyg_9735_(lean_io_mk_world());
res = l_Lean_Elab_Term_Quotation_initFn____x40_Lean_Elab_Quotation___hyg_9730_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));

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

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

3089
stage0/stdlib/Lean/Elab/Tactic/Conv/Congr.c generated
View file

File diff suppressed because it is too large Load diff

29
stage0/stdlib/Lean/Elab/Tactic/Conv/Rewrite.c generated Normal file
View file

@ -0,0 +1,29 @@
// Lean compiler output
// Module: Lean.Elab.Tactic.Conv.Rewrite
// Imports: Init
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
#ifdef __cplusplus
extern "C" {
#endif
lean_object* initialize_Init(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Lean_Elab_Tactic_Conv_Rewrite(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus
}
#endif

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

@ -366,7 +366,7 @@ lean_object* l_Lean_throwKernelException___at_Lean_Elab_Term_evalExpr___spec__4(
lean_object* l_Lean_Elab_Term_mkFreshIdent___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_isMonadApp___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Lean_Meta_ppGoal(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_ppGoal(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_resolveLocalName_loop_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_isExplicit___boxed(lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_addAutoBoundImplicits___spec__5(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -10953,10 +10953,9 @@ return x_11;
lean_object* l_Lean_Elab_Term_ppGoal(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
uint8_t x_9; lean_object* x_10;
x_9 = 0;
x_10 = l_Lean_Meta_ppGoal(x_1, x_9, x_4, x_5, x_6, x_7, x_8);
return x_10;
lean_object* x_9;
x_9 = l_Lean_Meta_ppGoal(x_1, x_4, x_5, x_6, x_7, x_8);
return x_9;
}
}
lean_object* l_Lean_Elab_Term_ppGoal___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {

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

@ -21,6 +21,7 @@ lean_object* l_Lean_Expr_data_match__1(lean_object*);
static lean_object* l_Lean_Expr_ctorName___closed__7;
static lean_object* l_Lean_mkNatLit___closed__8;
lean_object* l_Lean_instLTLiteral;
static lean_object* l_Lean_mkLHSGoal___closed__2;
uint8_t l_Lean_Expr_bindingInfo_x21(lean_object*);
lean_object* l_Lean_Expr_updateSort___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_update_forall(lean_object*, uint8_t, lean_object*, lean_object*);
@ -34,6 +35,7 @@ lean_object* l_Lean_Expr_isApp_match__1___rarg(lean_object*, lean_object*, lean_
static lean_object* l___private_Lean_Expr_0__Lean_reprLiteral____x40_Lean_Expr___hyg_98____closed__1;
lean_object* l_Lean_Expr_hasAnyFVar_visit_match__1(lean_object*);
static lean_object* l_Lean_mkNatLit___closed__4;
lean_object* l_Lean_isLHSGoal_x3f(lean_object*);
lean_object* l_Lean_Expr_mvarId_x21(lean_object*);
lean_object* l_Lean_Expr_bindingDomain_x21___boxed(lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprLiteral____x40_Lean_Expr___hyg_98____closed__2;
@ -124,6 +126,7 @@ static lean_object* l___private_Lean_Expr_0__Lean_reprLiteral____x40_Lean_Expr__
lean_object* l_Lean_Expr_hasLevelParamEx___boxed(lean_object*);
uint64_t l_Lean_Expr_Data_hash(uint64_t);
lean_object* l_Lean_Expr_instantiateLevelParamsCore_visit_match__1(lean_object*);
lean_object* l_Lean_mkLHSGoal(lean_object*);
static lean_object* l_Lean_mkDecIsTrue___closed__5;
lean_object* l_Lean_mkMVar(lean_object*);
size_t l_USize_sub(size_t, size_t);
@ -196,6 +199,7 @@ lean_object* l_Lean_Expr_isNatLit_match__1___rarg(lean_object*, lean_object*, le
lean_object* l_Lean_Expr_getOptParamDefault_x3f(lean_object*);
lean_object* l_Nat_max(lean_object*, lean_object*);
lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_361__match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_isLHSGoal_x3f_match__1(lean_object*);
lean_object* l_Lean_Expr_getRevArgD(lean_object*, lean_object*, lean_object*);
uint64_t l_List_foldl___at_Lean_mkConst___spec__1(uint64_t, lean_object*);
lean_object* l_List_mapTRAux___at_Lean_Expr_instantiateLevelParams___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -330,6 +334,7 @@ lean_object* l_Lean_Expr_instantiateLevelParamsCore_visit_match__1___rarg(lean_o
lean_object* l_Lean_BinderInfo_isInstImplicit_match__1(lean_object*);
lean_object* l_Lean_Expr_replaceFVar(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_headBeta(lean_object*);
static lean_object* l_Lean_isLHSGoal_x3f___closed__1;
uint8_t lean_expr_binder_info(lean_object*);
static uint64_t l_Lean_Expr_mkData___closed__2;
lean_object* lean_level_update_max(lean_object*, lean_object*, lean_object*);
@ -392,6 +397,7 @@ static lean_object* l_Lean_Literal_type___closed__1;
lean_object* lean_expr_abstract_range(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_getArg_x21___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Expr_bindingDomain_x21___closed__1;
lean_object* l_Lean_isLHSGoal_x3f___boxed(lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_361____closed__21;
static lean_object* l_Lean_Expr_getRevArg_x21___closed__3;
lean_object* l_Lean_Expr_isConst_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -399,6 +405,7 @@ lean_object* l_Lean_BinderInfo_isInstImplicit_match__1___rarg___boxed(lean_objec
lean_object* l_Lean_Expr_instantiateLevelParamsCore_visit___at_Lean_Expr_instantiateLevelParams___spec__1___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Expr_ctorName___closed__3;
lean_object* l_Lean_Expr_hasAnyFVar_visit___at_Lean_Expr_containsFVar___spec__1___boxed(lean_object*, lean_object*);
static lean_object* l_Lean_isLHSGoal_x3f___closed__2;
lean_object* l_Lean_Expr_natLit_x3f(lean_object*);
lean_object* lean_expr_mk_const(lean_object*, lean_object*);
lean_object* l_Lean_Expr_data_match__1___rarg(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*);
@ -629,6 +636,7 @@ lean_object* l_Lean_Expr_quickLt___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Expr_instToStringExpr;
static lean_object* l_Lean_mkEM___closed__4;
lean_object* l___private_Lean_Expr_0__Lean_Expr_getAppArgsAux_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_isLHSGoal_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_isFVar_match__1___rarg(lean_object*, lean_object*, lean_object*);
uint64_t l_UInt32_toUInt64(uint32_t);
lean_object* l_Lean_ExprStructEq_instToStringExprStructEq___boxed(lean_object*);
@ -737,6 +745,7 @@ static lean_object* l_Lean_mkNot___closed__1;
static lean_object* l___private_Lean_Expr_0__Lean_reprLiteral____x40_Lean_Expr___hyg_98____closed__7;
lean_object* l_Array_mapMUnsafe_map___at_Lean_Expr_setAppPPExplicit___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_mkLHSGoal___closed__1;
uint64_t l_UInt64_shiftRight(uint64_t, uint64_t);
lean_object* l_Lean_Expr_hasLooseBVars___boxed(lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_361____closed__11;
@ -16202,6 +16211,164 @@ lean_dec(x_1);
return x_3;
}
}
static lean_object* _init_l_Lean_mkLHSGoal___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("_lhsGoal");
return x_1;
}
}
static lean_object* _init_l_Lean_mkLHSGoal___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_mkLHSGoal___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_mkLHSGoal(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_mkLHSGoal___closed__2;
x_3 = l_Lean_mkAnnotation(x_2, x_1);
return x_3;
}
}
lean_object* l_Lean_isLHSGoal_x3f_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
lean_object* x_4; lean_object* x_5;
lean_dec(x_3);
x_4 = lean_box(0);
x_5 = lean_apply_1(x_2, x_4);
return x_5;
}
else
{
lean_object* x_6; lean_object* x_7;
lean_dec(x_2);
x_6 = lean_ctor_get(x_1, 0);
lean_inc(x_6);
lean_dec(x_1);
x_7 = lean_apply_1(x_3, x_6);
return x_7;
}
}
}
lean_object* l_Lean_isLHSGoal_x3f_match__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_isLHSGoal_x3f_match__1___rarg), 3, 0);
return x_2;
}
}
static lean_object* _init_l_Lean_isLHSGoal_x3f___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Eq");
return x_1;
}
}
static lean_object* _init_l_Lean_isLHSGoal_x3f___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_isLHSGoal_x3f___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_isLHSGoal_x3f(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_mkLHSGoal___closed__2;
x_3 = l_Lean_annotation_x3f(x_2, x_1);
if (lean_obj_tag(x_3) == 0)
{
lean_object* x_4;
x_4 = lean_box(0);
return x_4;
}
else
{
uint8_t x_5;
x_5 = !lean_is_exclusive(x_3);
if (x_5 == 0)
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9;
x_6 = lean_ctor_get(x_3, 0);
x_7 = l_Lean_isLHSGoal_x3f___closed__2;
x_8 = lean_unsigned_to_nat(3u);
x_9 = l_Lean_Expr_isAppOfArity(x_6, x_7, x_8);
if (x_9 == 0)
{
lean_object* x_10;
lean_free_object(x_3);
lean_dec(x_6);
x_10 = lean_box(0);
return x_10;
}
else
{
lean_object* x_11; lean_object* x_12;
x_11 = l_Lean_Expr_appFn_x21(x_6);
lean_dec(x_6);
x_12 = l_Lean_Expr_appArg_x21(x_11);
lean_dec(x_11);
lean_ctor_set(x_3, 0, x_12);
return x_3;
}
}
else
{
lean_object* x_13; lean_object* x_14; lean_object* x_15; uint8_t x_16;
x_13 = lean_ctor_get(x_3, 0);
lean_inc(x_13);
lean_dec(x_3);
x_14 = l_Lean_isLHSGoal_x3f___closed__2;
x_15 = lean_unsigned_to_nat(3u);
x_16 = l_Lean_Expr_isAppOfArity(x_13, x_14, x_15);
if (x_16 == 0)
{
lean_object* x_17;
lean_dec(x_13);
x_17 = lean_box(0);
return x_17;
}
else
{
lean_object* x_18; lean_object* x_19; lean_object* x_20;
x_18 = l_Lean_Expr_appFn_x21(x_13);
lean_dec(x_13);
x_19 = l_Lean_Expr_appArg_x21(x_18);
lean_dec(x_18);
x_20 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_20, 0, x_19);
return x_20;
}
}
}
}
}
lean_object* l_Lean_isLHSGoal_x3f___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_isLHSGoal_x3f(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* l_Lean_mkFreshFVarId___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -16808,6 +16975,14 @@ l_Lean_Expr_setPPUniverses___closed__2 = _init_l_Lean_Expr_setPPUniverses___clos
lean_mark_persistent(l_Lean_Expr_setPPUniverses___closed__2);
l_Lean_mkAnnotation___closed__1 = _init_l_Lean_mkAnnotation___closed__1();
lean_mark_persistent(l_Lean_mkAnnotation___closed__1);
l_Lean_mkLHSGoal___closed__1 = _init_l_Lean_mkLHSGoal___closed__1();
lean_mark_persistent(l_Lean_mkLHSGoal___closed__1);
l_Lean_mkLHSGoal___closed__2 = _init_l_Lean_mkLHSGoal___closed__2();
lean_mark_persistent(l_Lean_mkLHSGoal___closed__2);
l_Lean_isLHSGoal_x3f___closed__1 = _init_l_Lean_isLHSGoal_x3f___closed__1();
lean_mark_persistent(l_Lean_isLHSGoal_x3f___closed__1);
l_Lean_isLHSGoal_x3f___closed__2 = _init_l_Lean_isLHSGoal_x3f___closed__2();
lean_mark_persistent(l_Lean_isLHSGoal_x3f___closed__2);
l_Lean_mkNot___closed__1 = _init_l_Lean_mkNot___closed__1();
lean_mark_persistent(l_Lean_mkNot___closed__1);
l_Lean_mkNot___closed__2 = _init_l_Lean_mkNot___closed__2();

5005
stage0/stdlib/Lean/Meta/IndPredBelow.c generated
View file

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

19
stage0/stdlib/Lean/PrettyPrinter.c generated
View file

@ -44,6 +44,7 @@ static lean_object* l_Lean_PPContext_runMetaM___rarg___closed__4;
uint8_t l_USize_decLt(size_t, size_t);
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_PrettyPrinter_0__Lean_PrettyPrinter_noContext___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Lean_Meta_ppGoal(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_PrettyPrinter_0__Lean_PrettyPrinter_withoutContext___rarg(lean_object*, lean_object*);
static lean_object* l_Lean_PPContext_runMetaM___rarg___closed__9;
extern lean_object* l_Lean_PrettyPrinter_parenthesizerAttribute;
@ -113,7 +114,6 @@ lean_object* l___private_Lean_PrettyPrinter_0__Lean_PrettyPrinter_withoutContext
lean_object* l_Lean_Parser_Module_module_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
lean_object* l_instHashableProd___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_ppGoal___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ParserCompiler_registerParserCompiler___rarg(lean_object*, lean_object*);
extern lean_object* l_Lean_Expr_instBEqExpr;
lean_object* l___private_Lean_PrettyPrinter_0__Lean_PrettyPrinter_withoutContext___at_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter___hyg_329____spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1910,16 +1910,13 @@ return x_6;
lean_object* l_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter___hyg_329____lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_4 = 0;
x_5 = lean_box(x_4);
x_6 = lean_alloc_closure((void*)(l_Lean_Meta_ppGoal___boxed), 7, 2);
lean_closure_set(x_6, 0, x_2);
lean_closure_set(x_6, 1, x_5);
x_7 = lean_alloc_closure((void*)(l___private_Lean_PrettyPrinter_0__Lean_PrettyPrinter_withoutContext___at_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter___hyg_329____spec__1), 6, 1);
lean_closure_set(x_7, 0, x_6);
x_8 = l_Lean_PPContext_runMetaM___rarg(x_1, x_7, x_3);
return x_8;
lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = lean_alloc_closure((void*)(l_Lean_Meta_ppGoal), 6, 1);
lean_closure_set(x_4, 0, x_2);
x_5 = lean_alloc_closure((void*)(l___private_Lean_PrettyPrinter_0__Lean_PrettyPrinter_withoutContext___at_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter___hyg_329____spec__1), 6, 1);
lean_closure_set(x_5, 0, x_4);
x_6 = l_Lean_PPContext_runMetaM___rarg(x_1, x_5, x_3);
return x_6;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter___hyg_329____closed__1() {

453
stage0/stdlib/Lean/PrettyPrinter/Delaborator/Builtins.c generated
View file

@ -46,6 +46,7 @@ lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAux
lean_object* l_Array_foldrMUnsafe_fold___at_Lean_PrettyPrinter_Delaborator_delabForall___spec__2(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNameMkNum___closed__3;
lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_PrettyPrinter_Delaborator_delab___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_isLHSGoal_x3f(lean_object*);
lean_object* l_Array_mapIdxM_map___at___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_delabPatterns___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppImplicit___lambda__3___closed__1;
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabLam___lambda__3___closed__4;
@ -58,6 +59,7 @@ lean_object* l_Lean_PrettyPrinter_Delaborator_unfoldMDatas_match__1(lean_object*
lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppMatch_match__3(lean_object*);
lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNameMkStr(lean_object*);
static lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withMDataExpr___at_Lean_PrettyPrinter_Delaborator_withMDataOptions___spec__2___rarg___closed__1;
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppArg___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_stringToMessageData(lean_object*);
lean_object* l_List_forIn_loop___at_Lean_PrettyPrinter_Delaborator_withMDataOptions___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppMatch_match__3___rarg(lean_object*, lean_object*);
@ -120,6 +122,7 @@ lean_object* l_Lean_PrettyPrinter_Delaborator_delabOfScientific_match__2___rarg(
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabLam___lambda__3___closed__2;
lean_object* l_Lean_getPPAnalysisNamedArg___boxed(lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_PrettyPrinter_Delaborator_delabAppMatch___spec__12___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppArg___at_Lean_PrettyPrinter_Delaborator_delabMData___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_forIn_loop___at_Lean_PrettyPrinter_Delaborator_isRegularApp___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lambda__5___closed__9;
lean_object* l_Lean_Expr_bindingDomain_x21(lean_object*);
@ -142,7 +145,6 @@ static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabFVar___cl
lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNameMkNum(lean_object*);
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabLam___lambda__3___closed__1;
lean_object* l_Array_mapMUnsafe_map___at_Lean_PrettyPrinter_Delaborator_delabAppMatch___spec__14(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppArg___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_PrettyPrinter_Delaborator_unexpandStructureInstance___lambda__3___closed__15;
uint8_t l_Array_anyMUnsafe_any___at_Lean_PrettyPrinter_Delaborator_delabAppExplicit___spec__1(lean_object*, size_t, size_t);
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppArg___at_Lean_PrettyPrinter_Delaborator_delabDoElems___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -188,7 +190,6 @@ static lean_object* l_Lean_PrettyPrinter_Delaborator_delabOfScientific_match__1_
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withBindingBody___at___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_delabPatterns_usingNamesAux___spec__1___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_hasIdent_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_withMDataOptions___at_Lean_PrettyPrinter_Delaborator_withMDatasOptions___spec__1(lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_descend___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_delabConst___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_get(lean_object*, lean_object*);
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabLam___lambda__3___closed__3;
@ -245,6 +246,7 @@ lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabAppExplicit(lean
lean_object* l_Lean_PrettyPrinter_Delaborator_delabLam_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withLetDecl___at_Lean_PrettyPrinter_Delaborator_delabLetE___spec__1(lean_object*);
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabProjectionApp___closed__3;
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppFn___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_pow(lean_object*, lean_object*);
static lean_object* l_Array_mapMUnsafe_map___at_Lean_PrettyPrinter_Delaborator_delabDo___spec__1___closed__1;
lean_object* l_Lean_PrettyPrinter_Delaborator_reifyName___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -392,7 +394,6 @@ lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppImplicit___lambda__2___box
uint8_t l_Array_anyMUnsafe_any___at_Lean_PrettyPrinter_Delaborator_hasIdent___spec__1(lean_object*, lean_object*, size_t, size_t);
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabConst___lambda__3___closed__6;
lean_object* l___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_checkForNameClash(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppFn___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_isRegularApp___lambda__1(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_delabDIte_delabBranch_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_delabProj_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -409,6 +410,7 @@ lean_object* l_Lean_PrettyPrinter_Delaborator_hasIdent___boxed(lean_object*, lea
lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_PrettyPrinter_Delaborator_delabAppMatch___spec__15(lean_object*, lean_object*, size_t, size_t, lean_object*);
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNameMkStr___closed__1;
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppFn___at_Lean_PrettyPrinter_Delaborator_delabMData___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabSort___closed__14;
lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabAppImplicit(lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_unexpandStructureInstance___lambda__2(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -446,12 +448,14 @@ static lean_object* l_Lean_PrettyPrinter_Delaborator_unexpandStructureInstance__
lean_object* l_Lean_PrettyPrinter_Delaborator_reifyName_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabLetE___closed__6;
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabMData___closed__5;
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabAppMatch___closed__2;
lean_object* l_Lean_Meta_mkLambdaFVars(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabLetE___closed__4;
lean_object* l_Lean_PrettyPrinter_Delaborator_delabBVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_delabConst___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_fvarId_x21(lean_object*);
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabMData___closed__4;
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabSort___closed__3;
lean_object* l___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_delabPatterns_usingNamesAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabFVar___closed__3;
@ -575,7 +579,6 @@ static lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withProj___at_Lean_
lean_object* l_Lean_PrettyPrinter_Delaborator_delabLetE___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_getRevAliases(lean_object*, lean_object*);
extern lean_object* l_Lean_instInhabitedExpr;
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__11;
lean_object* l___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_delabPatterns_usingNames(lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_delabDoElems___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_firstM___at_Lean_PrettyPrinter_Delaborator_unexpandRegularApp___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -608,7 +611,6 @@ lean_object* l_Std_Range_forIn_loop___at_Lean_PrettyPrinter_Delaborator_isRegula
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabAppExplicit___closed__4;
lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabForall(lean_object*);
lean_object* l_Lean_mkSepArray(lean_object*, lean_object*);
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__10;
lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabSort(lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withBindingBody___at___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_skippingBinders_loop_visitLambda___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabForall___closed__1;
@ -666,7 +668,6 @@ extern lean_object* l_Lean_projectionFnInfoExt;
static lean_object* l_Array_mapMUnsafe_map___at_Lean_PrettyPrinter_Delaborator_delabAppMatch___spec__9___closed__1;
lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_getPPCoercions___boxed(lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_descend___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withBindingBody___at___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_delabPatterns_usingNamesAux___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_PrettyPrinter_Delaborator_delabDo___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_ParamKind_isRegularExplicit___boxed(lean_object*);
@ -731,6 +732,7 @@ lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppMatch___lambda__4(lean_obj
lean_object* l_Array_foldrMUnsafe_fold___at_Lean_PrettyPrinter_Delaborator_delabForall___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_PrettyPrinter_Delaborator_getParamKinds___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_scientificLitKind;
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_descend___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_maybeAddBlockImplicit(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_bindingName_x21(lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_getParamKinds_forallTelescopeArgs___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -814,7 +816,6 @@ static lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lambda__
lean_object* l_Lean_PrettyPrinter_Delaborator_delabOfNat_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_delabOfScientific___lambda__1(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_descend___at___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_delabPatterns_usingNamesAux___spec__2(lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppArg___at_Lean_PrettyPrinter_Delaborator_delabProjectionApp___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabConst___lambda__4___closed__1;
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabConst___lambda__3___closed__10;
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppFnArgs___at_Lean_PrettyPrinter_Delaborator_delabAppMatch___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -925,7 +926,6 @@ lean_object* l_Lean_PrettyPrinter_Delaborator_unexpandRegularApp_match__1(lean_o
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppMatch___lambda__6___closed__9;
lean_object* l_Lean_PrettyPrinter_Delaborator_getParamKinds_forallTelescopeArgs___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* l_ReaderT_instMonadReaderT___rarg(lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppFn___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_delabForall___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_lengthTRAux___rarg(lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_withMDataOptions___at_Lean_PrettyPrinter_Delaborator_withMDatasOptions___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -959,6 +959,7 @@ lean_object* l_List_forIn_loop___at_Lean_PrettyPrinter_Delaborator_withMDatasOpt
lean_object* l_Lean_PrettyPrinter_Delaborator_delabSort_match__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_pure___at_Lean_PrettyPrinter_Delaborator_instMonadQuotationDelabM___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_skippingBinders_loop___rarg___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* l_Lean_PrettyPrinter_Delaborator_SubExpr_descend___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_delabLetE_match__1(lean_object*);
static lean_object* l_Lean_PrettyPrinter_Delaborator_reifyName_match__1___rarg___closed__2;
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_HoleIterator_next(lean_object*);
@ -20123,25 +20124,79 @@ return x_37;
}
}
}
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppArg___at_Lean_PrettyPrinter_Delaborator_delabMData___spec__4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_9 = l_Lean_PrettyPrinter_Delaborator_SubExpr_getExpr___at_Lean_PrettyPrinter_Delaborator_getExprKind___spec__1(x_2, x_3, x_4, x_5, x_6, x_7, x_8);
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_9, 1);
lean_inc(x_11);
lean_dec(x_9);
x_12 = l_Lean_Expr_appArg_x21(x_10);
lean_dec(x_10);
x_13 = lean_unsigned_to_nat(1u);
x_14 = l_Lean_PrettyPrinter_Delaborator_SubExpr_descend___at_Lean_PrettyPrinter_Delaborator_delab___spec__2(x_12, x_13, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_11);
return x_14;
}
}
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppFn___at_Lean_PrettyPrinter_Delaborator_delabMData___spec__5(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_9 = l_Lean_PrettyPrinter_Delaborator_SubExpr_getExpr___at_Lean_PrettyPrinter_Delaborator_getExprKind___spec__1(x_2, x_3, x_4, x_5, x_6, x_7, x_8);
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_9, 1);
lean_inc(x_11);
lean_dec(x_9);
x_12 = l_Lean_Expr_appFn_x21(x_10);
lean_dec(x_10);
x_13 = lean_unsigned_to_nat(0u);
x_14 = l_Lean_PrettyPrinter_Delaborator_SubExpr_descend___at_Lean_PrettyPrinter_Delaborator_delab___spec__2(x_12, x_13, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_11);
return x_14;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabMData___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lambda__5___closed__2;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppArg___at_Lean_PrettyPrinter_Delaborator_delabMData___spec__4), 8, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabMData___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_PrettyPrinter_Delaborator_delabMData___closed__1;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppFn___at_Lean_PrettyPrinter_Delaborator_delabMData___spec__5), 8, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabMData___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("inaccessible");
return x_1;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabMData___closed__2() {
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabMData___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_PrettyPrinter_Delaborator_maybeAddBlockImplicit___closed__7;
x_2 = l_Lean_PrettyPrinter_Delaborator_delabMData___closed__1;
x_2 = l_Lean_PrettyPrinter_Delaborator_delabMData___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabMData___closed__3() {
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabMData___closed__5() {
_start:
{
lean_object* x_1;
@ -20163,139 +20218,159 @@ x_11 = l_Lean_Meta_Match_inaccessible_x3f(x_9);
lean_dec(x_9);
if (lean_obj_tag(x_11) == 0)
{
lean_object* x_12; lean_object* x_13;
x_12 = l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lambda__5___closed__2;
x_13 = l_Lean_PrettyPrinter_Delaborator_withMDataOptions___at_Lean_PrettyPrinter_Delaborator_delabMData___spec__1(x_12, x_1, x_2, x_3, x_4, x_5, x_6, x_10);
return x_13;
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_12 = l_Lean_PrettyPrinter_Delaborator_SubExpr_getExpr___at_Lean_PrettyPrinter_Delaborator_getExprKind___spec__1(x_1, x_2, x_3, x_4, x_5, x_6, x_10);
x_13 = lean_ctor_get(x_12, 0);
lean_inc(x_13);
x_14 = lean_ctor_get(x_12, 1);
lean_inc(x_14);
lean_dec(x_12);
x_15 = l_Lean_isLHSGoal_x3f(x_13);
lean_dec(x_13);
if (lean_obj_tag(x_15) == 0)
{
lean_object* x_16; lean_object* x_17;
x_16 = l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lambda__5___closed__2;
x_17 = l_Lean_PrettyPrinter_Delaborator_withMDataOptions___at_Lean_PrettyPrinter_Delaborator_delabMData___spec__1(x_16, x_1, x_2, x_3, x_4, x_5, x_6, x_14);
return x_17;
}
else
{
lean_object* x_14; lean_object* x_15;
lean_object* x_18; lean_object* x_19;
lean_dec(x_15);
x_18 = l_Lean_PrettyPrinter_Delaborator_delabMData___closed__2;
x_19 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withMDataExpr___at_Lean_PrettyPrinter_Delaborator_delabMData___spec__3(x_18, x_1, x_2, x_3, x_4, x_5, x_6, x_14);
return x_19;
}
}
else
{
lean_object* x_20; lean_object* x_21;
lean_dec(x_11);
x_14 = l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lambda__5___closed__2;
x_20 = l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lambda__5___closed__2;
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_1);
x_15 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withMDataExpr___at_Lean_PrettyPrinter_Delaborator_delabMData___spec__3(x_14, x_1, x_2, x_3, x_4, x_5, x_6, x_10);
if (lean_obj_tag(x_15) == 0)
x_21 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withMDataExpr___at_Lean_PrettyPrinter_Delaborator_delabMData___spec__3(x_20, x_1, x_2, x_3, x_4, x_5, x_6, x_10);
if (lean_obj_tag(x_21) == 0)
{
uint8_t x_16;
x_16 = lean_ctor_get_uint8(x_1, sizeof(void*)*5);
uint8_t x_22;
x_22 = lean_ctor_get_uint8(x_1, sizeof(void*)*5);
lean_dec(x_1);
if (x_16 == 0)
if (x_22 == 0)
{
uint8_t x_17;
uint8_t x_23;
lean_dec(x_6);
lean_dec(x_5);
x_17 = !lean_is_exclusive(x_15);
if (x_17 == 0)
x_23 = !lean_is_exclusive(x_21);
if (x_23 == 0)
{
return x_15;
return x_21;
}
else
{
lean_object* x_18; lean_object* x_19; lean_object* x_20;
x_18 = lean_ctor_get(x_15, 0);
x_19 = lean_ctor_get(x_15, 1);
lean_inc(x_19);
lean_inc(x_18);
lean_dec(x_15);
x_20 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_20, 0, x_18);
lean_ctor_set(x_20, 1, x_19);
return x_20;
}
}
else
{
lean_object* x_21; lean_object* x_22; lean_object* x_23; uint8_t x_24;
x_21 = lean_ctor_get(x_15, 0);
lean_inc(x_21);
x_22 = lean_ctor_get(x_15, 1);
lean_inc(x_22);
lean_dec(x_15);
x_23 = l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_PrettyPrinter_Delaborator_delab___spec__3___rarg(x_5, x_6, x_22);
lean_dec(x_6);
x_24 = !lean_is_exclusive(x_23);
if (x_24 == 0)
{
lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35;
x_25 = lean_ctor_get(x_23, 0);
x_26 = l_Lean_PrettyPrinter_Delaborator_delabMData___closed__3;
lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_24 = lean_ctor_get(x_21, 0);
x_25 = lean_ctor_get(x_21, 1);
lean_inc(x_25);
x_27 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_27, 0, x_25);
lean_ctor_set(x_27, 1, x_26);
x_28 = l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lambda__5___closed__9;
x_29 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_29, 0, x_25);
lean_ctor_set(x_29, 1, x_28);
x_30 = l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lambda__5___closed__10;
x_31 = lean_array_push(x_30, x_27);
x_32 = lean_array_push(x_31, x_21);
x_33 = lean_array_push(x_32, x_29);
x_34 = l_Lean_PrettyPrinter_Delaborator_delabMData___closed__2;
x_35 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_35, 0, x_34);
lean_ctor_set(x_35, 1, x_33);
lean_ctor_set(x_23, 0, x_35);
return x_23;
lean_inc(x_24);
lean_dec(x_21);
x_26 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_26, 0, x_24);
lean_ctor_set(x_26, 1, x_25);
return x_26;
}
}
else
{
lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48;
x_36 = lean_ctor_get(x_23, 0);
x_37 = lean_ctor_get(x_23, 1);
lean_inc(x_37);
lean_inc(x_36);
lean_dec(x_23);
x_38 = l_Lean_PrettyPrinter_Delaborator_delabMData___closed__3;
lean_inc(x_36);
x_39 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_39, 0, x_36);
lean_ctor_set(x_39, 1, x_38);
x_40 = l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lambda__5___closed__9;
x_41 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_41, 0, x_36);
lean_ctor_set(x_41, 1, x_40);
x_42 = l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lambda__5___closed__10;
x_43 = lean_array_push(x_42, x_39);
x_44 = lean_array_push(x_43, x_21);
x_45 = lean_array_push(x_44, x_41);
x_46 = l_Lean_PrettyPrinter_Delaborator_delabMData___closed__2;
x_47 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_47, 0, x_46);
lean_ctor_set(x_47, 1, x_45);
x_48 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_48, 0, x_47);
lean_ctor_set(x_48, 1, x_37);
return x_48;
lean_object* x_27; lean_object* x_28; lean_object* x_29; uint8_t x_30;
x_27 = lean_ctor_get(x_21, 0);
lean_inc(x_27);
x_28 = lean_ctor_get(x_21, 1);
lean_inc(x_28);
lean_dec(x_21);
x_29 = l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_PrettyPrinter_Delaborator_delab___spec__3___rarg(x_5, x_6, x_28);
lean_dec(x_6);
x_30 = !lean_is_exclusive(x_29);
if (x_30 == 0)
{
lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41;
x_31 = lean_ctor_get(x_29, 0);
x_32 = l_Lean_PrettyPrinter_Delaborator_delabMData___closed__5;
lean_inc(x_31);
x_33 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_33, 0, x_31);
lean_ctor_set(x_33, 1, x_32);
x_34 = l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lambda__5___closed__9;
x_35 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_35, 0, x_31);
lean_ctor_set(x_35, 1, x_34);
x_36 = l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lambda__5___closed__10;
x_37 = lean_array_push(x_36, x_33);
x_38 = lean_array_push(x_37, x_27);
x_39 = lean_array_push(x_38, x_35);
x_40 = l_Lean_PrettyPrinter_Delaborator_delabMData___closed__4;
x_41 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_41, 0, x_40);
lean_ctor_set(x_41, 1, x_39);
lean_ctor_set(x_29, 0, x_41);
return x_29;
}
else
{
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;
x_42 = lean_ctor_get(x_29, 0);
x_43 = lean_ctor_get(x_29, 1);
lean_inc(x_43);
lean_inc(x_42);
lean_dec(x_29);
x_44 = l_Lean_PrettyPrinter_Delaborator_delabMData___closed__5;
lean_inc(x_42);
x_45 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_45, 0, x_42);
lean_ctor_set(x_45, 1, x_44);
x_46 = l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lambda__5___closed__9;
x_47 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_47, 0, x_42);
lean_ctor_set(x_47, 1, x_46);
x_48 = l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lambda__5___closed__10;
x_49 = lean_array_push(x_48, x_45);
x_50 = lean_array_push(x_49, x_27);
x_51 = lean_array_push(x_50, x_47);
x_52 = l_Lean_PrettyPrinter_Delaborator_delabMData___closed__4;
x_53 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_53, 0, x_52);
lean_ctor_set(x_53, 1, x_51);
x_54 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_54, 0, x_53);
lean_ctor_set(x_54, 1, x_43);
return x_54;
}
}
}
else
{
uint8_t x_49;
uint8_t x_55;
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_1);
x_49 = !lean_is_exclusive(x_15);
if (x_49 == 0)
x_55 = !lean_is_exclusive(x_21);
if (x_55 == 0)
{
return x_15;
return x_21;
}
else
{
lean_object* x_50; lean_object* x_51; lean_object* x_52;
x_50 = lean_ctor_get(x_15, 0);
x_51 = lean_ctor_get(x_15, 1);
lean_inc(x_51);
lean_inc(x_50);
lean_dec(x_15);
x_52 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_52, 0, x_50);
lean_ctor_set(x_52, 1, x_51);
return x_52;
lean_object* x_56; lean_object* x_57; lean_object* x_58;
x_56 = lean_ctor_get(x_21, 0);
x_57 = lean_ctor_get(x_21, 1);
lean_inc(x_57);
lean_inc(x_56);
lean_dec(x_21);
x_58 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_58, 0, x_56);
lean_ctor_set(x_58, 1, x_57);
return x_58;
}
}
}
@ -22507,7 +22582,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_PrettyPrinter_Delaborator_delabFVar___closed__2;
x_2 = l_Lean_PrettyPrinter_Delaborator_delabLam___lambda__3___closed__12;
x_3 = lean_unsigned_to_nat(546u);
x_3 = lean_unsigned_to_nat(548u);
x_4 = lean_unsigned_to_nat(44u);
x_5 = l_Lean_PrettyPrinter_Delaborator_delabFVar___closed__4;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -25540,7 +25615,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_PrettyPrinter_Delaborator_delabFVar___closed__2;
x_2 = l_Lean_PrettyPrinter_Delaborator_delabLetE___closed__1;
x_3 = lean_unsigned_to_nat(583u);
x_3 = lean_unsigned_to_nat(585u);
x_4 = lean_unsigned_to_nat(38u);
x_5 = l_Lean_PrettyPrinter_Delaborator_delabFVar___closed__4;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -26397,7 +26472,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_PrettyPrinter_Delaborator_delabFVar___closed__2;
x_2 = l_Lean_PrettyPrinter_Delaborator_delabLit___closed__1;
x_3 = lean_unsigned_to_nat(596u);
x_3 = lean_unsigned_to_nat(598u);
x_4 = lean_unsigned_to_nat(31u);
x_5 = l_Lean_PrettyPrinter_Delaborator_delabFVar___closed__4;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -28139,7 +28214,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_PrettyPrinter_Delaborator_delabFVar___closed__2;
x_2 = l_Lean_PrettyPrinter_Delaborator_delabProj___closed__1;
x_3 = lean_unsigned_to_nat(635u);
x_3 = lean_unsigned_to_nat(637u);
x_4 = lean_unsigned_to_nat(38u);
x_5 = l_Lean_PrettyPrinter_Delaborator_delabFVar___closed__4;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -28451,23 +28526,6 @@ x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Delaborator_delabProjectio
return x_2;
}
}
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppArg___at_Lean_PrettyPrinter_Delaborator_delabProjectionApp___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_9 = l_Lean_PrettyPrinter_Delaborator_SubExpr_getExpr___at_Lean_PrettyPrinter_Delaborator_getExprKind___spec__1(x_2, x_3, x_4, x_5, x_6, x_7, x_8);
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_9, 1);
lean_inc(x_11);
lean_dec(x_9);
x_12 = l_Lean_Expr_appArg_x21(x_10);
lean_dec(x_10);
x_13 = lean_unsigned_to_nat(1u);
x_14 = l_Lean_PrettyPrinter_Delaborator_SubExpr_descend___at_Lean_PrettyPrinter_Delaborator_delab___spec__2(x_12, x_13, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_11);
return x_14;
}
}
lean_object* l_Lean_PrettyPrinter_Delaborator_delabProjectionApp___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
@ -28595,7 +28653,7 @@ lean_dec(x_30);
x_34 = l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lambda__5___closed__2;
lean_inc(x_7);
lean_inc(x_6);
x_35 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppArg___at_Lean_PrettyPrinter_Delaborator_delabProjectionApp___spec__1(x_34, x_2, x_3, x_4, x_5, x_6, x_7, x_33);
x_35 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppArg___at_Lean_PrettyPrinter_Delaborator_delabMData___spec__4(x_34, x_2, x_3, x_4, x_5, x_6, x_7, x_33);
if (lean_obj_tag(x_35) == 0)
{
lean_object* x_36; lean_object* x_37; lean_object* x_38; uint8_t x_39;
@ -28728,7 +28786,7 @@ lean_object* x_77; lean_object* x_78;
x_77 = l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lambda__5___closed__2;
lean_inc(x_7);
lean_inc(x_6);
x_78 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppArg___at_Lean_PrettyPrinter_Delaborator_delabProjectionApp___spec__1(x_77, x_2, x_3, x_4, x_5, x_6, x_7, x_70);
x_78 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppArg___at_Lean_PrettyPrinter_Delaborator_delabMData___spec__4(x_77, x_2, x_3, x_4, x_5, x_6, x_7, x_70);
if (lean_obj_tag(x_78) == 0)
{
lean_object* x_79; lean_object* x_80; lean_object* x_81; uint8_t x_82;
@ -29301,24 +29359,7 @@ lean_dec(x_1);
return x_9;
}
}
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppFn___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_9 = l_Lean_PrettyPrinter_Delaborator_SubExpr_getExpr___at_Lean_PrettyPrinter_Delaborator_getExprKind___spec__1(x_2, x_3, x_4, x_5, x_6, x_7, x_8);
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_9, 1);
lean_inc(x_11);
lean_dec(x_9);
x_12 = l_Lean_Expr_appFn_x21(x_10);
lean_dec(x_10);
x_13 = lean_unsigned_to_nat(0u);
x_14 = l_Lean_PrettyPrinter_Delaborator_SubExpr_descend___at_Lean_PrettyPrinter_Delaborator_delab___spec__2(x_12, x_13, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_11);
return x_14;
}
}
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_descend___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_descend___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
_start:
{
uint8_t x_11;
@ -29380,7 +29421,7 @@ return x_31;
}
}
}
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppArg___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppArg___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
@ -29393,11 +29434,11 @@ lean_dec(x_9);
x_12 = l_Lean_Expr_appArg_x21(x_10);
lean_dec(x_10);
x_13 = lean_unsigned_to_nat(1u);
x_14 = l_Lean_PrettyPrinter_Delaborator_SubExpr_descend___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__3(x_12, x_13, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_11);
x_14 = l_Lean_PrettyPrinter_Delaborator_SubExpr_descend___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__2(x_12, x_13, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_11);
return x_14;
}
}
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppFn___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppFn___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
@ -29410,7 +29451,7 @@ lean_dec(x_9);
x_12 = l_Lean_Expr_appFn_x21(x_10);
lean_dec(x_10);
x_13 = lean_unsigned_to_nat(0u);
x_14 = l_Lean_PrettyPrinter_Delaborator_SubExpr_descend___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__3(x_12, x_13, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_11);
x_14 = l_Lean_PrettyPrinter_Delaborator_SubExpr_descend___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__2(x_12, x_13, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_11);
return x_14;
}
}
@ -29418,8 +29459,8 @@ static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lambda__5___closed__2;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppArg___at_Lean_PrettyPrinter_Delaborator_delabProjectionApp___spec__1), 8, 1);
x_1 = l_Lean_PrettyPrinter_Delaborator_delabMData___closed__2;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppFn___at_Lean_PrettyPrinter_Delaborator_delabMData___spec__5), 8, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
@ -29428,43 +29469,23 @@ static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__1;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppFn___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__1), 8, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__2;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppFn___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__1), 8, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_box(0);
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Delaborator_delabDIte_delabBranch), 8, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__5() {
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__4;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppArg___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__2), 8, 1);
x_1 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__2;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppArg___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__1), 8, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__6() {
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__4() {
_start:
{
lean_object* x_1;
@ -29472,17 +29493,17 @@ x_1 = lean_mk_string("termDepIfThenElse");
return x_1;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__7() {
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__6;
x_2 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__4;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__8() {
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__6() {
_start:
{
lean_object* x_1;
@ -29490,7 +29511,7 @@ x_1 = lean_mk_string("if");
return x_1;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__9() {
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__7() {
_start:
{
lean_object* x_1;
@ -29498,7 +29519,7 @@ x_1 = lean_mk_string("then");
return x_1;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__10() {
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__8() {
_start:
{
lean_object* x_1;
@ -29506,7 +29527,7 @@ x_1 = lean_mk_string("else");
return x_1;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__11() {
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2;
@ -29561,14 +29582,14 @@ goto block_88;
block_88:
{
lean_object* x_14; lean_object* x_15;
x_14 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__3;
x_14 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__1;
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
x_15 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppFn___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__1(x_14, x_2, x_3, x_4, x_5, x_6, x_7, x_13);
x_15 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppFn___at_Lean_PrettyPrinter_Delaborator_delabMData___spec__5(x_14, x_2, x_3, x_4, x_5, x_6, x_7, x_13);
if (lean_obj_tag(x_15) == 0)
{
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
@ -29577,14 +29598,14 @@ lean_inc(x_16);
x_17 = lean_ctor_get(x_15, 1);
lean_inc(x_17);
lean_dec(x_15);
x_18 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__5;
x_18 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__3;
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
x_19 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppFn___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__4(x_18, x_2, x_3, x_4, x_5, x_6, x_7, x_17);
x_19 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppFn___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__3(x_18, x_2, x_3, x_4, x_5, x_6, x_7, x_17);
if (lean_obj_tag(x_19) == 0)
{
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;
@ -29605,7 +29626,7 @@ x_25 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Delaborator_delabDIte_del
lean_closure_set(x_25, 0, x_24);
lean_inc(x_7);
lean_inc(x_6);
x_26 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppArg___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__2(x_25, x_2, x_3, x_4, x_5, x_6, x_7, x_21);
x_26 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppArg___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__1(x_25, x_2, x_3, x_4, x_5, x_6, x_7, x_21);
if (lean_obj_tag(x_26) == 0)
{
lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; uint8_t x_31;
@ -29624,7 +29645,7 @@ if (x_31 == 0)
{
lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; 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;
x_32 = lean_ctor_get(x_30, 0);
x_33 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__8;
x_33 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__6;
lean_inc(x_32);
x_34 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_34, 0, x_32);
@ -29635,16 +29656,16 @@ lean_inc(x_32);
x_37 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_37, 0, x_32);
lean_ctor_set(x_37, 1, x_36);
x_38 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__9;
x_38 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__7;
lean_inc(x_32);
x_39 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_39, 0, x_32);
lean_ctor_set(x_39, 1, x_38);
x_40 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__10;
x_40 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__8;
x_41 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_41, 0, x_32);
lean_ctor_set(x_41, 1, x_40);
x_42 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__11;
x_42 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__9;
x_43 = lean_array_push(x_42, x_34);
x_44 = lean_array_push(x_43, x_35);
x_45 = lean_array_push(x_44, x_37);
@ -29653,7 +29674,7 @@ x_47 = lean_array_push(x_46, x_39);
x_48 = lean_array_push(x_47, x_22);
x_49 = lean_array_push(x_48, x_41);
x_50 = lean_array_push(x_49, x_29);
x_51 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__7;
x_51 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__5;
x_52 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_52, 0, x_51);
lean_ctor_set(x_52, 1, x_50);
@ -29668,7 +29689,7 @@ x_54 = lean_ctor_get(x_30, 1);
lean_inc(x_54);
lean_inc(x_53);
lean_dec(x_30);
x_55 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__8;
x_55 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__6;
lean_inc(x_53);
x_56 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_56, 0, x_53);
@ -29679,16 +29700,16 @@ lean_inc(x_53);
x_59 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_59, 0, x_53);
lean_ctor_set(x_59, 1, x_58);
x_60 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__9;
x_60 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__7;
lean_inc(x_53);
x_61 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_61, 0, x_53);
lean_ctor_set(x_61, 1, x_60);
x_62 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__10;
x_62 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__8;
x_63 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_63, 0, x_53);
lean_ctor_set(x_63, 1, x_62);
x_64 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__11;
x_64 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__9;
x_65 = lean_array_push(x_64, x_56);
x_66 = lean_array_push(x_65, x_57);
x_67 = lean_array_push(x_66, x_59);
@ -29697,7 +29718,7 @@ x_69 = lean_array_push(x_68, x_61);
x_70 = lean_array_push(x_69, x_22);
x_71 = lean_array_push(x_70, x_63);
x_72 = lean_array_push(x_71, x_29);
x_73 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__7;
x_73 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__5;
x_74 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_74, 0, x_73);
lean_ctor_set(x_74, 1, x_72);
@ -29826,11 +29847,11 @@ x_10 = l_Lean_PrettyPrinter_Delaborator_whenPPOption(x_8, x_9, x_1, x_2, x_3, x_
return x_10;
}
}
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_descend___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_descend___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11;
x_11 = l_Lean_PrettyPrinter_Delaborator_SubExpr_descend___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__3(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
x_11 = l_Lean_PrettyPrinter_Delaborator_SubExpr_descend___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__2(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
lean_dec(x_2);
return x_11;
}
@ -30009,14 +30030,14 @@ goto block_62;
block_62:
{
lean_object* x_18; lean_object* x_19;
x_18 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__1;
x_18 = l_Lean_PrettyPrinter_Delaborator_delabMData___closed__1;
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
lean_inc(x_1);
x_19 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppFn___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__1(x_18, x_1, x_2, x_3, x_4, x_5, x_6, x_17);
x_19 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppFn___at_Lean_PrettyPrinter_Delaborator_delabMData___spec__5(x_18, x_1, x_2, x_3, x_4, x_5, x_6, x_17);
if (lean_obj_tag(x_19) == 0)
{
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23;
@ -30028,7 +30049,7 @@ lean_dec(x_19);
x_22 = l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lambda__5___closed__2;
lean_inc(x_6);
lean_inc(x_5);
x_23 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppArg___at_Lean_PrettyPrinter_Delaborator_delabProjectionApp___spec__1(x_22, x_1, x_2, x_3, x_4, x_5, x_6, x_21);
x_23 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppArg___at_Lean_PrettyPrinter_Delaborator_delabMData___spec__4(x_22, x_1, x_2, x_3, x_4, x_5, x_6, x_21);
if (lean_obj_tag(x_23) == 0)
{
lean_object* x_24; lean_object* x_25; uint8_t x_26;
@ -30901,7 +30922,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_PrettyPrinter_Delaborator_delabFVar___closed__2;
x_2 = l_Lean_PrettyPrinter_Delaborator_delabDoElems___closed__5;
x_3 = lean_unsigned_to_nat(707u);
x_3 = lean_unsigned_to_nat(709u);
x_4 = lean_unsigned_to_nat(40u);
x_5 = l_Lean_PrettyPrinter_Delaborator_delabFVar___closed__4;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -31219,14 +31240,14 @@ x_84 = l_Lean_instInhabitedExpr;
x_85 = lean_unsigned_to_nat(2u);
x_86 = lean_array_get(x_84, x_83, x_85);
lean_dec(x_83);
x_87 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__1;
x_87 = l_Lean_PrettyPrinter_Delaborator_delabMData___closed__1;
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
lean_inc(x_1);
x_88 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppFn___at_Lean_PrettyPrinter_Delaborator_delabDIte___spec__1(x_87, x_1, x_2, x_3, x_4, x_5, x_6, x_10);
x_88 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppFn___at_Lean_PrettyPrinter_Delaborator_delabMData___spec__5(x_87, x_1, x_2, x_3, x_4, x_5, x_6, x_10);
if (lean_obj_tag(x_88) == 0)
{
lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94;
@ -36044,6 +36065,10 @@ l_Lean_PrettyPrinter_Delaborator_delabMData___closed__2 = _init_l_Lean_PrettyPri
lean_mark_persistent(l_Lean_PrettyPrinter_Delaborator_delabMData___closed__2);
l_Lean_PrettyPrinter_Delaborator_delabMData___closed__3 = _init_l_Lean_PrettyPrinter_Delaborator_delabMData___closed__3();
lean_mark_persistent(l_Lean_PrettyPrinter_Delaborator_delabMData___closed__3);
l_Lean_PrettyPrinter_Delaborator_delabMData___closed__4 = _init_l_Lean_PrettyPrinter_Delaborator_delabMData___closed__4();
lean_mark_persistent(l_Lean_PrettyPrinter_Delaborator_delabMData___closed__4);
l_Lean_PrettyPrinter_Delaborator_delabMData___closed__5 = _init_l_Lean_PrettyPrinter_Delaborator_delabMData___closed__5();
lean_mark_persistent(l_Lean_PrettyPrinter_Delaborator_delabMData___closed__5);
l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabMData___closed__1 = _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabMData___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabMData___closed__1);
l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabMData___closed__2 = _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabMData___closed__2();
@ -36319,10 +36344,6 @@ l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__8 = _init_l_Lea
lean_mark_persistent(l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__8);
l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__9 = _init_l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__9();
lean_mark_persistent(l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__9);
l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__10 = _init_l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__10();
lean_mark_persistent(l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__10);
l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__11 = _init_l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__11();
lean_mark_persistent(l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__11);
l_Lean_PrettyPrinter_Delaborator_delabDIte___closed__1 = _init_l_Lean_PrettyPrinter_Delaborator_delabDIte___closed__1();
lean_mark_persistent(l_Lean_PrettyPrinter_Delaborator_delabDIte___closed__1);
l_Lean_PrettyPrinter_Delaborator_delabDIte___closed__2 = _init_l_Lean_PrettyPrinter_Delaborator_delabDIte___closed__2();

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

File diff suppressed because it is too large Load diff

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

@ -110,6 +110,7 @@ lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_initFn____x40_Lean_Server_F
static lean_object* l___private_Lean_Data_Lsp_Diagnostics_0__Lean_Lsp_toJsonDiagnosticWith____x40_Lean_Data_Lsp_Diagnostics___hyg_851____at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_821____spec__4___closed__1;
lean_object* l_Lean_Widget_getInteractiveDiagnostics___rarg___lambda__2(lean_object*);
lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_209____spec__1___lambda__7(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_7008____spec__22(lean_object*);
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_209____closed__2;
lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instFromJsonRpcEncodingPacket;
static lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_209____spec__1___lambda__5___closed__1;
@ -130,7 +131,6 @@ lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_initFn____x40_Lean_Server_F
static lean_object* l___private_Lean_Server_FileWorker_WidgetRequests_0__Lean_Widget_Lean_Widget_InfoPopup_fromJsonRpcEncodingPacket____x40_Lean_Server_FileWorker_WidgetRequests___hyg_322____closed__1;
lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___lambda__8(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_7010____spec__22(lean_object*);
static lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_209____spec__1___closed__1;
lean_object* l_Lean_Server_WithRpcRef_encodeUnsafe___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_209____spec__6(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Data_Lsp_Diagnostics_0__Lean_Lsp_toJsonDiagnosticWith____x40_Lean_Data_Lsp_Diagnostics___hyg_851____at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_821____spec__4___closed__7;
@ -339,11 +339,11 @@ lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEnco
lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_525____spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_525____lambda__5(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_525____lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_7010____spec__20(lean_object*);
static lean_object* l_Lean_Widget_getInteractiveDiagnostics___rarg___closed__2;
static lean_object* l_Lean_Server_WithRpcRef_decodeUnsafeAs___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_209____spec__4___rarg___closed__4;
static lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___closed__2;
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_732____closed__5;
lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_7008____spec__20(lean_object*);
lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonDocumentFilter____x40_Lean_Data_Lsp_Basic___hyg_1594____spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__16(lean_object*);
lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__15(lean_object*);
@ -8936,7 +8936,7 @@ lean_inc(x_12);
x_13 = lean_ctor_get(x_11, 1);
lean_inc(x_13);
lean_dec(x_11);
x_14 = l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_7010____spec__20(x_3);
x_14 = l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_7008____spec__20(x_3);
x_15 = lean_alloc_closure((void*)(l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_209____spec__1___lambda__1___boxed), 3, 1);
lean_closure_set(x_15, 0, x_14);
x_16 = l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_732____spec__1___lambda__3___closed__1;
@ -9634,7 +9634,7 @@ lean_inc(x_12);
x_13 = lean_ctor_get(x_11, 1);
lean_inc(x_13);
lean_dec(x_11);
x_14 = l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_7010____spec__22(x_3);
x_14 = l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_7008____spec__22(x_3);
x_15 = lean_alloc_closure((void*)(l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_209____spec__1___lambda__1___boxed), 3, 1);
lean_closure_set(x_15, 0, x_14);
x_16 = l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_732____spec__1___lambda__3___closed__1;

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

@ -388,19 +388,17 @@ return x_3;
static lean_object* _init_l_Lean_Widget_instInhabitedInfoWithCtx___closed__19() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5;
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_Widget_instInhabitedInfoWithCtx___closed__18;
x_3 = l_Lean_Widget_instInhabitedInfoWithCtx___closed__12;
x_4 = 0;
x_5 = lean_alloc_ctor(0, 5, 1);
lean_ctor_set(x_5, 0, x_2);
lean_ctor_set(x_5, 1, x_3);
lean_ctor_set(x_5, 2, x_1);
lean_ctor_set(x_5, 3, x_3);
lean_ctor_set(x_5, 4, x_1);
lean_ctor_set_uint8(x_5, sizeof(void*)*5, x_4);
return x_5;
x_4 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_4, 0, x_2);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set(x_4, 2, x_1);
lean_ctor_set(x_4, 3, x_3);
lean_ctor_set(x_4, 4, x_1);
return x_4;
}
}
static lean_object* _init_l_Lean_Widget_instInhabitedInfoWithCtx___closed__20() {

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

@ -313,7 +313,7 @@ static lean_object* l_Lean_Widget_InteractiveGoal_pretty___closed__3;
lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InteractiveGoals_instRpcEncodingInteractiveGoalsRpcEncodingPacket___spec__40___rarg___lambda__1(lean_object*, lean_object*, size_t);
lean_object* l_Lean_Widget_goalToInteractive_ppVars_match__1(lean_object*);
lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InteractiveGoal_instRpcEncodingInteractiveGoalRpcEncodingPacket___spec__18___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Widget_goalToInteractive___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* l_Lean_Widget_goalToInteractive___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_Lean_Widget_InteractiveTermGoal_instRpcEncodingInteractiveTermGoalRpcEncodingPacket___spec__4___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InteractiveGoal_instRpcEncodingInteractiveGoalRpcEncodingPacket___spec__6___rarg___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InteractiveHypothesis_instRpcEncodingInteractiveHypothesisRpcEncodingPacket___spec__18(lean_object*);
@ -503,7 +503,6 @@ lean_object* l_Lean_Widget_InteractiveGoal_pretty_match__2(lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InteractiveGoals_instRpcEncodingInteractiveGoalsRpcEncodingPacket___spec__6___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Widget_goalToInteractive___closed__1;
lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InteractiveHypothesis_instRpcEncodingInteractiveHypothesisRpcEncodingPacket___spec__13(lean_object*);
lean_object* l_Lean_Widget_goalToInteractive___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Widget_InteractiveGoal_0__Lean_Widget_Lean_Widget_InteractiveHypothesis_toJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveGoal___hyg_136_(lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InteractiveGoals_instRpcEncodingInteractiveGoalsRpcEncodingPacket___spec__3___rarg___lambda__1(size_t, lean_object*, lean_object*, lean_object*, size_t, lean_object*);
lean_object* l_String_intercalate(lean_object*, lean_object*);
@ -601,7 +600,6 @@ lean_object* l_Lean_Widget_instInhabitedInteractiveTermGoal;
static lean_object* l___private_Lean_Widget_InteractiveGoal_0__Lean_Widget_Lean_Widget_InteractiveGoals_fromJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveGoal___hyg_1077____closed__1;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Widget_goalToInteractive___spec__7(uint8_t, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Widget_TaggedText_0__Lean_Widget_fromJsonTaggedText____x40_Lean_Widget_TaggedText___hyg_344____at___private_Lean_Widget_InteractiveGoal_0__Lean_Widget_Lean_Widget_InteractiveHypothesis_fromJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveGoal___hyg_78____spec__2___lambda__1___boxed(lean_object*);
lean_object* l_Lean_Meta_getGoalTarget(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlFromMAux___at_Lean_Widget_goalToInteractive___spec__4(uint8_t, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InteractiveTermGoal_instRpcEncodingInteractiveTermGoalRpcEncodingPacket___spec__18(lean_object*);
lean_object* l_Lean_MetavarContext_findDecl_x3f(lean_object*, lean_object*);
@ -653,7 +651,7 @@ lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InteractiveHypo
static lean_object* l_Lean_Widget_goalToInteractive_ppVars___closed__1;
lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InteractiveHypothesis_instRpcEncodingInteractiveHypothesisRpcEncodingPacket___spec__11(lean_object*);
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonPlainGoal____x40_Lean_Data_Lsp_Extra___hyg_439____spec__1(size_t, size_t, lean_object*);
lean_object* l_Lean_Widget_goalToInteractive___lambda__1(lean_object*, uint8_t, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Widget_goalToInteractive___lambda__1(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InteractiveTermGoal_instRpcEncodingInteractiveTermGoalRpcEncodingPacket___spec__8___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Widget_InteractiveGoal_pretty___spec__1(lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l___private_Lean_Widget_InteractiveCode_0__Lean_Widget_Lean_Widget_InfoWithCtx_encodeUnsafe____x40_Lean_Widget_InteractiveCode___hyg_5____rarg(lean_object*, lean_object*, lean_object*);
@ -757,7 +755,7 @@ static lean_object* l_Lean_Widget_Lean_Widget_InteractiveGoals_instRpcEncodingIn
lean_object* l_Lean_LocalContext_sanitizeNames(lean_object*, lean_object*);
lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InteractiveTermGoal_instRpcEncodingInteractiveTermGoalRpcEncodingPacket___spec__35(lean_object*);
lean_object* l_Lean_Widget_goalToInteractive_ppVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Widget_goalToInteractive(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Widget_goalToInteractive(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InteractiveHypothesis_instRpcEncodingInteractiveHypothesisRpcEncodingPacket___spec__3___rarg(lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_Lean_Widget_InteractiveGoals_instRpcEncodingInteractiveGoalsRpcEncodingPacket___spec__1___rarg___lambda__1(size_t, lean_object*, lean_object*, size_t, lean_object*);
lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_Lean_Widget_InteractiveHypothesis_instRpcEncodingInteractiveHypothesisRpcEncodingPacket___spec__2___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, size_t);
@ -22310,303 +22308,306 @@ lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* l_Lean_Widget_goalToInteractive___lambda__1(lean_object* x_1, uint8_t x_2, lean_object* x_3, lean_object* x_4, uint8_t x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
lean_object* l_Lean_Widget_goalToInteractive___lambda__1(lean_object* x_1, uint8_t x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
_start:
{
lean_object* x_11;
lean_inc(x_9);
lean_object* x_10;
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
x_11 = l_Lean_Meta_ToHide_collect(x_1, x_6, x_7, x_8, x_9, x_10);
if (lean_obj_tag(x_11) == 0)
lean_inc(x_5);
lean_inc(x_1);
x_10 = l_Lean_Meta_ToHide_collect(x_1, x_5, x_6, x_7, x_8, x_9);
if (lean_obj_tag(x_10) == 0)
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_12 = lean_ctor_get(x_11, 0);
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18;
x_11 = lean_ctor_get(x_10, 0);
lean_inc(x_11);
x_12 = lean_ctor_get(x_10, 1);
lean_inc(x_12);
x_13 = lean_ctor_get(x_11, 1);
lean_dec(x_10);
x_13 = lean_ctor_get(x_11, 0);
lean_inc(x_13);
lean_dec(x_11);
x_14 = lean_ctor_get(x_12, 0);
x_14 = lean_ctor_get(x_11, 1);
lean_inc(x_14);
x_15 = lean_ctor_get(x_12, 1);
lean_inc(x_15);
lean_dec(x_12);
x_16 = lean_box(0);
x_17 = l_Lean_Widget_goalToInteractive___lambda__1___closed__2;
x_18 = lean_unsigned_to_nat(0u);
lean_inc(x_9);
lean_dec(x_11);
x_15 = lean_box(0);
x_16 = l_Lean_Widget_goalToInteractive___lambda__1___closed__2;
x_17 = lean_unsigned_to_nat(0u);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
x_19 = l_Lean_LocalContext_foldlM___at_Lean_Widget_goalToInteractive___spec__2(x_2, x_14, x_15, x_3, x_17, x_18, x_6, x_7, x_8, x_9, x_13);
lean_dec(x_15);
lean_inc(x_5);
x_18 = l_Lean_LocalContext_foldlM___at_Lean_Widget_goalToInteractive___spec__2(x_2, x_13, x_14, x_3, x_16, x_17, x_5, x_6, x_7, x_8, x_12);
lean_dec(x_14);
if (lean_obj_tag(x_19) == 0)
lean_dec(x_13);
if (lean_obj_tag(x_18) == 0)
{
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;
x_20 = lean_ctor_get(x_19, 0);
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_19 = lean_ctor_get(x_18, 0);
lean_inc(x_19);
x_20 = lean_ctor_get(x_19, 1);
lean_inc(x_20);
x_21 = lean_ctor_get(x_20, 1);
x_21 = lean_ctor_get(x_18, 1);
lean_inc(x_21);
x_22 = lean_ctor_get(x_19, 1);
lean_dec(x_18);
x_22 = lean_ctor_get(x_19, 0);
lean_inc(x_22);
lean_dec(x_19);
x_23 = lean_ctor_get(x_20, 0);
lean_inc(x_23);
lean_dec(x_20);
x_24 = lean_ctor_get(x_21, 0);
x_24 = lean_ctor_get(x_20, 1);
lean_inc(x_24);
x_25 = lean_ctor_get(x_21, 1);
lean_inc(x_25);
lean_dec(x_21);
lean_inc(x_9);
lean_dec(x_20);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
x_26 = l_Lean_Widget_goalToInteractive_pushPending(x_23, x_24, x_25, x_6, x_7, x_8, x_9, x_22);
if (lean_obj_tag(x_26) == 0)
lean_inc(x_5);
x_25 = l_Lean_Widget_goalToInteractive_pushPending(x_22, x_23, x_24, x_5, x_6, x_7, x_8, x_21);
if (lean_obj_tag(x_25) == 0)
{
lean_object* x_27; lean_object* x_28; lean_object* x_29;
x_27 = lean_ctor_get(x_26, 0);
lean_object* x_26; lean_object* x_27; lean_object* x_28;
x_26 = lean_ctor_get(x_25, 0);
lean_inc(x_26);
x_27 = lean_ctor_get(x_25, 1);
lean_inc(x_27);
x_28 = lean_ctor_get(x_26, 1);
lean_inc(x_28);
lean_dec(x_26);
lean_inc(x_9);
lean_dec(x_25);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_4);
x_29 = l_Lean_Meta_getGoalTarget(x_4, x_5, x_6, x_7, x_8, x_9, x_28);
if (lean_obj_tag(x_29) == 0)
lean_inc(x_5);
x_28 = l_Lean_Meta_instantiateMVars(x_1, x_5, x_6, x_7, x_8, x_27);
if (lean_obj_tag(x_28) == 0)
{
lean_object* x_30; lean_object* x_31; lean_object* x_32;
x_30 = lean_ctor_get(x_29, 0);
lean_object* x_29; lean_object* x_30; lean_object* x_31;
x_29 = lean_ctor_get(x_28, 0);
lean_inc(x_29);
x_30 = lean_ctor_get(x_28, 1);
lean_inc(x_30);
x_31 = lean_ctor_get(x_29, 1);
lean_inc(x_31);
lean_dec(x_29);
x_32 = l_Lean_Widget_exprToInteractive(x_30, x_6, x_7, x_8, x_9, x_31);
lean_dec(x_28);
x_31 = l_Lean_Widget_exprToInteractive(x_29, x_5, x_6, x_7, x_8, x_30);
if (lean_obj_tag(x_31) == 0)
{
lean_object* x_32;
x_32 = lean_ctor_get(x_4, 0);
lean_inc(x_32);
lean_dec(x_4);
if (lean_obj_tag(x_32) == 0)
{
lean_object* x_33;
x_33 = lean_ctor_get(x_4, 0);
lean_inc(x_33);
lean_dec(x_4);
if (lean_obj_tag(x_33) == 0)
uint8_t x_33;
x_33 = !lean_is_exclusive(x_31);
if (x_33 == 0)
{
uint8_t x_34;
x_34 = !lean_is_exclusive(x_32);
if (x_34 == 0)
{
lean_object* x_35; lean_object* x_36;
x_35 = lean_ctor_get(x_32, 0);
x_36 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_36, 0, x_27);
lean_ctor_set(x_36, 1, x_35);
lean_ctor_set(x_36, 2, x_16);
lean_ctor_set(x_32, 0, x_36);
return x_32;
lean_object* x_34; lean_object* x_35;
x_34 = lean_ctor_get(x_31, 0);
x_35 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_35, 0, x_26);
lean_ctor_set(x_35, 1, x_34);
lean_ctor_set(x_35, 2, x_15);
lean_ctor_set(x_31, 0, x_35);
return x_31;
}
else
{
lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40;
x_37 = lean_ctor_get(x_32, 0);
x_38 = lean_ctor_get(x_32, 1);
lean_inc(x_38);
lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39;
x_36 = lean_ctor_get(x_31, 0);
x_37 = lean_ctor_get(x_31, 1);
lean_inc(x_37);
lean_dec(x_32);
x_39 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_39, 0, x_27);
lean_inc(x_36);
lean_dec(x_31);
x_38 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_38, 0, x_26);
lean_ctor_set(x_38, 1, x_36);
lean_ctor_set(x_38, 2, x_15);
x_39 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_39, 0, x_38);
lean_ctor_set(x_39, 1, x_37);
lean_ctor_set(x_39, 2, x_16);
x_40 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_40, 0, x_39);
lean_ctor_set(x_40, 1, x_38);
return x_40;
return x_39;
}
}
else
{
uint8_t x_41;
x_41 = !lean_is_exclusive(x_32);
if (x_41 == 0)
uint8_t x_40;
x_40 = !lean_is_exclusive(x_31);
if (x_40 == 0)
{
lean_object* x_42; lean_object* x_43; uint8_t x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47;
x_42 = lean_ctor_get(x_32, 0);
x_43 = lean_erase_macro_scopes(x_33);
x_44 = 1;
x_45 = l_Lean_Name_toString(x_43, x_44);
x_46 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_46, 0, x_45);
x_47 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_47, 0, x_27);
lean_ctor_set(x_47, 1, x_42);
lean_ctor_set(x_47, 2, x_46);
lean_ctor_set(x_32, 0, x_47);
return x_32;
lean_object* x_41; lean_object* x_42; uint8_t x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46;
x_41 = lean_ctor_get(x_31, 0);
x_42 = lean_erase_macro_scopes(x_32);
x_43 = 1;
x_44 = l_Lean_Name_toString(x_42, x_43);
x_45 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_45, 0, x_44);
x_46 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_46, 0, x_26);
lean_ctor_set(x_46, 1, x_41);
lean_ctor_set(x_46, 2, x_45);
lean_ctor_set(x_31, 0, x_46);
return x_31;
}
else
{
lean_object* x_48; lean_object* x_49; lean_object* x_50; uint8_t x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55;
x_48 = lean_ctor_get(x_32, 0);
x_49 = lean_ctor_get(x_32, 1);
lean_inc(x_49);
lean_object* x_47; lean_object* x_48; lean_object* x_49; uint8_t x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54;
x_47 = lean_ctor_get(x_31, 0);
x_48 = lean_ctor_get(x_31, 1);
lean_inc(x_48);
lean_dec(x_32);
x_50 = lean_erase_macro_scopes(x_33);
x_51 = 1;
x_52 = l_Lean_Name_toString(x_50, x_51);
x_53 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_53, 0, x_52);
x_54 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_54, 0, x_27);
lean_inc(x_47);
lean_dec(x_31);
x_49 = lean_erase_macro_scopes(x_32);
x_50 = 1;
x_51 = l_Lean_Name_toString(x_49, x_50);
x_52 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_52, 0, x_51);
x_53 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_53, 0, x_26);
lean_ctor_set(x_53, 1, x_47);
lean_ctor_set(x_53, 2, x_52);
x_54 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_54, 0, x_53);
lean_ctor_set(x_54, 1, x_48);
lean_ctor_set(x_54, 2, x_53);
x_55 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_55, 0, x_54);
lean_ctor_set(x_55, 1, x_49);
return x_55;
return x_54;
}
}
}
else
{
uint8_t x_56;
lean_dec(x_27);
lean_dec(x_4);
x_56 = !lean_is_exclusive(x_32);
if (x_56 == 0)
{
return x_32;
}
else
{
lean_object* x_57; lean_object* x_58; lean_object* x_59;
x_57 = lean_ctor_get(x_32, 0);
x_58 = lean_ctor_get(x_32, 1);
lean_inc(x_58);
lean_inc(x_57);
lean_dec(x_32);
x_59 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_59, 0, x_57);
lean_ctor_set(x_59, 1, x_58);
return x_59;
}
}
}
else
{
uint8_t x_60;
lean_dec(x_27);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_4);
x_60 = !lean_is_exclusive(x_29);
if (x_60 == 0)
{
return x_29;
}
else
{
lean_object* x_61; lean_object* x_62; lean_object* x_63;
x_61 = lean_ctor_get(x_29, 0);
x_62 = lean_ctor_get(x_29, 1);
lean_inc(x_62);
lean_inc(x_61);
lean_dec(x_29);
x_63 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_63, 0, x_61);
lean_ctor_set(x_63, 1, x_62);
return x_63;
}
}
}
else
{
uint8_t x_64;
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_4);
x_64 = !lean_is_exclusive(x_26);
if (x_64 == 0)
{
return x_26;
}
else
{
lean_object* x_65; lean_object* x_66; lean_object* x_67;
x_65 = lean_ctor_get(x_26, 0);
x_66 = lean_ctor_get(x_26, 1);
lean_inc(x_66);
lean_inc(x_65);
uint8_t x_55;
lean_dec(x_26);
x_67 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_67, 0, x_65);
lean_ctor_set(x_67, 1, x_66);
return x_67;
}
}
}
else
{
uint8_t x_68;
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_4);
x_68 = !lean_is_exclusive(x_19);
if (x_68 == 0)
x_55 = !lean_is_exclusive(x_31);
if (x_55 == 0)
{
return x_19;
return x_31;
}
else
{
lean_object* x_69; lean_object* x_70; lean_object* x_71;
x_69 = lean_ctor_get(x_19, 0);
x_70 = lean_ctor_get(x_19, 1);
lean_inc(x_70);
lean_inc(x_69);
lean_dec(x_19);
x_71 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_71, 0, x_69);
lean_ctor_set(x_71, 1, x_70);
return x_71;
lean_object* x_56; lean_object* x_57; lean_object* x_58;
x_56 = lean_ctor_get(x_31, 0);
x_57 = lean_ctor_get(x_31, 1);
lean_inc(x_57);
lean_inc(x_56);
lean_dec(x_31);
x_58 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_58, 0, x_56);
lean_ctor_set(x_58, 1, x_57);
return x_58;
}
}
}
else
{
uint8_t x_72;
lean_dec(x_9);
uint8_t x_59;
lean_dec(x_26);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
x_59 = !lean_is_exclusive(x_28);
if (x_59 == 0)
{
return x_28;
}
else
{
lean_object* x_60; lean_object* x_61; lean_object* x_62;
x_60 = lean_ctor_get(x_28, 0);
x_61 = lean_ctor_get(x_28, 1);
lean_inc(x_61);
lean_inc(x_60);
lean_dec(x_28);
x_62 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_62, 0, x_60);
lean_ctor_set(x_62, 1, x_61);
return x_62;
}
}
}
else
{
uint8_t x_63;
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_1);
x_63 = !lean_is_exclusive(x_25);
if (x_63 == 0)
{
return x_25;
}
else
{
lean_object* x_64; lean_object* x_65; lean_object* x_66;
x_64 = lean_ctor_get(x_25, 0);
x_65 = lean_ctor_get(x_25, 1);
lean_inc(x_65);
lean_inc(x_64);
lean_dec(x_25);
x_66 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_66, 0, x_64);
lean_ctor_set(x_66, 1, x_65);
return x_66;
}
}
}
else
{
uint8_t x_67;
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_1);
x_67 = !lean_is_exclusive(x_18);
if (x_67 == 0)
{
return x_18;
}
else
{
lean_object* x_68; lean_object* x_69; lean_object* x_70;
x_68 = lean_ctor_get(x_18, 0);
x_69 = lean_ctor_get(x_18, 1);
lean_inc(x_69);
lean_inc(x_68);
lean_dec(x_18);
x_70 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_70, 0, x_68);
lean_ctor_set(x_70, 1, x_69);
return x_70;
}
}
}
else
{
uint8_t x_71;
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_72 = !lean_is_exclusive(x_11);
if (x_72 == 0)
lean_dec(x_1);
x_71 = !lean_is_exclusive(x_10);
if (x_71 == 0)
{
return x_11;
return x_10;
}
else
{
lean_object* x_73; lean_object* x_74; lean_object* x_75;
x_73 = lean_ctor_get(x_11, 0);
x_74 = lean_ctor_get(x_11, 1);
lean_inc(x_74);
lean_object* x_72; lean_object* x_73; lean_object* x_74;
x_72 = lean_ctor_get(x_10, 0);
x_73 = lean_ctor_get(x_10, 1);
lean_inc(x_73);
lean_dec(x_11);
x_75 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_75, 0, x_73);
lean_ctor_set(x_75, 1, x_74);
return x_75;
lean_inc(x_72);
lean_dec(x_10);
x_74 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_74, 0, x_72);
lean_ctor_set(x_74, 1, x_73);
return x_74;
}
}
}
@ -22637,82 +22638,80 @@ x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
lean_object* l_Lean_Widget_goalToInteractive(lean_object* x_1, uint8_t x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
lean_object* l_Lean_Widget_goalToInteractive(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_8 = lean_st_ref_get(x_6, x_7);
x_9 = lean_ctor_get(x_8, 1);
lean_inc(x_9);
lean_dec(x_8);
x_10 = lean_st_ref_get(x_4, x_9);
x_11 = lean_ctor_get(x_10, 0);
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_7 = lean_st_ref_get(x_5, x_6);
x_8 = lean_ctor_get(x_7, 1);
lean_inc(x_8);
lean_dec(x_7);
x_9 = lean_st_ref_get(x_3, x_8);
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_9, 1);
lean_inc(x_11);
x_12 = lean_ctor_get(x_10, 1);
lean_dec(x_9);
x_12 = lean_ctor_get(x_10, 0);
lean_inc(x_12);
lean_dec(x_10);
x_13 = lean_ctor_get(x_11, 0);
lean_inc(x_13);
lean_dec(x_11);
lean_inc(x_1);
x_14 = l_Lean_MetavarContext_findDecl_x3f(x_13, x_1);
if (lean_obj_tag(x_14) == 0)
x_13 = l_Lean_MetavarContext_findDecl_x3f(x_12, x_1);
if (lean_obj_tag(x_13) == 0)
{
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
x_15 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_15, 0, x_1);
x_16 = l_Lean_Widget_goalToInteractive___closed__2;
x_17 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set(x_17, 1, x_15);
x_18 = l_Lean_Widget_goalToInteractive___closed__3;
x_19 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_19, 0, x_17);
lean_ctor_set(x_19, 1, x_18);
x_20 = l_Lean_throwError___at_Lean_Widget_goalToInteractive___spec__1(x_19, x_3, x_4, x_5, x_6, x_12);
lean_dec(x_6);
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_14 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_14, 0, x_1);
x_15 = l_Lean_Widget_goalToInteractive___closed__2;
x_16 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_16, 0, x_15);
lean_ctor_set(x_16, 1, x_14);
x_17 = l_Lean_Widget_goalToInteractive___closed__3;
x_18 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_18, 0, x_16);
lean_ctor_set(x_18, 1, x_17);
x_19 = l_Lean_throwError___at_Lean_Widget_goalToInteractive___spec__1(x_18, x_2, x_3, x_4, x_5, x_11);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
return x_20;
lean_dec(x_2);
return x_19;
}
else
{
lean_object* x_21; lean_object* x_22; lean_object* x_23; uint8_t x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35;
lean_object* x_20; lean_object* x_21; lean_object* x_22; uint8_t x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33;
lean_dec(x_1);
x_21 = lean_ctor_get(x_14, 0);
x_20 = lean_ctor_get(x_13, 0);
lean_inc(x_20);
lean_dec(x_13);
x_21 = lean_ctor_get(x_4, 0);
lean_inc(x_21);
lean_dec(x_14);
x_22 = lean_ctor_get(x_5, 0);
lean_inc(x_22);
x_23 = l_Lean_Meta_pp_auxDecls;
x_24 = l_Lean_Option_get___at_Lean_ppExpr___spec__1(x_22, x_23);
x_25 = lean_ctor_get(x_21, 1);
lean_inc(x_25);
x_26 = lean_box(0);
x_27 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_27, 0, x_22);
lean_ctor_set(x_27, 1, x_26);
lean_ctor_set(x_27, 2, x_26);
x_28 = l_Lean_LocalContext_sanitizeNames(x_25, x_27);
x_29 = lean_ctor_get(x_28, 0);
x_22 = l_Lean_Meta_pp_auxDecls;
x_23 = l_Lean_Option_get___at_Lean_ppExpr___spec__1(x_21, x_22);
x_24 = lean_ctor_get(x_20, 1);
lean_inc(x_24);
x_25 = lean_box(0);
x_26 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_26, 0, x_21);
lean_ctor_set(x_26, 1, x_25);
lean_ctor_set(x_26, 2, x_25);
x_27 = l_Lean_LocalContext_sanitizeNames(x_24, x_26);
x_28 = lean_ctor_get(x_27, 0);
lean_inc(x_28);
lean_dec(x_27);
x_29 = lean_ctor_get(x_20, 4);
lean_inc(x_29);
lean_dec(x_28);
x_30 = lean_ctor_get(x_21, 4);
x_30 = lean_ctor_get(x_20, 2);
lean_inc(x_30);
x_31 = lean_ctor_get(x_21, 2);
lean_inc(x_31);
x_32 = lean_box(x_24);
x_33 = lean_box(x_2);
lean_inc(x_29);
x_34 = lean_alloc_closure((void*)(l_Lean_Widget_goalToInteractive___lambda__1___boxed), 10, 5);
lean_closure_set(x_34, 0, x_31);
lean_closure_set(x_34, 1, x_32);
lean_closure_set(x_34, 2, x_29);
lean_closure_set(x_34, 3, x_21);
lean_closure_set(x_34, 4, x_33);
x_35 = l_Lean_Meta_withLCtx___at___private_Lean_Meta_LevelDefEq_0__Lean_Meta_mkLeveErrorMessageCore___spec__1___rarg(x_29, x_30, x_34, x_3, x_4, x_5, x_6, x_12);
return x_35;
x_31 = lean_box(x_23);
lean_inc(x_28);
x_32 = lean_alloc_closure((void*)(l_Lean_Widget_goalToInteractive___lambda__1___boxed), 9, 4);
lean_closure_set(x_32, 0, x_30);
lean_closure_set(x_32, 1, x_31);
lean_closure_set(x_32, 2, x_28);
lean_closure_set(x_32, 3, x_20);
x_33 = l_Lean_Meta_withLCtx___at___private_Lean_Meta_LevelDefEq_0__Lean_Meta_mkLeveErrorMessageCore___spec__1___rarg(x_28, x_29, x_32, x_2, x_3, x_4, x_5, x_11);
return x_33;
}
}
}
@ -22946,26 +22945,14 @@ lean_dec(x_2);
return x_13;
}
}
lean_object* l_Lean_Widget_goalToInteractive___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
lean_object* l_Lean_Widget_goalToInteractive___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
_start:
{
uint8_t x_11; uint8_t x_12; lean_object* x_13;
x_11 = lean_unbox(x_2);
uint8_t x_10; lean_object* x_11;
x_10 = lean_unbox(x_2);
lean_dec(x_2);
x_12 = lean_unbox(x_5);
lean_dec(x_5);
x_13 = l_Lean_Widget_goalToInteractive___lambda__1(x_1, x_11, x_3, x_4, x_12, x_6, x_7, x_8, x_9, x_10);
return x_13;
}
}
lean_object* l_Lean_Widget_goalToInteractive___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
uint8_t x_8; lean_object* x_9;
x_8 = lean_unbox(x_2);
lean_dec(x_2);
x_9 = l_Lean_Widget_goalToInteractive(x_1, x_8, x_3, x_4, x_5, x_6, x_7);
return x_9;
x_11 = l_Lean_Widget_goalToInteractive___lambda__1(x_1, x_10, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
return x_11;
}
}
lean_object* initialize_Init(lean_object*);