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-01-13 18:43:16 -08:00
parent e5b93783b0
commit 5c91b395d6
43 changed files with 547 additions and 592 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
stage0/src/Init/Coe.lean generated
View file

@ -63,19 +63,19 @@ abbrev coeFun {α : Sort u} {γ : α → Sort v} (a : α) [CoeFun α γ] : γ a
abbrev coeSort {α : Sort u} {β : Sort v} (a : α) [CoeSort α β] : β :=
CoeSort.coe a
instance coeTrans {α : Sort u} {β : Sort v} {δ : Sort w} [CoeTC α β] [Coe β δ] : CoeTC α δ where
instance coeTrans {α : Sort u} {β : Sort v} {δ : Sort w} [Coe β δ] [CoeTC α β] : CoeTC α δ where
coe a := coeB (coeTC a : β)
instance coeBase {α : Sort u} {β : Sort v} [Coe α β] : CoeTC α β where
coe a := coeB a
instance coeOfHeafOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} {γ : Sort w'} (a : α) [CoeTC β δ] [CoeTail δ γ] [CoeHead α β] : CoeT α a γ where
instance coeOfHeafOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} {γ : Sort w'} (a : α) [CoeHead α β] [CoeTail δ γ] [CoeTC β δ] : CoeT α a γ where
coe := coeTail (coeTC (coeHead a : β) : δ)
instance coeOfHeadOfTC {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTC β δ] [CoeHead α β] : CoeT α a δ where
instance coeOfHeadOfTC {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeHead α β] [CoeTC β δ] : CoeT α a δ where
coe := coeTC (coeHead a : β)
instance coeOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTC α β] [CoeTail β δ] : CoeT α a δ where
instance coeOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTail β δ] [CoeTC α β] : CoeT α a δ where
coe := coeTail (coeTC a : β)
instance coeOfHead {α : Sort u} {β : Sort v} (a : α) [CoeHead α β] : CoeT α a β where
@ -116,7 +116,7 @@ instance subtypeCoe {α : Sort u} {p : α → Prop} : CoeHead { x // p x } α wh
Remark: one may question why we use `OfNat α` instead of `Coe Nat α`.
Reason: `OfNat` is for implementing polymorphic numeric literals, and we may
want to have numberic literals for a type α and **no** coercion from `Nat` to `α`. -/
instance hasOfNatOfCoe [OfNat α n] [Coe α β] : OfNat β n where
instance hasOfNatOfCoe [Coe α β] [OfNat α n] : OfNat β n where
ofNat := coe (OfNat.ofNat n : α)
@[inline] def liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α β : Type u} [MonadLiftT m n] [∀ a, CoeT α a β] [Monad n] (x : m α) : n β := do

2
stage0/src/Init/Control/Basic.lean generated
View file

@ -86,7 +86,7 @@ class MonadControlT (m : Type u → Type v) (n : Type u → Type w) where
export MonadControlT (stM liftWith restoreM)
instance (m n o) [MonadControlT m n] [MonadControl n o] : MonadControlT m o where
instance (m n o) [MonadControl n o] [MonadControlT m n] : MonadControlT m o where
stM α := stM m n (MonadControl.stM n o α)
liftWith f := MonadControl.liftWith fun x₂ => liftWith fun x₁ => f (x₁ ∘ x₂)
restoreM := MonadControl.restoreM ∘ restoreM

2
stage0/src/Init/Control/Reader.lean generated
View file

@ -18,7 +18,7 @@ namespace ReaderT
@[inline] protected def failure [Alternative m] : ReaderT ρ m α :=
fun s => failure
instance [Monad m] [Alternative m] : Alternative (ReaderT ρ m) where
instance [Alternative m] [Monad m] : Alternative (ReaderT ρ m) where
failure := ReaderT.failure
orElse := ReaderT.orElse

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

@ -135,7 +135,7 @@ def mkFreshId {m : Type → Type} [Monad m] [MonadNameGenerator m] : m Name := d
setNGen ngen.next
pure r
instance monadNameGeneratorLift (m n : Type → Type) [MonadNameGenerator m] [MonadLift m n] : MonadNameGenerator n := {
instance monadNameGeneratorLift (m n : Type → Type) [MonadLift m n] [MonadNameGenerator m] : MonadNameGenerator n := {
getNGen := liftM (getNGen : m _),
setNGen := fun ngen => liftM (setNGen ngen : m _)
}

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

@ -1176,7 +1176,7 @@ export MonadLiftT (monadLift)
abbrev liftM := @monadLift
instance (m n o) [MonadLiftT m n] [MonadLift n o] : MonadLiftT m o where
instance (m n o) [MonadLift n o] [MonadLiftT m n] : MonadLiftT m o where
monadLift x := MonadLift.monadLift (m := n) (monadLift x)
instance (m) : MonadLiftT m m where
@ -1196,7 +1196,7 @@ class MonadFunctorT (m : Type u → Type v) (n : Type u → Type w) where
export MonadFunctorT (monadMap)
instance (m n o) [MonadFunctorT m n] [MonadFunctor n o] : MonadFunctorT m o where
instance (m n o) [MonadFunctor n o] [MonadFunctorT m n] : MonadFunctorT m o where
monadMap f := MonadFunctor.monadMap (m := n) (monadMap (m := m) f)
instance monadFunctorRefl (m) : MonadFunctorT m m where
@ -1324,7 +1324,7 @@ export MonadReader (read)
instance (ρ : Type u) (m : Type u → Type v) [MonadReaderOf ρ m] : MonadReader ρ m where
read := readThe ρ
instance {ρ : Type u} {m : Type u → Type v} {n : Type u → Type w} [MonadReaderOf ρ m] [MonadLift m n] : MonadReaderOf ρ n where
instance {ρ : Type u} {m : Type u → Type v} {n : Type u → Type w} [MonadLift m n] [MonadReaderOf ρ m] : MonadReaderOf ρ n where
read := liftM (m := m) read
instance {ρ : Type u} {m : Type u → Type v} [Monad m] : MonadReaderOf ρ (ReaderT ρ m) where
@ -1344,7 +1344,7 @@ export MonadWithReader (withReader)
instance (ρ : Type u) (m : Type u → Type v) [MonadWithReaderOf ρ m] : MonadWithReader ρ m where
withReader := withTheReader ρ
instance {ρ : Type u} {m : Type u → Type v} {n : Type u → Type v} [MonadWithReaderOf ρ m] [MonadFunctor m n] : MonadWithReaderOf ρ n where
instance {ρ : Type u} {m : Type u → Type v} {n : Type u → Type v} [MonadFunctor m n] [MonadWithReaderOf ρ m] : MonadWithReaderOf ρ n where
withReader f := monadMap (m := m) (withTheReader ρ f)
instance {ρ : Type u} {m : Type u → Type v} [Monad m] : MonadWithReaderOf ρ (ReaderT ρ m) where
@ -1396,7 +1396,7 @@ instance (σ : Type u) (m : Type u → Type v) [MonadStateOf σ m] : MonadState
-- NOTE: The Ordering of the following two instances determines that the top-most `StateT` Monad layer
-- will be picked first
instance {σ : Type u} {m : Type u → Type v} {n : Type u → Type w} [MonadStateOf σ m] [MonadLift m n] : MonadStateOf σ n where
instance {σ : Type u} {m : Type u → Type v} {n : Type u → Type w} [MonadLift m n] [MonadStateOf σ m] : MonadStateOf σ n where
get := liftM (m := m) MonadStateOf.get
set := fun s => liftM (m := m) (MonadStateOf.set s)
modifyGet := fun f => monadLift (m := m) (MonadState.modifyGet f)
@ -1742,7 +1742,7 @@ class MonadRef (m : Type → Type) where
export MonadRef (getRef)
instance (m n : Type → Type) [MonadRef m] [MonadFunctor m n] [MonadLift m n] : MonadRef n where
instance (m n : Type → Type) [MonadLift m n] [MonadFunctor m n] [MonadRef m] : MonadRef n where
getRef := liftM (getRef : m _)
withRef := fun ref x => monadMap (m := m) (MonadRef.withRef ref) x
@ -1786,7 +1786,7 @@ export MonadQuotation (getCurrMacroScope getMainModule withFreshMacroScope)
def MonadRef.mkInfoFromRefPos [Monad m] [MonadRef m] : m SourceInfo := do
return { pos := (← getRef).getPos }
instance {m n : Type → Type} [MonadQuotation m] [MonadLift m n] [MonadFunctor m n] : MonadQuotation n where
instance {m n : Type → Type} [MonadFunctor m n] [MonadLift m n] [MonadQuotation m] : MonadQuotation n where
getCurrMacroScope := liftM (m := m) getCurrMacroScope
getMainModule := liftM (m := m) getMainModule
withFreshMacroScope := monadMap (m := m) withFreshMacroScope

2
stage0/src/Init/System/ST.lean generated
View file

@ -19,7 +19,7 @@ instance (σ : Type) : Monad (ST σ) := inferInstanceAs (Monad (EST _ _))
-- Auxiliary class for inferring the "state" of `EST` and `ST` monads
class STWorld (σ : outParam Type) (m : Type → Type)
instance {σ m n} [STWorld σ m] [MonadLift m n] : STWorld σ n := ⟨⟩
instance {σ m n} [MonadLift m n] [STWorld σ m] : STWorld σ n := ⟨⟩
instance {ε σ} : STWorld σ (EST ε σ) := ⟨⟩
@[noinline, nospecialize]

4
stage0/src/Lean/Data/Options.lean generated
View file

@ -102,8 +102,8 @@ class MonadOptions (m : Type → Type) where
export MonadOptions (getOptions)
instance (m n) [MonadOptions m] [MonadLift m n] : MonadOptions n :=
{ getOptions := liftM (getOptions : m _) }
instance (m n) [MonadLift m n] [MonadOptions m] : MonadOptions n where
getOptions := liftM (getOptions : m _)
variables {m} [Monad m] [MonadOptions m]

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

@ -74,7 +74,7 @@ class MonadInfoTree (m : Type → Type) where
export MonadInfoTree (getInfoState modifyInfoState)
instance (m n) [MonadInfoTree m] [MonadLift m n] : MonadInfoTree n where
instance (m n) [MonadLift m n] [MonadInfoTree m] : MonadInfoTree n where
getInfoState := liftM (getInfoState : m _)
modifyInfoState f := liftM (modifyInfoState f : m _)

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

@ -21,12 +21,11 @@ class MonadLog (m : Type → Type) extends MonadFileMap m where
export MonadLog (getFileName logMessage)
instance (m n) [MonadLog m] [MonadLift m n] : MonadLog n := {
getRef := liftM (MonadLog.getRef : m _),
getFileMap := liftM (getFileMap : m _),
getFileName := liftM (getFileName : m _),
instance (m n) [MonadLift m n] [MonadLog m] : MonadLog n where
getRef := liftM (MonadLog.getRef : m _)
getFileMap := liftM (getFileMap : m _)
getFileName := liftM (getFileName : m _)
logMessage := fun msg => liftM (logMessage msg : m _ )
}
variables {m : Type → Type} [Monad m] [MonadLog m] [AddMessageContext m]

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

@ -141,7 +141,7 @@ class MonadMacroAdapter (m : Type → Type) where
getNextMacroScope : m MacroScope
setNextMacroScope : MacroScope → m Unit
instance (m n) [MonadMacroAdapter m] [MonadLift m n] : MonadMacroAdapter n := {
instance (m n) [MonadLift m n] [MonadMacroAdapter m] : MonadMacroAdapter n := {
getCurrMacroScope := liftM (MonadMacroAdapter.getCurrMacroScope : m _),
getNextMacroScope := liftM (MonadMacroAdapter.getNextMacroScope : m _),
setNextMacroScope := fun s => liftM (MonadMacroAdapter.setNextMacroScope s : m _)

5
stage0/src/Lean/Environment.lean generated
View file

@ -703,9 +703,8 @@ class MonadEnv (m : Type → Type) where
export MonadEnv (getEnv modifyEnv)
instance (m n) [MonadEnv m] [MonadLift m n] : MonadEnv n := {
getEnv := liftM (getEnv : m Environment),
instance (m n) [MonadLift m n] [MonadEnv m] : MonadEnv n where
getEnv := liftM (getEnv : m Environment)
modifyEnv := fun f => liftM (modifyEnv f : m Unit)
}
end Lean

2
stage0/src/Lean/LocalContext.lean generated
View file

@ -383,7 +383,7 @@ class MonadLCtx (m : Type → Type) where
export MonadLCtx (getLCtx)
instance (m n) [MonadLCtx m] [MonadLift m n] : MonadLCtx n where
instance (m n) [MonadLift m n] [MonadLCtx m] : MonadLCtx n where
getLCtx := liftM (getLCtx : m _)
def replaceFVarIdAtLocalDecl (fvarId : FVarId) (e : Expr) (d : LocalDecl) : LocalDecl :=

4
stage0/src/Lean/Message.lean generated
View file

@ -215,8 +215,8 @@ class AddMessageContext (m : Type → Type) where
export AddMessageContext (addMessageContext)
instance (m n) [AddMessageContext m] [MonadLift m n] : AddMessageContext n :=
{ addMessageContext := fun msg => liftM (addMessageContext msg : m _) }
instance (m n) [MonadLift m n] [AddMessageContext m] : AddMessageContext n where
addMessageContext := fun msg => liftM (addMessageContext msg : m _)
def addMessageContextPartial {m} [Monad m] [MonadEnv m] [MonadOptions m] (msgData : MessageData) : m MessageData := do
let env ← getEnv

2
stage0/src/Lean/MetavarContext.lean generated
View file

@ -290,7 +290,7 @@ class MonadMCtx (m : Type → Type) where
export MonadMCtx (getMCtx modifyMCtx)
instance (m n) [MonadMCtx m] [MonadLift m n] : MonadMCtx n where
instance (m n) [MonadLift m n] [MonadMCtx m] : MonadMCtx n where
getMCtx := liftM (getMCtx : m _)
modifyMCtx := fun f => liftM (modifyMCtx f : m _)

2
stage0/src/Lean/ResolveName.lean generated
View file

@ -151,7 +151,7 @@ class MonadResolveName (m : Type → Type) where
export MonadResolveName (getCurrNamespace getOpenDecls)
instance (m n) [MonadResolveName m] [MonadLift m n] : MonadResolveName n where
instance (m n) [MonadLift m n] [MonadResolveName m] : MonadResolveName n where
getCurrNamespace := liftM (m:=m) getCurrNamespace
getOpenDecls := liftM (m:=m) getOpenDecls

6
stage0/src/Lean/Util/Trace.lean generated
View file

@ -38,9 +38,9 @@ class MonadTrace (m : Type → Type) where
export MonadTrace (getTraceState modifyTraceState)
instance (m n) [MonadTrace m] [MonadLift m n] : MonadTrace n :=
{ modifyTraceState := fun f => liftM (modifyTraceState f : m _),
getTraceState := liftM (getTraceState : m _) }
instance (m n) [MonadLift m n] [MonadTrace m] : MonadTrace n where
modifyTraceState := fun f => liftM (modifyTraceState f : m _)
getTraceState := liftM (getTraceState : m _)
variables {α : Type} {m : Type → Type} [Monad m] [MonadTrace m]

20
stage0/stdlib/Init/Coe.c generated
View file

@ -642,8 +642,8 @@ lean_object* l_coeTrans___rarg(lean_object* x_1, lean_object* x_2, lean_object*
_start:
{
lean_object* x_4; lean_object* x_5;
x_4 = lean_apply_1(x_1, x_3);
x_5 = lean_apply_1(x_2, x_4);
x_4 = lean_apply_1(x_2, x_3);
x_5 = lean_apply_1(x_1, x_4);
return x_5;
}
}
@ -676,8 +676,8 @@ lean_object* l_coeOfHeafOfTCOfTail___rarg(lean_object* x_1, lean_object* x_2, le
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_5 = lean_apply_1(x_4, x_1);
x_6 = lean_apply_1(x_2, x_5);
x_5 = lean_apply_1(x_2, x_1);
x_6 = lean_apply_1(x_4, x_5);
x_7 = lean_apply_1(x_3, x_6);
return x_7;
}
@ -694,8 +694,8 @@ lean_object* l_coeOfHeadOfTC___rarg(lean_object* x_1, lean_object* x_2, lean_obj
_start:
{
lean_object* x_4; lean_object* x_5;
x_4 = lean_apply_1(x_3, x_1);
x_5 = lean_apply_1(x_2, x_4);
x_4 = lean_apply_1(x_2, x_1);
x_5 = lean_apply_1(x_3, x_4);
return x_5;
}
}
@ -711,8 +711,8 @@ lean_object* l_coeOfTCOfTail___rarg(lean_object* x_1, lean_object* x_2, lean_obj
_start:
{
lean_object* x_4; lean_object* x_5;
x_4 = lean_apply_1(x_2, x_1);
x_5 = lean_apply_1(x_3, x_4);
x_4 = lean_apply_1(x_3, x_1);
x_5 = lean_apply_1(x_2, x_4);
return x_5;
}
}
@ -922,7 +922,7 @@ lean_object* l_hasOfNatOfCoe___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_apply_1(x_2, x_1);
x_3 = lean_apply_1(x_1, x_2);
return x_3;
}
}
@ -939,7 +939,7 @@ _start:
{
lean_object* x_4;
x_4 = l_hasOfNatOfCoe(x_1, x_2, x_3);
lean_dec(x_2);
lean_dec(x_3);
return x_4;
}
}

10
stage0/stdlib/Init/Control/Basic.c generated
View file

@ -1841,14 +1841,14 @@ lean_object* l_instMonadControlT___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
lean_inc(x_1);
lean_inc(x_2);
lean_inc(x_1);
x_3 = lean_alloc_closure((void*)(l_instMonadControlT___rarg___lambda__4), 4, 2);
lean_closure_set(x_3, 0, x_2);
lean_closure_set(x_3, 1, x_1);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
x_4 = lean_alloc_closure((void*)(l_instMonadControlT___rarg___lambda__5), 4, 2);
lean_closure_set(x_4, 0, x_2);
lean_closure_set(x_4, 1, x_1);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
x_5 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_5, 0, x_3);
lean_ctor_set(x_5, 1, x_4);

8
stage0/stdlib/Init/Control/Reader.c generated
View file

@ -113,15 +113,15 @@ lean_object* l_ReaderT_instAlternativeReaderT___rarg(lean_object* x_1, lean_obje
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_3 = l_ReaderT_instMonadReaderT___rarg(x_1);
x_3 = l_ReaderT_instMonadReaderT___rarg(x_2);
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
lean_dec(x_3);
lean_inc(x_2);
lean_inc(x_1);
x_5 = lean_alloc_closure((void*)(l_ReaderT_instAlternativeReaderT___rarg___lambda__1___boxed), 3, 1);
lean_closure_set(x_5, 0, x_2);
lean_closure_set(x_5, 0, x_1);
x_6 = lean_alloc_closure((void*)(l_ReaderT_instAlternativeReaderT___rarg___lambda__2), 5, 1);
lean_closure_set(x_6, 0, x_2);
lean_closure_set(x_6, 0, x_1);
x_7 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_7, 0, x_4);
lean_ctor_set(x_7, 1, x_5);

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

@ -2170,13 +2170,13 @@ lean_object* l_Lean_monadNameGeneratorLift___rarg(lean_object* x_1, lean_object*
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_3 = lean_ctor_get(x_1, 0);
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
lean_inc(x_2);
x_4 = lean_apply_2(x_2, lean_box(0), x_3);
lean_inc(x_1);
x_4 = lean_apply_2(x_1, lean_box(0), x_3);
x_5 = lean_alloc_closure((void*)(l_Lean_monadNameGeneratorLift___rarg___lambda__1), 3, 2);
lean_closure_set(x_5, 0, x_1);
lean_closure_set(x_5, 1, x_2);
lean_closure_set(x_5, 0, x_2);
lean_closure_set(x_5, 1, x_1);
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_4);
lean_ctor_set(x_6, 1, x_5);

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

@ -5349,8 +5349,8 @@ lean_object* l_instMonadLiftT___rarg(lean_object* x_1, lean_object* x_2, lean_ob
_start:
{
lean_object* x_5; lean_object* x_6;
x_5 = lean_apply_2(x_1, lean_box(0), x_4);
x_6 = lean_apply_2(x_2, lean_box(0), x_5);
x_5 = lean_apply_2(x_2, lean_box(0), x_4);
x_6 = lean_apply_2(x_1, lean_box(0), x_5);
return x_6;
}
}
@ -5410,8 +5410,8 @@ _start:
lean_object* x_6; lean_object* x_7;
x_6 = lean_alloc_closure((void*)(l_instMonadFunctorT___rarg___lambda__2), 4, 2);
lean_closure_set(x_6, 0, x_4);
lean_closure_set(x_6, 1, x_1);
x_7 = lean_apply_3(x_2, lean_box(0), x_6, x_5);
lean_closure_set(x_6, 1, x_2);
x_7 = lean_apply_3(x_1, lean_box(0), x_6, x_5);
return x_7;
}
}
@ -6083,7 +6083,7 @@ lean_object* l_instMonadReaderOf___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_apply_2(x_2, lean_box(0), x_1);
x_3 = lean_apply_2(x_1, lean_box(0), x_2);
return x_3;
}
}
@ -6158,9 +6158,9 @@ _start:
{
lean_object* x_6; lean_object* x_7;
x_6 = lean_alloc_closure((void*)(l_instMonadWithReaderOf___rarg___lambda__1), 4, 2);
lean_closure_set(x_6, 0, x_1);
lean_closure_set(x_6, 0, x_2);
lean_closure_set(x_6, 1, x_4);
x_7 = lean_apply_3(x_2, lean_box(0), x_6, x_5);
x_7 = lean_apply_3(x_1, lean_box(0), x_6, x_5);
return x_7;
}
}
@ -6403,18 +6403,18 @@ lean_object* l_instMonadStateOf___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_3 = lean_ctor_get(x_1, 0);
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
lean_inc(x_2);
x_4 = lean_apply_2(x_2, lean_box(0), x_3);
lean_inc(x_2);
lean_inc(x_1);
x_4 = lean_apply_2(x_1, lean_box(0), x_3);
lean_inc(x_1);
lean_inc(x_2);
x_5 = lean_alloc_closure((void*)(l_instMonadStateOf___rarg___lambda__1), 3, 2);
lean_closure_set(x_5, 0, x_1);
lean_closure_set(x_5, 1, x_2);
lean_closure_set(x_5, 0, x_2);
lean_closure_set(x_5, 1, x_1);
x_6 = lean_alloc_closure((void*)(l_instMonadStateOf___rarg___lambda__2), 4, 2);
lean_closure_set(x_6, 0, x_1);
lean_closure_set(x_6, 1, x_2);
lean_closure_set(x_6, 0, x_2);
lean_closure_set(x_6, 1, x_1);
x_7 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_7, 0, x_4);
lean_ctor_set(x_7, 1, x_5);
@ -9556,11 +9556,11 @@ lean_object* l_Lean_instMonadRef___rarg(lean_object* x_1, lean_object* x_2, lean
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_4 = lean_ctor_get(x_1, 0);
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
x_5 = lean_apply_2(x_3, lean_box(0), x_4);
x_5 = lean_apply_2(x_1, lean_box(0), x_4);
x_6 = lean_alloc_closure((void*)(l_Lean_instMonadRef___rarg___lambda__2), 5, 2);
lean_closure_set(x_6, 0, x_1);
lean_closure_set(x_6, 0, x_3);
lean_closure_set(x_6, 1, x_2);
x_7 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_7, 0, x_5);
@ -9758,21 +9758,21 @@ lean_object* l_Lean_instMonadQuotation___rarg(lean_object* x_1, lean_object* x_2
_start:
{
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* x_11;
x_4 = lean_ctor_get(x_1, 0);
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
lean_inc(x_1);
lean_inc(x_2);
lean_inc(x_3);
x_5 = l_Lean_instMonadRef___rarg(x_4, x_3, x_2);
x_6 = lean_ctor_get(x_1, 1);
x_5 = l_Lean_instMonadRef___rarg(x_2, x_1, x_4);
x_6 = lean_ctor_get(x_3, 1);
lean_inc(x_6);
lean_inc(x_2);
x_7 = lean_apply_2(x_2, lean_box(0), x_6);
x_8 = lean_ctor_get(x_1, 2);
x_8 = lean_ctor_get(x_3, 2);
lean_inc(x_8);
x_9 = lean_apply_2(x_2, lean_box(0), x_8);
x_10 = lean_alloc_closure((void*)(l_Lean_instMonadQuotation___rarg___lambda__2), 4, 2);
lean_closure_set(x_10, 0, x_1);
lean_closure_set(x_10, 1, x_3);
lean_closure_set(x_10, 0, x_3);
lean_closure_set(x_10, 1, x_1);
x_11 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_11, 0, x_5);
lean_ctor_set(x_11, 1, x_7);

2
stage0/stdlib/Lean/Data/Options.c generated
View file

@ -1708,7 +1708,7 @@ lean_object* l_Lean_instMonadOptions___rarg(lean_object* x_1, lean_object* x_2)
_start:
{
lean_object* x_3;
x_3 = lean_apply_2(x_2, lean_box(0), x_1);
x_3 = lean_apply_2(x_1, lean_box(0), x_2);
return x_3;
}
}

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

@ -677,6 +677,7 @@ lean_object* l_Lean_findField_x3f(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_ElabAppArgs_hasOptAutoParams___closed__1;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_App_0__Lean_Elab_Term_mergeFailures___spec__1(size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_registerMVarErrorImplicitArgInfo(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_Elab_Term_instMonadQuotationTermElabM___closed__1;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_App_0__Lean_Elab_Term_mergeFailures___spec__1___closed__2;
lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_ElabAppArgs_propagateExpectedType___closed__8;
extern lean_object* l_prec_x28___x29___closed__3;
@ -710,7 +711,6 @@ lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_ElabAppArgs_propagateEx
lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_resolveLValAux_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_List_forIn_loop___at___private_Lean_Elab_App_0__Lean_Elab_Term_ElabAppArgs_synthesizePendingAndNormalizeFunType___spec__4(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___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppAux___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*);
extern lean_object* l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__5;
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
uint8_t l_List_isEmpty___rarg(lean_object*);
lean_object* l_List_lengthAux___rarg(lean_object*, lean_object*);
@ -22322,7 +22322,7 @@ static lean_object* _init_l___private_Lean_Elab_App_0__Lean_Elab_Term_addLValArg
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__5;
x_1 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__1;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = lean_ctor_get(x_2, 1);
@ -22336,8 +22336,8 @@ static lean_object* _init_l___private_Lean_Elab_App_0__Lean_Elab_Term_addLValArg
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Elab_App_0__Lean_Elab_Term_addLValArg___closed__1;
x_2 = l_instMonadControlReaderT___closed__2;
x_1 = l_instMonadControlReaderT___closed__2;
x_2 = l___private_Lean_Elab_App_0__Lean_Elab_Term_addLValArg___closed__1;
x_3 = l_instMonadControlT___rarg(x_1, x_2);
return x_3;
}
@ -22346,9 +22346,9 @@ lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_addLValArg(lean_object*
_start:
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18;
x_14 = l___private_Lean_Elab_App_0__Lean_Elab_Term_addLValArg___closed__1;
x_15 = l___private_Lean_Elab_App_0__Lean_Elab_Term_addLValArg___closed__2;
x_16 = l_instMonadControlReaderT___closed__2;
x_14 = l_instMonadControlReaderT___closed__2;
x_15 = l___private_Lean_Elab_App_0__Lean_Elab_Term_addLValArg___closed__1;
x_16 = l___private_Lean_Elab_App_0__Lean_Elab_Term_addLValArg___closed__2;
x_17 = lean_alloc_closure((void*)(l___private_Lean_Elab_App_0__Lean_Elab_Term_addLValArg___lambda__2___boxed), 17, 8);
lean_closure_set(x_17, 0, x_5);
lean_closure_set(x_17, 1, x_1);

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

@ -55,7 +55,6 @@ extern lean_object* l_Lean_Parser_Term_letEqnsDecl___closed__2;
lean_object* l_Lean_Elab_Term_elabArrow___closed__1;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_12458____closed__7;
lean_object* lean_array_uget(lean_object*, size_t);
extern lean_object* l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__8;
lean_object* l_Lean_Elab_Term_declareTacticSyntax___closed__5;
lean_object* l_Lean_Elab_Term_elabLetDeclAux_match__1(lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_elabDepArrow___closed__1;
@ -451,6 +450,7 @@ lean_object* l_ReaderT_instMonadReaderT___rarg(lean_object*);
lean_object* l_Lean_Elab_Term_quoteAutoTactic___closed__17;
lean_object* l_Lean_Elab_Term_elabLetDeclAux___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_prec_x28___x29___closed__3;
extern lean_object* l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__2;
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
extern lean_object* l_Lean_mkOptionalNode___closed__2;
lean_object* l_Lean_Elab_Term_declareTacticSyntax___closed__4;
@ -1438,7 +1438,7 @@ static lean_object* _init_l_Lean_Elab_Term_quoteAutoTactic___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__8;
x_1 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__2;
x_2 = l_ReaderT_instMonadReaderT___rarg(x_1);
return x_2;
}

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

@ -489,13 +489,13 @@ lean_object* l_Lean_Elab_instMonadInfoTree___rarg(lean_object* x_1, lean_object*
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_3 = lean_ctor_get(x_1, 0);
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
lean_inc(x_2);
x_4 = lean_apply_2(x_2, lean_box(0), x_3);
lean_inc(x_1);
x_4 = lean_apply_2(x_1, lean_box(0), x_3);
x_5 = lean_alloc_closure((void*)(l_Lean_Elab_instMonadInfoTree___rarg___lambda__1), 3, 2);
lean_closure_set(x_5, 0, x_1);
lean_closure_set(x_5, 1, x_2);
lean_closure_set(x_5, 0, x_2);
lean_closure_set(x_5, 1, x_1);
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_4);
lean_ctor_set(x_6, 1, x_5);

22
stage0/stdlib/Lean/Elab/Log.c generated
View file

@ -120,21 +120,21 @@ lean_object* l_Lean_Elab_instMonadLog___rarg(lean_object* x_1, lean_object* x_2)
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_3 = lean_ctor_get(x_1, 0);
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
lean_inc(x_2);
x_4 = lean_apply_2(x_2, lean_box(0), x_3);
x_5 = lean_ctor_get(x_1, 1);
lean_inc(x_1);
x_4 = lean_apply_2(x_1, lean_box(0), x_3);
x_5 = lean_ctor_get(x_2, 1);
lean_inc(x_5);
lean_inc(x_2);
x_6 = lean_apply_2(x_2, lean_box(0), x_5);
x_7 = lean_ctor_get(x_1, 2);
lean_inc(x_1);
x_6 = lean_apply_2(x_1, lean_box(0), x_5);
x_7 = lean_ctor_get(x_2, 2);
lean_inc(x_7);
lean_inc(x_2);
x_8 = lean_apply_2(x_2, lean_box(0), x_7);
lean_inc(x_1);
x_8 = lean_apply_2(x_1, lean_box(0), x_7);
x_9 = lean_alloc_closure((void*)(l_Lean_Elab_instMonadLog___rarg___lambda__1), 3, 2);
lean_closure_set(x_9, 0, x_1);
lean_closure_set(x_9, 1, x_2);
lean_closure_set(x_9, 0, x_2);
lean_closure_set(x_9, 1, x_1);
x_10 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_10, 0, x_4);
lean_ctor_set(x_10, 1, x_6);

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

@ -715,6 +715,7 @@ lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_na
lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_CtorApp_finalize___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_CtorApp_pushNewArg___closed__2;
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_CtorApp_pushNewArg___closed__1;
extern lean_object* l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__1;
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_CtorApp_pushNewArg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkFreshTypeMVar(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_instMonadReaderT___rarg(lean_object*);
@ -757,7 +758,6 @@ extern lean_object* l_rawNatLit___closed__5;
extern lean_object* l_Lean_expandExplicitBindersAux_loop___closed__4;
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_withPatternVars_loop_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_5535____closed__3;
extern lean_object* l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__5;
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
uint8_t l_List_isEmpty___rarg(lean_object*);
lean_object* l_Lean_Elab_Term_ToDepElimPattern_main___lambda__1___boxed__const__1;
@ -1942,7 +1942,7 @@ x_13 = lean_array_get_size(x_1);
x_14 = lean_usize_of_nat(x_13);
lean_dec(x_13);
x_15 = 0;
x_16 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__5;
x_16 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__1;
lean_inc(x_1);
x_17 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabDiscrsWitMatchType___spec__1(x_1, x_16, x_1, x_14, x_15, x_12, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
if (lean_obj_tag(x_17) == 0)

6
stage0/stdlib/Lean/Elab/PreDefinition/Main.c generated
View file

@ -166,6 +166,7 @@ uint8_t l_Array_anyMUnsafe_any___at_Lean_Elab_addPreDefinitions___spec__4(lean_o
extern lean_object* l_Lean_Expr_FoldConstsImpl_initCache;
lean_object* l_Lean_Elab_WFRecursion___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_indentD(lean_object*);
extern lean_object* l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__1;
lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_sccAux___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__9___lambda__1(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*);
lean_object* l_Lean_Expr_FindImpl_findM_x3f_visit(lean_object*, size_t, lean_object*, lean_object*);
extern lean_object* l_Lean_CollectMVars_instInhabitedState___closed__1;
@ -177,7 +178,6 @@ lean_object* l___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_getMVarsAtPre
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__3(lean_object*, size_t, lean_object*, lean_object*, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__8___lambda__3___closed__1;
lean_object* l_List_forM___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__19(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__5;
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_isNonRecursive___boxed(lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___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*);
@ -630,7 +630,7 @@ x_9 = lean_array_get_size(x_1);
x_10 = lean_usize_of_nat(x_9);
lean_dec(x_9);
x_11 = 0;
x_12 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__5;
x_12 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__1;
x_13 = l_Lean_Elab_Term_quoteAutoTactic___closed__4;
x_14 = lean_box(0);
lean_inc(x_7);
@ -4343,7 +4343,7 @@ x_17 = l___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs(x_
x_18 = lean_array_get_size(x_17);
x_19 = lean_usize_of_nat(x_18);
lean_dec(x_18);
x_20 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__5;
x_20 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__1;
x_21 = l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__8(x_20, x_11, x_17, x_19, x_11, x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_16);
if (lean_obj_tag(x_21) == 0)
{

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

@ -469,7 +469,6 @@ lean_object* l_Lean_Elab_Term_elabProp___rarg(lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImplicitLambdaAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_logException___at___private_Lean_Elab_Term_0__Lean_Elab_Term_exceptionToSorry___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_isStrLit_x3f(lean_object*);
extern lean_object* l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__6;
lean_object* l_Lean_Elab_logAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_exceptionToSorry___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_mkTypeMismatchError___closed__1;
lean_object* l_Lean_Elab_Term_tryPostponeIfHasMVars_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -733,6 +732,7 @@ lean_object* l_Lean_Elab_Term_registerMVarErrorImplicitArgInfo___boxed(lean_obje
lean_object* l_Lean_Elab_Term_throwTypeMismatchError(lean_object*);
lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_elabSort(lean_object*);
extern lean_object* l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__1;
lean_object* l_Lean_Elab_Term_tryCoeThunk_x3f_match__1___rarg___closed__1;
lean_object* l_Lean_KVMap_getNat(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryLiftAndCoe___closed__2;
@ -3683,30 +3683,25 @@ static lean_object* _init_l_Lean_Elab_Term_instMonadQuotationTermElabM___closed_
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_PrettyPrinter_Formatter_symbolNoAntiquot_formatter___closed__1;
x_2 = lean_alloc_closure((void*)(l_ReaderT_instMonadFunctorReaderT___boxed), 4, 3);
lean_closure_set(x_2, 0, lean_box(0));
lean_closure_set(x_2, 1, lean_box(0));
lean_closure_set(x_2, 2, x_1);
x_1 = l_Lean_PrettyPrinter_Formatter_symbolNoAntiquot_formatter___closed__2;
x_2 = l_ReaderT_instMonadReaderT___rarg(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Core_instMonadRefCoreM;
x_2 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__1;
x_3 = l_StateRefT_x27_instMonadLiftStateRefT_x27___closed__1;
x_4 = l_Lean_instMonadRef___rarg(x_1, x_2, x_3);
return x_4;
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__1;
x_2 = l_ReaderT_instMonadReaderT___rarg(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_PrettyPrinter_Formatter_symbolNoAntiquot_formatter___closed__2;
x_1 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__2;
x_2 = lean_alloc_closure((void*)(l_ReaderT_instMonadFunctorReaderT___boxed), 4, 3);
lean_closure_set(x_2, 0, lean_box(0));
lean_closure_set(x_2, 1, lean_box(0));
@ -3717,12 +3712,13 @@ return x_2;
static lean_object* _init_l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__2;
x_2 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__3;
x_3 = l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__6;
x_4 = l_Lean_instMonadRef___rarg(x_1, x_2, x_3);
return x_4;
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__1;
x_2 = lean_alloc_closure((void*)(l_ReaderT_instMonadFunctorReaderT___boxed), 4, 3);
lean_closure_set(x_2, 0, lean_box(0));
lean_closure_set(x_2, 1, lean_box(0));
lean_closure_set(x_2, 2, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__5() {
@ -3730,7 +3726,10 @@ _start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_PrettyPrinter_Formatter_symbolNoAntiquot_formatter___closed__2;
x_2 = l_ReaderT_instMonadReaderT___rarg(x_1);
x_2 = lean_alloc_closure((void*)(l_ReaderT_instMonadFunctorReaderT___boxed), 4, 3);
lean_closure_set(x_2, 0, lean_box(0));
lean_closure_set(x_2, 1, lean_box(0));
lean_closure_set(x_2, 2, x_1);
return x_2;
}
}
@ -3738,7 +3737,7 @@ static lean_object* _init_l_Lean_Elab_Term_instMonadQuotationTermElabM___closed_
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__5;
x_1 = l_Lean_PrettyPrinter_Formatter_symbolNoAntiquot_formatter___closed__1;
x_2 = lean_alloc_closure((void*)(l_ReaderT_instMonadFunctorReaderT___boxed), 4, 3);
lean_closure_set(x_2, 0, lean_box(0));
lean_closure_set(x_2, 1, lean_box(0));
@ -3750,9 +3749,9 @@ static lean_object* _init_l_Lean_Elab_Term_instMonadQuotationTermElabM___closed_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__4;
x_1 = l_StateRefT_x27_instMonadLiftStateRefT_x27___closed__1;
x_2 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__6;
x_3 = l_StateRefT_x27_instMonadLiftStateRefT_x27___closed__1;
x_3 = l_Lean_Core_instMonadRefCoreM;
x_4 = l_Lean_instMonadRef___rarg(x_1, x_2, x_3);
return x_4;
}
@ -3760,31 +3759,32 @@ return x_4;
static lean_object* _init_l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__5;
x_2 = l_ReaderT_instMonadReaderT___rarg(x_1);
return x_2;
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__1;
x_2 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__5;
x_3 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__7;
x_4 = l_Lean_instMonadRef___rarg(x_1, x_2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__8;
x_2 = lean_alloc_closure((void*)(l_ReaderT_instMonadFunctorReaderT___boxed), 4, 3);
lean_closure_set(x_2, 0, lean_box(0));
lean_closure_set(x_2, 1, lean_box(0));
lean_closure_set(x_2, 2, x_1);
return x_2;
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_StateRefT_x27_instMonadLiftStateRefT_x27___closed__1;
x_2 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__4;
x_3 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__8;
x_4 = l_Lean_instMonadRef___rarg(x_1, x_2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__7;
x_2 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__9;
x_3 = l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__6;
x_1 = l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__1;
x_2 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__3;
x_3 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__9;
x_4 = l_Lean_instMonadRef___rarg(x_1, x_2, x_3);
return x_4;
}

16
stage0/stdlib/Lean/Elab/Util.c generated
View file

@ -2058,17 +2058,17 @@ lean_object* l_Lean_Elab_instMonadMacroAdapter___rarg(lean_object* x_1, lean_obj
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_3 = lean_ctor_get(x_1, 0);
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
lean_inc(x_2);
x_4 = lean_apply_2(x_2, lean_box(0), x_3);
x_5 = lean_ctor_get(x_1, 1);
lean_inc(x_1);
x_4 = lean_apply_2(x_1, lean_box(0), x_3);
x_5 = lean_ctor_get(x_2, 1);
lean_inc(x_5);
lean_inc(x_2);
x_6 = lean_apply_2(x_2, lean_box(0), x_5);
lean_inc(x_1);
x_6 = lean_apply_2(x_1, lean_box(0), x_5);
x_7 = lean_alloc_closure((void*)(l_Lean_Elab_instMonadMacroAdapter___rarg___lambda__1), 3, 2);
lean_closure_set(x_7, 0, x_1);
lean_closure_set(x_7, 1, x_2);
lean_closure_set(x_7, 0, x_2);
lean_closure_set(x_7, 1, x_1);
x_8 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_8, 0, x_4);
lean_ctor_set(x_8, 1, x_6);

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

@ -13459,13 +13459,13 @@ lean_object* l_Lean_instMonadEnv___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_3 = lean_ctor_get(x_1, 0);
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
lean_inc(x_2);
x_4 = lean_apply_2(x_2, lean_box(0), x_3);
lean_inc(x_1);
x_4 = lean_apply_2(x_1, lean_box(0), x_3);
x_5 = lean_alloc_closure((void*)(l_Lean_instMonadEnv___rarg___lambda__1), 3, 2);
lean_closure_set(x_5, 0, x_1);
lean_closure_set(x_5, 1, x_2);
lean_closure_set(x_5, 0, x_2);
lean_closure_set(x_5, 1, x_1);
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_4);
lean_ctor_set(x_6, 1, x_5);

2
stage0/stdlib/Lean/LocalContext.c generated
View file

@ -11179,7 +11179,7 @@ lean_object* l_Lean_instMonadLCtx___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_apply_2(x_2, lean_box(0), x_1);
x_3 = lean_apply_2(x_1, lean_box(0), x_2);
return x_3;
}
}

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

@ -27,15 +27,15 @@ lean_object* l_String_splitAux___at_Lean_stringToMessageData___spec__2___boxed(l
lean_object* l_Lean_addMessageContextPartial___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addMessageContextFull___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_stringToMessageData(lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__7;
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__5;
uint8_t l_Lean_MessageData_isNest(lean_object*);
lean_object* l_Lean_termM_x21_____closed__2;
lean_object* l_Lean_KernelException_toMessageData___closed__19;
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__14;
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__14;
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__7;
lean_object* l_Lean_instBEqMessageSeverity___closed__1;
lean_object* l_Lean_termM_x21_____closed__1;
extern lean_object* l_term_x5b___x5d___closed__9;
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__5;
extern lean_object* l_Char_quote___closed__1;
extern lean_object* l_Lean_Parser_Syntax_addPrec___closed__2;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
@ -43,12 +43,12 @@ lean_object* l_Lean_MessageLog_hasErrors_match__1___rarg(uint8_t, lean_object*,
lean_object* l_Lean_MessageData_ofList___closed__3;
uint8_t l_USize_decEq(size_t, size_t);
lean_object* lean_array_uget(lean_object*, size_t);
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__3;
lean_object* l_Lean_termM_x21__;
lean_object* l_Lean_KernelException_toMessageData___closed__7;
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__15;
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__3;
lean_object* l_Lean_MessageData_format(lean_object*, lean_object*);
lean_object* l_String_split___at_Lean_stringToMessageData___spec__1(lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__15;
extern lean_object* l_Std_Format_defWidth;
lean_object* l_Lean_MessageData_instCoeNameMessageData(lean_object*);
lean_object* l_Lean_MessageLog_hasErrors___boxed(lean_object*);
@ -68,6 +68,7 @@ lean_object* l_Lean_MessageData_joinSep_match__1___rarg(lean_object*, lean_objec
lean_object* l_Lean_MessageData_isNil_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkMVar(lean_object*);
size_t l_USize_sub(size_t, size_t);
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__10;
lean_object* l_Std_PersistentArray_append___rarg(lean_object*, lean_object*);
lean_object* l_Lean_instBEqMessageSeverity;
extern lean_object* l_Lean_instInhabitedParserDescr___closed__1;
@ -75,7 +76,6 @@ lean_object* l_Lean_Message_toString___lambda__1(lean_object*, lean_object*, lea
lean_object* l_Lean_MessageLog_hasErrors_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MessageData_ofList_match__1(lean_object*);
extern lean_object* l_Std_PersistentArray_empty___closed__1;
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__10;
extern lean_object* l_instReprSigma___rarg___closed__1;
lean_object* l_Lean_MessageData_nil;
lean_object* l_Lean_instToMessageDataArray___rarg(lean_object*, lean_object*);
@ -92,10 +92,10 @@ lean_object* lean_string_utf8_extract(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MessageData_formatAux___closed__1;
lean_object* l_Lean_MessageData_instCoeArrayExprMessageData___boxed(lean_object*);
lean_object* l_Lean_KernelException_toMessageData_match__2(lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__16;
extern lean_object* l_Applicative_seqRight___default___rarg___closed__1;
uint8_t l_Lean_Message_severity___default;
extern lean_object* l_Std_Format_sbracket___closed__4;
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__16;
lean_object* l_Lean_MessageData_instCoeArrayExprMessageData(lean_object*);
size_t l_USize_shiftRight(size_t, size_t);
lean_object* l_Lean_Message_toString___lambda__3___closed__1;
@ -121,20 +121,20 @@ lean_object* l_Lean_Name_toStringWithSep(lean_object*, lean_object*);
lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlFromMAux___at_Lean_MessageLog_getInfoMessages___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_string_utf8_next(lean_object*, lean_object*);
lean_object* l_Lean_MessageLog_toList(lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__6;
lean_object* l_Lean_instToMessageDataLevel(lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__6;
lean_object* l_Lean_ppGoal(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlMAux___at_Lean_MessageLog_getInfoMessages___spec__3(lean_object*, lean_object*);
lean_object* l_Lean_instToMessageDataOptionExpr_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_MessageLog_getInfoMessages___spec__4(lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_KernelException_toMessageData___closed__6;
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__13;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_MessageLog_getInfoMessages___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l_Lean_MessageLog_append(lean_object*, lean_object*);
lean_object* l_Lean_MessageLog_getInfoMessages_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_foldlM___at_Lean_MessageLog_getInfoMessages___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__13;
lean_object* l_Lean_MessageData_toString(lean_object*, lean_object*);
lean_object* l_Lean_Message_caption___default;
lean_object* l_Lean_MessageLog_errorsToWarnings_match__1___rarg(uint8_t, lean_object*, lean_object*);
@ -173,7 +173,7 @@ extern lean_object* l___private_Init_Util_0__mkPanicMessage___closed__2;
uint8_t l_Array_anyMUnsafe_any___at_Lean_MessageLog_hasErrors___spec__4(lean_object*, size_t, size_t);
lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlFromMAux___at_Lean_MessageLog_toList___spec__2(lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_instToMessageDataString___closed__1;
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1677_(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1678_(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_instInhabitedMessage;
lean_object* l_Nat_repr(lean_object*);
lean_object* l_Lean_KernelException_toMessageData___closed__18;
@ -217,12 +217,12 @@ lean_object* l___private_Lean_Message_0__Lean_beqMessageSeverity____x40_Lean_Mes
lean_object* l_Lean_instToMessageDataMessageData;
lean_object* l_Std_PersistentArray_foldlM___at_Lean_MessageLog_toList___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlMAux___at_Lean_MessageLog_toList___spec__3(lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__11;
lean_object* l_Lean_Message_toString_match__1(lean_object*);
extern lean_object* l_instReprList___rarg___closed__2;
lean_object* l_Lean_MessageData_ofList___closed__2;
lean_object* l_Lean_KernelException_toMessageData___closed__27;
lean_object* l_Array_anyMUnsafe_any___at_Lean_MessageLog_hasErrors___spec__4___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__11;
lean_object* l_Lean_instToMessageDataOption(lean_object*);
extern lean_object* l_Lean_Parser_Syntax_addPrec___closed__10;
lean_object* l_Lean_KernelException_toMessageData_match__2___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*);
@ -258,7 +258,7 @@ extern lean_object* l___private_Lean_Declaration_0__Lean_reprDefinitionSafety___
lean_object* l_Std_fmt___at_Lean_Level_PP_Result_format___spec__1(lean_object*);
lean_object* l_Lean_instToMessageDataList(lean_object*);
lean_object* l_Lean_instToMessageDataOption___rarg___closed__3;
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__1;
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__2;
uint8_t l_UInt32_decEq(uint32_t, uint32_t);
lean_object* l_Lean_Message_toString___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_push___rarg(lean_object*, lean_object*);
@ -267,10 +267,11 @@ lean_object* l_Lean_KernelException_toMessageData___closed__8;
lean_object* l_Lean_MessageLog_empty;
uint8_t l_String_isEmpty(lean_object*);
lean_object* l_Lean_MessageData_instCoeOptionExprMessageData(lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__2;
lean_object* l_Lean_instInhabitedMessageLog;
lean_object* l_Lean_KernelException_toMessageData___closed__4;
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__1;
lean_object* l_Lean_Message_toString___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__9;
lean_object* l_Lean_MessageData_ofList_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_List_map___at_Lean_MessageData_instCoeListExprMessageData___spec__1(lean_object*);
lean_object* l_Lean_MessageData_nestD(lean_object*);
@ -282,18 +283,17 @@ lean_object* l_Lean_Message_toString___lambda__3___closed__2;
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
lean_object* l_Lean_KernelException_toMessageData___closed__21;
lean_object* l_Lean_mkErrorStringWithPos___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__9;
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__4;
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__4;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_MessageLog_toList___spec__5(lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_MessageLog_getInfoMessages(lean_object*);
lean_object* l_Std_PersistentArray_forM___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__8;
lean_object* l_Lean_instToMessageDataOptionExpr___closed__3;
lean_object* l_Lean_KernelException_toMessageData___closed__2;
lean_object* l_Lean_MessageData_instCoeListExprMessageData(lean_object*);
lean_object* l_Lean_MessageData_ofList___closed__4;
lean_object* l_Lean_mkMessageEx___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MessageData_bracket(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__8;
lean_object* l_Lean_Message_endPos___default;
lean_object* l_Lean_MessageData_joinSep___boxed(lean_object*, lean_object*);
lean_object* l_Lean_KernelException_toMessageData___closed__31;
@ -363,7 +363,6 @@ uint8_t lean_string_utf8_at_end(lean_object*, lean_object*);
lean_object* l_Lean_Message_toString___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_13985____closed__9;
lean_object* l_Lean_MessageData_formatAux___closed__2;
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__12;
lean_object* l_Lean_MessageLog_add(lean_object*, lean_object*);
lean_object* lean_nat_to_int(lean_object*);
lean_object* l_Lean_addMessageContextPartial(lean_object*);
@ -372,6 +371,7 @@ extern lean_object* l_Array_instReprArray___rarg___closed__3;
lean_object* l_Lean_mkErrorStringWithPos(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MessageData_isNil___boxed(lean_object*);
lean_object* l_Lean_Syntax_formatStxAux(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__12;
lean_object* l_Lean_MessageData_ofList___closed__1;
lean_object* l_Lean_MessageData_arrayExpr_toMessageData___closed__1;
lean_object* l_Lean_KernelException_toMessageData___closed__11;
@ -5480,8 +5480,8 @@ lean_object* l_Lean_instAddMessageContext___rarg(lean_object* x_1, lean_object*
_start:
{
lean_object* x_4; lean_object* x_5;
x_4 = lean_apply_1(x_1, x_3);
x_5 = lean_apply_2(x_2, lean_box(0), x_4);
x_4 = lean_apply_1(x_2, x_3);
x_5 = lean_apply_2(x_1, lean_box(0), x_4);
return x_5;
}
}
@ -6225,7 +6225,7 @@ x_1 = l_Lean_termM_x21_____closed__6;
return x_1;
}
}
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__1() {
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__1() {
_start:
{
lean_object* x_1;
@ -6233,22 +6233,22 @@ x_1 = lean_mk_string("MessageData");
return x_1;
}
}
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__2() {
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__1;
x_1 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__1;
x_2 = lean_string_utf8_byte_size(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__3() {
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__1;
x_1 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__1;
x_2 = lean_unsigned_to_nat(0u);
x_3 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__2;
x_3 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__2;
x_4 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -6256,51 +6256,51 @@ lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__4() {
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__1;
x_2 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__5() {
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__2;
x_2 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__1;
x_2 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__6() {
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__5;
x_2 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__5;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__7() {
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__6;
x_2 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__6;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__8() {
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__8() {
_start:
{
lean_object* x_1;
@ -6308,22 +6308,22 @@ x_1 = lean_mk_string("toMessageData");
return x_1;
}
}
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__9() {
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__8;
x_1 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__8;
x_2 = lean_string_utf8_byte_size(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__10() {
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__8;
x_1 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__8;
x_2 = lean_unsigned_to_nat(0u);
x_3 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__9;
x_3 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__9;
x_4 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -6331,17 +6331,17 @@ lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__11() {
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__8;
x_2 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__8;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__12() {
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__12() {
_start:
{
lean_object* x_1;
@ -6349,51 +6349,51 @@ x_1 = lean_mk_string("ToMessageData");
return x_1;
}
}
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__13() {
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__13() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__2;
x_2 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__12;
x_2 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__12;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__14() {
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__14() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__13;
x_2 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__8;
x_1 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__13;
x_2 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__8;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__15() {
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__15() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__14;
x_2 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__14;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__16() {
static lean_object* _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__16() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__15;
x_2 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__15;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1677_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1678_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; uint8_t x_5;
@ -6425,13 +6425,13 @@ x_12 = lean_ctor_get(x_2, 2);
lean_inc(x_12);
x_13 = lean_ctor_get(x_2, 1);
lean_inc(x_13);
x_14 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__4;
x_14 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__4;
lean_inc(x_12);
lean_inc(x_13);
x_15 = l_Lean_addMacroScope(x_13, x_14, x_12);
x_16 = l_Lean_instInhabitedSourceInfo___closed__1;
x_17 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__3;
x_18 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__7;
x_17 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__3;
x_18 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__7;
x_19 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_19, 0, x_16);
lean_ctor_set(x_19, 1, x_17);
@ -6441,10 +6441,10 @@ x_20 = l_Lean_MonadRef_mkInfoFromRefPos___at_myMacro____x40_Init_Notation___hyg_
x_21 = lean_ctor_get(x_20, 1);
lean_inc(x_21);
lean_dec(x_20);
x_22 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__11;
x_22 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__11;
x_23 = l_Lean_addMacroScope(x_13, x_22, x_12);
x_24 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__10;
x_25 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__16;
x_24 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__10;
x_25 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__16;
x_26 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_26, 0, x_16);
lean_ctor_set(x_26, 1, x_24);
@ -7681,38 +7681,38 @@ l_Lean_termM_x21_____closed__6 = _init_l_Lean_termM_x21_____closed__6();
lean_mark_persistent(l_Lean_termM_x21_____closed__6);
l_Lean_termM_x21__ = _init_l_Lean_termM_x21__();
lean_mark_persistent(l_Lean_termM_x21__);
l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__1 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__1();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__1);
l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__2 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__2();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__2);
l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__3 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__3();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__3);
l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__4 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__4();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__4);
l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__5 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__5();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__5);
l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__6 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__6();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__6);
l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__7 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__7();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__7);
l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__8 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__8();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__8);
l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__9 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__9();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__9);
l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__10 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__10();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__10);
l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__11 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__11();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__11);
l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__12 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__12();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__12);
l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__13 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__13();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__13);
l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__14 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__14();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__14);
l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__15 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__15();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__15);
l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__16 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__16();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__16);
l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__1 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__1();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__1);
l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__2 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__2();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__2);
l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__3 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__3();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__3);
l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__4 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__4();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__4);
l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__5 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__5();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__5);
l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__6 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__6();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__6);
l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__7 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__7();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__7);
l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__8 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__8();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__8);
l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__9 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__9();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__9);
l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__10 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__10();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__10);
l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__11 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__11();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__11);
l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__12 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__12();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__12);
l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__13 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__13();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__13);
l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__14 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__14();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__14);
l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__15 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__15();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__15);
l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__16 = _init_l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__16();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__16);
l_Lean_KernelException_toMessageData___closed__1 = _init_l_Lean_KernelException_toMessageData___closed__1();
lean_mark_persistent(l_Lean_KernelException_toMessageData___closed__1);
l_Lean_KernelException_toMessageData___closed__2 = _init_l_Lean_KernelException_toMessageData___closed__2();

20
stage0/stdlib/Lean/Meta/Basic.c generated
View file

@ -26680,16 +26680,6 @@ return x_3;
static lean_object* _init_l_Lean_Meta_commitWhenSome_x3f___rarg___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Core_instMonadEnvCoreM;
x_2 = l_StateRefT_x27_instMonadLiftStateRefT_x27___closed__1;
x_3 = l_Lean_instMonadEnv___rarg(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_commitWhenSome_x3f___rarg___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_ReaderT_instMonadLiftReaderT), 3, 2);
lean_closure_set(x_1, 0, lean_box(0));
@ -26697,6 +26687,16 @@ lean_closure_set(x_1, 1, lean_box(0));
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_commitWhenSome_x3f___rarg___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_StateRefT_x27_instMonadLiftStateRefT_x27___closed__1;
x_2 = l_Lean_Core_instMonadEnvCoreM;
x_3 = l_Lean_instMonadEnv___rarg(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_commitWhenSome_x3f___rarg___closed__3() {
_start:
{

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

@ -62,10 +62,10 @@ lean_object* l_Lean_Meta_CheckAssignment_checkMVar_match__1___rarg(lean_object*,
lean_object* lean_array_uget(lean_object*, size_t);
lean_object* l___private_Lean_MetavarContext_0__Lean_MetavarContext_DependsOn_dep_visit(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_CheckAssignment_checkFVar___closed__11;
extern lean_object* l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__12;
lean_object* l_Lean_Meta_isDefEqStringLit(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_CheckAssignment_instMonadCacheExprExprCheckAssignmentM;
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldNonProjFnDefEq___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_CheckAssignment_checkFVar___closed__19;
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqBindingAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqOnFailure___spec__1___lambda__1(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_update_mdata(lean_object*, lean_object*);
@ -221,7 +221,6 @@ lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDelayedAssignedHead_
lean_object* l___private_Lean_MetavarContext_0__Lean_MetavarContext_DependsOn_dep_visitMain___at_Lean_Meta_CheckAssignment_check___spec__23___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_etaEq(lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__1;
extern lean_object* l_Lean_Meta_commitWhenSome_x3f___rarg___closed__2;
lean_object* l_Lean_Meta_CheckAssignment_throwOutOfScopeFVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_simpAssignmentArgAux_match__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDeltaCandidate_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -231,6 +230,7 @@ lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfold___rarg(lean_obj
lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlMAux___at_Lean_Meta_CheckAssignment_check___spec__53___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__2;
lean_object* l_Lean_Meta_isLevelDefEqAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_commitWhenSome_x3f___rarg___closed__1;
lean_object* l_Lean_mkAppN(lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_CheckAssignment_check___spec__57(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_Meta_CheckAssignment_checkAssignmentExceptionId;
@ -289,7 +289,6 @@ lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_assignConst___lambda__1___closed__2;
lean_object* l_Lean_Expr_constLevels_x21(lean_object*);
lean_object* l_Lean_addTrace___at_Lean_Meta_isLevelDefEqAux___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Core_instMonadRefCoreM;
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqLeft(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_simpAssignmentArgAux_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_processAssignment_process_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -313,7 +312,6 @@ lean_object* l_Lean_Meta_CheckAssignment_checkMVar___closed__4;
uint8_t l_Array_contains___at_Lean_Meta_CheckAssignment_check___spec__2(lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_processAssignmentFOApprox_loop_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_CheckAssignment_check___spec__56(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_Meta_CheckAssignment_checkFVar___closed__20;
lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlFromMAux___at_Lean_Meta_CheckAssignment_check___spec__52(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_Meta_isExprDefEqAuxImpl___lambda__2___closed__1;
lean_object* l_Lean_Meta_isDefEqNative_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -361,7 +359,6 @@ lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Met
lean_object* l_Lean_ConstantInfo_name(lean_object*);
uint8_t l_Array_anyMUnsafe_any___at_Lean_Meta_checkAssignment___spec__1(lean_object*, lean_object*, size_t, size_t);
extern lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_tryUnificationHints___spec__1___closed__2;
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__5;
lean_object* l_Lean_Meta_toCtorIfLit(lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstance___at___private_Lean_Meta_Basic_0__Lean_Meta_withNewLocalInstancesImp___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_CheckAssignment_checkFVar___closed__7;
@ -434,7 +431,6 @@ lean_object* l_Lean_mkLambda(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Meta_whenUndefDo(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldReducibeDefEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_CheckAssignment_check___spec__54___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__11;
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqLeftRight(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_checkAssignment(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_consumeLet_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -646,7 +642,6 @@ lean_object* lean_mk_array(lean_object*, lean_object*);
lean_object* l___private_Lean_Expr_0__Lean_mkAppRangeAux(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_mkLambdaFVarsWithLetDeps_addLetDeps___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Array_anyMUnsafe_any___at_Lean_Meta_CheckAssignment_check___spec__40(lean_object*, lean_object*, size_t, size_t);
extern lean_object* l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__9;
lean_object* l___private_Lean_MetavarContext_0__Lean_MetavarContext_DependsOn_dep_visit___at_Lean_Meta_CheckAssignment_check___spec__8(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Array_anyMUnsafe_any___at_Lean_Meta_CheckAssignment_check___spec__33(lean_object*, lean_object*, size_t, size_t);
uint8_t l_Array_anyMUnsafe_any___at_Lean_Meta_CheckAssignmentQuick_check_visit___spec__2(lean_object*, lean_object*, size_t, size_t);
@ -13123,8 +13118,8 @@ static lean_object* _init_l_Lean_Meta_CheckAssignment_checkFVar___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Core_instMonadTraceCoreM;
x_2 = l_StateRefT_x27_instMonadLiftStateRefT_x27___closed__1;
x_1 = l_StateRefT_x27_instMonadLiftStateRefT_x27___closed__1;
x_2 = l_Lean_Core_instMonadTraceCoreM;
x_3 = l_Lean_instMonadTrace___rarg(x_1, x_2);
return x_3;
}
@ -13133,8 +13128,8 @@ static lean_object* _init_l_Lean_Meta_CheckAssignment_checkFVar___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_CheckAssignment_checkFVar___closed__3;
x_2 = l_Lean_Meta_commitWhenSome_x3f___rarg___closed__2;
x_1 = l_Lean_Meta_commitWhenSome_x3f___rarg___closed__1;
x_2 = l_Lean_Meta_CheckAssignment_checkFVar___closed__3;
x_3 = l_Lean_instMonadTrace___rarg(x_1, x_2);
return x_3;
}
@ -13143,8 +13138,8 @@ static lean_object* _init_l_Lean_Meta_CheckAssignment_checkFVar___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_CheckAssignment_checkFVar___closed__4;
x_2 = l_StateRefT_x27_instMonadLiftStateRefT_x27___closed__1;
x_1 = l_StateRefT_x27_instMonadLiftStateRefT_x27___closed__1;
x_2 = l_Lean_Meta_CheckAssignment_checkFVar___closed__4;
x_3 = l_Lean_instMonadTrace___rarg(x_1, x_2);
return x_3;
}
@ -13153,8 +13148,8 @@ static lean_object* _init_l_Lean_Meta_CheckAssignment_checkFVar___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_CheckAssignment_checkFVar___closed__5;
x_2 = l_Lean_Meta_commitWhenSome_x3f___rarg___closed__2;
x_1 = l_Lean_Meta_commitWhenSome_x3f___rarg___closed__1;
x_2 = l_Lean_Meta_CheckAssignment_checkFVar___closed__5;
x_3 = l_Lean_instMonadTrace___rarg(x_1, x_2);
return x_3;
}
@ -13162,51 +13157,6 @@ return x_3;
static lean_object* _init_l_Lean_Meta_CheckAssignment_checkFVar___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Core_instMonadRefCoreM;
x_2 = l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__9;
x_3 = l_StateRefT_x27_instMonadLiftStateRefT_x27___closed__1;
x_4 = l_Lean_instMonadRef___rarg(x_1, x_2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Meta_CheckAssignment_checkFVar___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Meta_CheckAssignment_checkFVar___closed__7;
x_2 = l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__11;
x_3 = l_Lean_Meta_commitWhenSome_x3f___rarg___closed__2;
x_4 = l_Lean_instMonadRef___rarg(x_1, x_2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Meta_CheckAssignment_checkFVar___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__3;
x_2 = lean_alloc_closure((void*)(l_ReaderT_instMonadFunctorReaderT___boxed), 4, 3);
lean_closure_set(x_2, 0, lean_box(0));
lean_closure_set(x_2, 1, lean_box(0));
lean_closure_set(x_2, 2, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Meta_CheckAssignment_checkFVar___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Meta_CheckAssignment_checkFVar___closed__8;
x_2 = l_Lean_Meta_CheckAssignment_checkFVar___closed__9;
x_3 = l_StateRefT_x27_instMonadLiftStateRefT_x27___closed__1;
x_4 = l_Lean_instMonadRef___rarg(x_1, x_2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Meta_CheckAssignment_checkFVar___closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_CheckAssignment_checkFVar___closed__1;
x_2 = lean_alloc_closure((void*)(l_ReaderT_instMonadFunctorReaderT___boxed), 4, 3);
@ -13216,46 +13166,89 @@ lean_closure_set(x_2, 2, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Meta_CheckAssignment_checkFVar___closed__12() {
static lean_object* _init_l_Lean_Meta_CheckAssignment_checkFVar___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__3;
x_2 = lean_alloc_closure((void*)(l_ReaderT_instMonadFunctorReaderT___boxed), 4, 3);
lean_closure_set(x_2, 0, lean_box(0));
lean_closure_set(x_2, 1, lean_box(0));
lean_closure_set(x_2, 2, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Meta_CheckAssignment_checkFVar___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Meta_CheckAssignment_checkFVar___closed__10;
x_2 = l_Lean_Meta_CheckAssignment_checkFVar___closed__11;
x_3 = l_Lean_Meta_commitWhenSome_x3f___rarg___closed__2;
x_1 = l_StateRefT_x27_instMonadLiftStateRefT_x27___closed__1;
x_2 = l_Lean_Meta_CheckAssignment_checkFVar___closed__8;
x_3 = l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__12;
x_4 = l_Lean_instMonadRef___rarg(x_1, x_2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Meta_CheckAssignment_checkFVar___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Meta_commitWhenSome_x3f___rarg___closed__1;
x_2 = l_Lean_Meta_CheckAssignment_checkFVar___closed__7;
x_3 = l_Lean_Meta_CheckAssignment_checkFVar___closed__9;
x_4 = l_Lean_instMonadRef___rarg(x_1, x_2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Meta_CheckAssignment_checkFVar___closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_StateRefT_x27_instMonadLiftStateRefT_x27___closed__1;
x_2 = l_Lean_Meta_instAddMessageContextMetaM;
x_3 = lean_alloc_closure((void*)(l_Lean_instAddMessageContext___rarg), 3, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_CheckAssignment_checkFVar___closed__12() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_commitWhenSome_x3f___rarg___closed__1;
x_2 = l_Lean_Meta_CheckAssignment_checkFVar___closed__11;
x_3 = lean_alloc_closure((void*)(l_Lean_instAddMessageContext___rarg), 3, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_CheckAssignment_checkFVar___closed__13() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_instAddMessageContextMetaM;
x_2 = l_StateRefT_x27_instMonadLiftStateRefT_x27___closed__1;
x_3 = lean_alloc_closure((void*)(l_Lean_instAddMessageContext___rarg), 3, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Core_instMonadOptionsCoreM;
x_2 = lean_alloc_closure((void*)(l_StateRefT_x27_lift___rarg___boxed), 2, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Meta_CheckAssignment_checkFVar___closed__14() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_CheckAssignment_checkFVar___closed__13;
x_2 = l_Lean_Meta_commitWhenSome_x3f___rarg___closed__2;
x_3 = lean_alloc_closure((void*)(l_Lean_instAddMessageContext___rarg), 3, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
x_2 = lean_alloc_closure((void*)(l_ReaderT_instMonadLiftReaderT___rarg___boxed), 2, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Meta_CheckAssignment_checkFVar___closed__15() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Core_instMonadOptionsCoreM;
x_1 = l_Lean_Meta_CheckAssignment_checkFVar___closed__14;
x_2 = lean_alloc_closure((void*)(l_StateRefT_x27_lift___rarg___boxed), 2, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
@ -13274,37 +13267,17 @@ return x_2;
static lean_object* _init_l_Lean_Meta_CheckAssignment_checkFVar___closed__17() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_CheckAssignment_checkFVar___closed__16;
x_2 = lean_alloc_closure((void*)(l_StateRefT_x27_lift___rarg___boxed), 2, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Meta_CheckAssignment_checkFVar___closed__18() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_CheckAssignment_checkFVar___closed__17;
x_2 = lean_alloc_closure((void*)(l_ReaderT_instMonadLiftReaderT___rarg___boxed), 2, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Meta_CheckAssignment_checkFVar___closed__19() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("outOfScopeFVar");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_CheckAssignment_checkFVar___closed__20() {
static lean_object* _init_l_Lean_Meta_CheckAssignment_checkFVar___closed__18() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_checkTypesAndAssign___closed__2;
x_2 = l_Lean_Meta_CheckAssignment_checkFVar___closed__19;
x_2 = l_Lean_Meta_CheckAssignment_checkFVar___closed__17;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -13369,8 +13342,8 @@ x_24 = lean_ctor_get(x_18, 1);
lean_inc(x_24);
lean_dec(x_18);
x_25 = l_Lean_Meta_CheckAssignment_checkFVar___closed__2;
x_26 = l_Lean_Meta_CheckAssignment_checkFVar___closed__18;
x_27 = l_Lean_Meta_CheckAssignment_checkFVar___closed__20;
x_26 = l_Lean_Meta_CheckAssignment_checkFVar___closed__16;
x_27 = l_Lean_Meta_CheckAssignment_checkFVar___closed__18;
x_28 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___rarg(x_25, x_26, x_27);
lean_inc(x_8);
lean_inc(x_7);
@ -13415,8 +13388,8 @@ x_37 = lean_ctor_get(x_35, 1);
lean_inc(x_37);
lean_dec(x_35);
x_38 = l_Lean_Meta_CheckAssignment_checkFVar___closed__6;
x_39 = l_Lean_Meta_CheckAssignment_checkFVar___closed__12;
x_40 = l_Lean_Meta_CheckAssignment_checkFVar___closed__14;
x_39 = l_Lean_Meta_CheckAssignment_checkFVar___closed__10;
x_40 = l_Lean_Meta_CheckAssignment_checkFVar___closed__12;
x_41 = l_Lean_addTrace___rarg(x_25, x_38, x_39, x_40, x_27, x_36);
x_42 = lean_apply_7(x_41, x_3, x_4, x_5, x_6, x_7, x_8, x_37);
if (lean_obj_tag(x_42) == 0)
@ -13548,8 +13521,8 @@ x_64 = lean_ctor_get(x_58, 1);
lean_inc(x_64);
lean_dec(x_58);
x_65 = l_Lean_Meta_CheckAssignment_checkFVar___closed__2;
x_66 = l_Lean_Meta_CheckAssignment_checkFVar___closed__18;
x_67 = l_Lean_Meta_CheckAssignment_checkFVar___closed__20;
x_66 = l_Lean_Meta_CheckAssignment_checkFVar___closed__16;
x_67 = l_Lean_Meta_CheckAssignment_checkFVar___closed__18;
x_68 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___rarg(x_65, x_66, x_67);
lean_inc(x_8);
lean_inc(x_7);
@ -13594,8 +13567,8 @@ x_77 = lean_ctor_get(x_75, 1);
lean_inc(x_77);
lean_dec(x_75);
x_78 = l_Lean_Meta_CheckAssignment_checkFVar___closed__6;
x_79 = l_Lean_Meta_CheckAssignment_checkFVar___closed__12;
x_80 = l_Lean_Meta_CheckAssignment_checkFVar___closed__14;
x_79 = l_Lean_Meta_CheckAssignment_checkFVar___closed__10;
x_80 = l_Lean_Meta_CheckAssignment_checkFVar___closed__12;
x_81 = l_Lean_addTrace___rarg(x_65, x_78, x_79, x_80, x_67, x_76);
x_82 = lean_apply_7(x_81, x_3, x_4, x_5, x_6, x_7, x_8, x_77);
if (lean_obj_tag(x_82) == 0)
@ -14773,7 +14746,7 @@ x_147 = lean_ctor_get(x_141, 1);
lean_inc(x_147);
lean_dec(x_141);
x_148 = l_Lean_Meta_CheckAssignment_checkFVar___closed__2;
x_149 = l_Lean_Meta_CheckAssignment_checkFVar___closed__18;
x_149 = l_Lean_Meta_CheckAssignment_checkFVar___closed__16;
x_150 = l_Lean_Meta_CheckAssignment_checkMVar___closed__5;
x_151 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___rarg(x_148, x_149, x_150);
lean_inc(x_8);
@ -14819,8 +14792,8 @@ x_160 = lean_ctor_get(x_158, 1);
lean_inc(x_160);
lean_dec(x_158);
x_161 = l_Lean_Meta_CheckAssignment_checkFVar___closed__6;
x_162 = l_Lean_Meta_CheckAssignment_checkFVar___closed__12;
x_163 = l_Lean_Meta_CheckAssignment_checkFVar___closed__14;
x_162 = l_Lean_Meta_CheckAssignment_checkFVar___closed__10;
x_163 = l_Lean_Meta_CheckAssignment_checkFVar___closed__12;
x_164 = l_Lean_addTrace___rarg(x_148, x_161, x_162, x_163, x_150, x_159);
x_165 = lean_apply_7(x_164, x_3, x_4, x_5, x_6, x_7, x_8, x_160);
if (lean_obj_tag(x_165) == 0)
@ -14920,7 +14893,7 @@ x_25 = lean_ctor_get(x_19, 1);
lean_inc(x_25);
lean_dec(x_19);
x_26 = l_Lean_Meta_CheckAssignment_checkFVar___closed__2;
x_27 = l_Lean_Meta_CheckAssignment_checkFVar___closed__18;
x_27 = l_Lean_Meta_CheckAssignment_checkFVar___closed__16;
x_28 = l_Lean_Meta_CheckAssignment_checkMVar___closed__2;
x_29 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___rarg(x_26, x_27, x_28);
lean_inc(x_8);
@ -14966,8 +14939,8 @@ x_38 = lean_ctor_get(x_36, 1);
lean_inc(x_38);
lean_dec(x_36);
x_39 = l_Lean_Meta_CheckAssignment_checkFVar___closed__6;
x_40 = l_Lean_Meta_CheckAssignment_checkFVar___closed__12;
x_41 = l_Lean_Meta_CheckAssignment_checkFVar___closed__14;
x_40 = l_Lean_Meta_CheckAssignment_checkFVar___closed__10;
x_41 = l_Lean_Meta_CheckAssignment_checkFVar___closed__12;
x_42 = l_Lean_addTrace___rarg(x_26, x_39, x_40, x_41, x_28, x_37);
x_43 = lean_apply_7(x_42, x_3, x_4, x_5, x_6, x_7, x_8, x_38);
if (lean_obj_tag(x_43) == 0)
@ -15506,7 +15479,7 @@ x_304 = lean_ctor_get(x_298, 1);
lean_inc(x_304);
lean_dec(x_298);
x_305 = l_Lean_Meta_CheckAssignment_checkFVar___closed__2;
x_306 = l_Lean_Meta_CheckAssignment_checkFVar___closed__18;
x_306 = l_Lean_Meta_CheckAssignment_checkFVar___closed__16;
x_307 = l_Lean_Meta_CheckAssignment_checkMVar___closed__5;
x_308 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___rarg(x_305, x_306, x_307);
lean_inc(x_8);
@ -15552,8 +15525,8 @@ x_317 = lean_ctor_get(x_315, 1);
lean_inc(x_317);
lean_dec(x_315);
x_318 = l_Lean_Meta_CheckAssignment_checkFVar___closed__6;
x_319 = l_Lean_Meta_CheckAssignment_checkFVar___closed__12;
x_320 = l_Lean_Meta_CheckAssignment_checkFVar___closed__14;
x_319 = l_Lean_Meta_CheckAssignment_checkFVar___closed__10;
x_320 = l_Lean_Meta_CheckAssignment_checkFVar___closed__12;
x_321 = l_Lean_addTrace___rarg(x_305, x_318, x_319, x_320, x_307, x_316);
x_322 = lean_apply_7(x_321, x_3, x_4, x_5, x_6, x_7, x_8, x_317);
if (lean_obj_tag(x_322) == 0)
@ -15657,7 +15630,7 @@ x_186 = lean_ctor_get(x_180, 1);
lean_inc(x_186);
lean_dec(x_180);
x_187 = l_Lean_Meta_CheckAssignment_checkFVar___closed__2;
x_188 = l_Lean_Meta_CheckAssignment_checkFVar___closed__18;
x_188 = l_Lean_Meta_CheckAssignment_checkFVar___closed__16;
x_189 = l_Lean_Meta_CheckAssignment_checkMVar___closed__2;
x_190 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___rarg(x_187, x_188, x_189);
lean_inc(x_8);
@ -15703,8 +15676,8 @@ x_199 = lean_ctor_get(x_197, 1);
lean_inc(x_199);
lean_dec(x_197);
x_200 = l_Lean_Meta_CheckAssignment_checkFVar___closed__6;
x_201 = l_Lean_Meta_CheckAssignment_checkFVar___closed__12;
x_202 = l_Lean_Meta_CheckAssignment_checkFVar___closed__14;
x_201 = l_Lean_Meta_CheckAssignment_checkFVar___closed__10;
x_202 = l_Lean_Meta_CheckAssignment_checkFVar___closed__12;
x_203 = l_Lean_addTrace___rarg(x_187, x_200, x_201, x_202, x_189, x_198);
x_204 = lean_apply_7(x_203, x_3, x_4, x_5, x_6, x_7, x_8, x_199);
if (lean_obj_tag(x_204) == 0)
@ -16619,7 +16592,7 @@ lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; uint
x_22 = lean_ctor_get(x_16, 1);
lean_inc(x_22);
lean_dec(x_16);
x_23 = l_Lean_Meta_CheckAssignment_checkFVar___closed__20;
x_23 = l_Lean_Meta_CheckAssignment_checkFVar___closed__18;
x_24 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Meta_CheckAssignment_check___spec__4(x_23, x_2, x_3, x_4, x_5, x_6, x_7, x_22);
x_25 = lean_ctor_get(x_24, 0);
lean_inc(x_25);
@ -16730,7 +16703,7 @@ lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; uint
x_46 = lean_ctor_get(x_40, 1);
lean_inc(x_46);
lean_dec(x_40);
x_47 = l_Lean_Meta_CheckAssignment_checkFVar___closed__20;
x_47 = l_Lean_Meta_CheckAssignment_checkFVar___closed__18;
x_48 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Meta_CheckAssignment_check___spec__4(x_47, x_2, x_3, x_4, x_5, x_6, x_7, x_46);
x_49 = lean_ctor_get(x_48, 0);
lean_inc(x_49);
@ -52270,32 +52243,22 @@ return x_2;
static lean_object* _init_l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_CheckAssignment_checkFVar___closed__3;
x_2 = l_Lean_Meta_commitWhenSome_x3f___rarg___closed__2;
x_3 = l_Lean_instMonadTrace___rarg(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("stuckMVar");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__3() {
static lean_object* _init_l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_isExprDefEq___closed__2;
x_2 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__2;
x_2 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__4() {
static lean_object* _init_l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__3() {
_start:
{
lean_object* x_1;
@ -52303,11 +52266,11 @@ x_1 = lean_mk_string("found stuck MVar ");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__5() {
static lean_object* _init_l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__4;
x_1 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__3;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
@ -52389,8 +52352,8 @@ x_85 = lean_ctor_get(x_79, 1);
lean_inc(x_85);
lean_dec(x_79);
x_86 = l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__3;
x_87 = l_Lean_Meta_CheckAssignment_checkFVar___closed__16;
x_88 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__3;
x_87 = l_Lean_Meta_CheckAssignment_checkFVar___closed__14;
x_88 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__2;
x_89 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___rarg(x_86, x_87, x_88);
lean_inc(x_7);
lean_inc(x_6);
@ -52561,7 +52524,7 @@ else
lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54;
x_39 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_39, 0, x_15);
x_40 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__5;
x_40 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__4;
x_41 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_41, 0, x_40);
lean_ctor_set(x_41, 1, x_39);
@ -52579,10 +52542,10 @@ x_47 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_47, 0, x_45);
lean_ctor_set(x_47, 1, x_46);
x_48 = l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__3;
x_49 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__1;
x_50 = l_Lean_Meta_CheckAssignment_checkFVar___closed__8;
x_49 = l_Lean_Meta_CheckAssignment_checkFVar___closed__4;
x_50 = l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__12;
x_51 = l_Lean_Meta_instAddMessageContextMetaM;
x_52 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__3;
x_52 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__2;
x_53 = l_Lean_addTrace___rarg(x_48, x_49, x_50, x_51, x_52, x_47);
lean_inc(x_7);
lean_inc(x_6);
@ -52908,7 +52871,7 @@ lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; lean
x_78 = lean_ctor_get(x_72, 1);
lean_inc(x_78);
lean_dec(x_72);
x_79 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__3;
x_79 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__2;
x_80 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Meta_isLevelDefEqAux___spec__2(x_79, x_4, x_5, x_6, x_7, x_78);
x_81 = lean_ctor_get(x_80, 0);
lean_inc(x_81);
@ -53040,7 +53003,7 @@ else
lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53;
x_41 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_41, 0, x_17);
x_42 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__5;
x_42 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__4;
x_43 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_43, 0, x_42);
lean_ctor_set(x_43, 1, x_41);
@ -53057,7 +53020,7 @@ x_48 = l_Lean_KernelException_toMessageData___closed__15;
x_49 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_49, 0, x_47);
lean_ctor_set(x_49, 1, x_48);
x_50 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__3;
x_50 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__2;
x_51 = l_Lean_addTrace___at_Lean_Meta_isLevelDefEqAux___spec__1(x_50, x_49, x_4, x_5, x_6, x_7, x_22);
x_52 = lean_ctor_get(x_51, 1);
lean_inc(x_52);
@ -53313,7 +53276,7 @@ lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean
x_76 = lean_ctor_get(x_70, 1);
lean_inc(x_76);
lean_dec(x_70);
x_77 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__3;
x_77 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__2;
x_78 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Meta_isLevelDefEqAux___spec__2(x_77, x_4, x_5, x_6, x_7, x_76);
x_79 = lean_ctor_get(x_78, 0);
lean_inc(x_79);
@ -53443,7 +53406,7 @@ else
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;
x_39 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_39, 0, x_15);
x_40 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__5;
x_40 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__4;
x_41 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_41, 0, x_40);
lean_ctor_set(x_41, 1, x_39);
@ -53460,7 +53423,7 @@ x_46 = l_Lean_KernelException_toMessageData___closed__15;
x_47 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_47, 0, x_45);
lean_ctor_set(x_47, 1, x_46);
x_48 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__3;
x_48 = l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__2;
x_49 = l_Lean_addTrace___at_Lean_Meta_isLevelDefEqAux___spec__1(x_48, x_47, x_4, x_5, x_6, x_7, x_20);
x_50 = lean_ctor_get(x_49, 1);
lean_inc(x_50);
@ -58754,10 +58717,6 @@ l_Lean_Meta_CheckAssignment_checkFVar___closed__17 = _init_l_Lean_Meta_CheckAssi
lean_mark_persistent(l_Lean_Meta_CheckAssignment_checkFVar___closed__17);
l_Lean_Meta_CheckAssignment_checkFVar___closed__18 = _init_l_Lean_Meta_CheckAssignment_checkFVar___closed__18();
lean_mark_persistent(l_Lean_Meta_CheckAssignment_checkFVar___closed__18);
l_Lean_Meta_CheckAssignment_checkFVar___closed__19 = _init_l_Lean_Meta_CheckAssignment_checkFVar___closed__19();
lean_mark_persistent(l_Lean_Meta_CheckAssignment_checkFVar___closed__19);
l_Lean_Meta_CheckAssignment_checkFVar___closed__20 = _init_l_Lean_Meta_CheckAssignment_checkFVar___closed__20();
lean_mark_persistent(l_Lean_Meta_CheckAssignment_checkFVar___closed__20);
l_Lean_Meta_CheckAssignment_checkMVar___closed__1 = _init_l_Lean_Meta_CheckAssignment_checkMVar___closed__1();
lean_mark_persistent(l_Lean_Meta_CheckAssignment_checkMVar___closed__1);
l_Lean_Meta_CheckAssignment_checkMVar___closed__2 = _init_l_Lean_Meta_CheckAssignment_checkMVar___closed__2();
@ -58828,8 +58787,6 @@ l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__3 = _init_l__
lean_mark_persistent(l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__3);
l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__4 = _init_l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__4();
lean_mark_persistent(l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__4);
l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__5 = _init_l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__5();
lean_mark_persistent(l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__5);
l_Lean_Meta_isExprDefEqAuxImpl___lambda__2___closed__1 = _init_l_Lean_Meta_isExprDefEqAuxImpl___lambda__2___closed__1();
lean_mark_persistent(l_Lean_Meta_isExprDefEqAuxImpl___lambda__2___closed__1);
l_Lean_Meta_isExprDefEqAuxImpl___closed__1 = _init_l_Lean_Meta_isExprDefEqAuxImpl___closed__1();

34
stage0/stdlib/Lean/Meta/LevelDefEq.c generated
View file

@ -75,10 +75,10 @@ lean_object* l_Lean_Meta_isLevelDefEqAux___closed__4;
lean_object* l_Lean_Meta_getPostponed___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_levelZero;
lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_solveSelfMax___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_commitWhenSome_x3f___rarg___closed__2;
lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_strictOccursMax___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Meta_isLevelDefEqAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_forIn___at___private_Lean_Meta_LevelDefEq_0__Lean_Meta_processPostponedStep___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_commitWhenSome_x3f___rarg___closed__1;
lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_postponeIsLevelDefEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_processPostponedStep___closed__3;
lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Meta_isLevelDefEqAux___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -22088,7 +22088,7 @@ static lean_object* _init_l_Lean_Meta_withoutPostponingUniverseConstraintsImp___
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__1;
x_1 = l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__2;
x_2 = lean_alloc_closure((void*)(l_ReaderT_instMonadFunctorReaderT___boxed), 4, 3);
lean_closure_set(x_2, 0, lean_box(0));
lean_closure_set(x_2, 1, lean_box(0));
@ -22099,19 +22099,8 @@ return x_2;
static lean_object* _init_l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Core_instMonadRefCoreM;
x_2 = l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__9;
x_3 = l_StateRefT_x27_instMonadLiftStateRefT_x27___closed__1;
x_4 = l_Lean_instMonadRef___rarg(x_1, x_2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__2;
x_1 = l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__1;
x_2 = lean_alloc_closure((void*)(l_ReaderT_instMonadFunctorReaderT___boxed), 4, 3);
lean_closure_set(x_2, 0, lean_box(0));
lean_closure_set(x_2, 1, lean_box(0));
@ -22119,13 +22108,24 @@ lean_closure_set(x_2, 2, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_StateRefT_x27_instMonadLiftStateRefT_x27___closed__1;
x_2 = l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__10;
x_3 = l_Lean_Core_instMonadRefCoreM;
x_4 = l_Lean_instMonadRef___rarg(x_1, x_2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__12() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__10;
x_2 = l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__11;
x_3 = l_Lean_Meta_commitWhenSome_x3f___rarg___closed__2;
x_1 = l_Lean_Meta_commitWhenSome_x3f___rarg___closed__1;
x_2 = l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__9;
x_3 = l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__11;
x_4 = l_Lean_instMonadRef___rarg(x_1, x_2, x_3);
return x_4;
}

10
stage0/stdlib/Lean/Meta/Tactic/Intro.c generated
View file

@ -55,8 +55,8 @@ lean_object* l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_introNImp_loop___ra
lean_object* l_Lean_Meta_intro_match__1___rarg(lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_introNImp(lean_object*);
lean_object* l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_introNImp_loop___rarg___closed__1;
extern lean_object* l_Lean_Meta_commitWhenSome_x3f___rarg___closed__2;
lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Intro___hyg_539_(lean_object*);
extern lean_object* l_Lean_Meta_commitWhenSome_x3f___rarg___closed__1;
lean_object* l_Lean_Meta_intro(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_intro1Core(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -464,8 +464,8 @@ static lean_object* _init_l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_introN
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Core_instMonadNameGeneratorCoreM;
x_2 = l_StateRefT_x27_instMonadLiftStateRefT_x27___closed__1;
x_1 = l_StateRefT_x27_instMonadLiftStateRefT_x27___closed__1;
x_2 = l_Lean_Core_instMonadNameGeneratorCoreM;
x_3 = l_Lean_monadNameGeneratorLift___rarg(x_1, x_2);
return x_3;
}
@ -474,8 +474,8 @@ static lean_object* _init_l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_introN
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_introNImp_loop___rarg___closed__2;
x_2 = l_Lean_Meta_commitWhenSome_x3f___rarg___closed__2;
x_1 = l_Lean_Meta_commitWhenSome_x3f___rarg___closed__1;
x_2 = l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_introNImp_loop___rarg___closed__2;
x_3 = l_Lean_monadNameGeneratorLift___rarg(x_1, x_2);
return x_3;
}

10
stage0/stdlib/Lean/MetavarContext.c generated
View file

@ -1651,13 +1651,13 @@ lean_object* l_Lean_instMonadMCtx___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_3 = lean_ctor_get(x_1, 0);
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
lean_inc(x_2);
x_4 = lean_apply_2(x_2, lean_box(0), x_3);
lean_inc(x_1);
x_4 = lean_apply_2(x_1, lean_box(0), x_3);
x_5 = lean_alloc_closure((void*)(l_Lean_instMonadMCtx___rarg___lambda__1), 3, 2);
lean_closure_set(x_5, 0, x_1);
lean_closure_set(x_5, 1, x_2);
lean_closure_set(x_5, 0, x_2);
lean_closure_set(x_5, 1, x_1);
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_4);
lean_ctor_set(x_6, 1, x_5);

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

@ -117,7 +117,6 @@ lean_object* l_Lean_PrettyPrinter_Delaborator_annotatePos_match__2___rarg(lean_o
lean_object* l_Lean_PrettyPrinter_Delaborator_mkDelabAttribute___lambda__1(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addTrace___at_Lean_Meta_isLevelDefEqAux___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_instMonadQuotationDelabM___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__6;
lean_object* l_Lean_getPPUnicode___boxed(lean_object*);
lean_object* l_Lean_getPPUnicode___closed__1;
extern lean_object* l_Lean_Parser_Syntax_addPrec___closed__3;
@ -186,6 +185,7 @@ extern lean_object* l_Lean_KernelException_toMessageData___closed__3;
lean_object* l_Lean_PrettyPrinter_Delaborator_withProj(lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_whenNotPPOption(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_withBindingBody___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__1;
lean_object* l_Lean_getPPCoercions___closed__1;
lean_object* l_Lean_PrettyPrinter_Delaborator_withBindingBodyUnusedName___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Expr_setPPExplicit___closed__1;
@ -267,6 +267,7 @@ extern lean_object* l_Lean_Expr_ctorName___closed__6;
lean_object* l_Lean_PrettyPrinter_Delaborator_withAppFn_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter_Delaborator_Basic___hyg_1583_(lean_object*);
lean_object* lean_mk_syntax_ident(lean_object*);
extern lean_object* l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__2;
lean_object* l_Lean_PrettyPrinter_Delaborator_mkAppUnexpanderAttribute___closed__1;
lean_object* l_Lean_PrettyPrinter_Delaborator_withBindingBody(lean_object*);
lean_object* l_Lean_initFn____x40_Lean_PrettyPrinter_Delaborator_Basic___hyg_109____closed__3;
@ -311,7 +312,6 @@ lean_object* l_Lean_getPPStructureProjections___boxed(lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_getExprKind___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_failure___rarg(lean_object*);
lean_object* l_Std_RBNode_find___at_Lean_PrettyPrinter_Delaborator_getPPOption___spec__1___boxed(lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__6;
lean_object* l_Lean_PrettyPrinter_Delaborator_getPPOption_match__1(lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_liftMetaM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_getPPBinderTypes___closed__1;
@ -1290,7 +1290,7 @@ static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_instAlternativeDelabM
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__8;
x_1 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__2;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_PrettyPrinter_Delaborator_instAlternativeDelabM___closed__1;
@ -1369,9 +1369,9 @@ static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_instMonadQuotationDel
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__4;
x_2 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__6;
x_3 = l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__6;
x_1 = l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__1;
x_2 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__4;
x_3 = l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__8;
x_4 = l_Lean_instMonadRef___rarg(x_1, x_2, x_3);
return x_4;
}

68
stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c generated
View file

@ -3174,17 +3174,36 @@ return x_8;
static lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_MetavarContext_MkBinding_mkBinding___closed__1;
x_2 = l_ReaderT_instMonadReaderT___rarg(x_1);
return x_2;
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_ReaderT_instMonadLiftReaderT), 3, 2);
lean_closure_set(x_1, 0, lean_box(0));
lean_closure_set(x_1, 1, lean_box(0));
return x_1;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__1;
x_1 = l_Lean_MetavarContext_MkBinding_mkBinding___closed__1;
x_2 = l_ReaderT_instMonadReaderT___rarg(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__2;
x_2 = l_ReaderT_instMonadReaderT___rarg(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__3;
x_2 = lean_alloc_closure((void*)(l_ReaderT_instMonadFunctorReaderT___boxed), 4, 3);
lean_closure_set(x_2, 0, lean_box(0));
lean_closure_set(x_2, 1, lean_box(0));
@ -3192,31 +3211,11 @@ lean_closure_set(x_2, 2, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Core_instMonadRefCoreM;
x_2 = l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__2;
x_3 = l_StateRefT_x27_instMonadLiftStateRefT_x27___closed__1;
x_4 = l_Lean_instMonadRef___rarg(x_1, x_2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__1;
x_2 = l_ReaderT_instMonadReaderT___rarg(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__4;
x_1 = l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__2;
x_2 = lean_alloc_closure((void*)(l_ReaderT_instMonadFunctorReaderT___boxed), 4, 3);
lean_closure_set(x_2, 0, lean_box(0));
lean_closure_set(x_2, 1, lean_box(0));
@ -3227,19 +3226,20 @@ return x_2;
static lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__6() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_ReaderT_instMonadLiftReaderT), 3, 2);
lean_closure_set(x_1, 0, lean_box(0));
lean_closure_set(x_1, 1, lean_box(0));
return x_1;
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_StateRefT_x27_instMonadLiftStateRefT_x27___closed__1;
x_2 = l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__5;
x_3 = l_Lean_Core_instMonadRefCoreM;
x_4 = l_Lean_instMonadRef___rarg(x_1, x_2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__3;
x_2 = l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__5;
x_1 = l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__1;
x_2 = l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__4;
x_3 = l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__6;
x_4 = l_Lean_instMonadRef___rarg(x_1, x_2, x_3);
return x_4;
@ -5098,7 +5098,7 @@ static lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize__
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__4;
x_1 = l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__3;
x_2 = l_instInhabitedPUnit;
x_3 = l_instInhabited___rarg(x_1, x_2);
return x_3;

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

@ -4628,14 +4628,14 @@ lean_object* l_Lean_instMonadResolveName___rarg(lean_object* x_1, lean_object* x
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_3 = lean_ctor_get(x_1, 0);
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
lean_inc(x_2);
x_4 = lean_apply_2(x_2, lean_box(0), x_3);
x_5 = lean_ctor_get(x_1, 1);
lean_inc(x_1);
x_4 = lean_apply_2(x_1, lean_box(0), x_3);
x_5 = lean_ctor_get(x_2, 1);
lean_inc(x_5);
lean_dec(x_1);
x_6 = lean_apply_2(x_2, lean_box(0), x_5);
lean_dec(x_2);
x_6 = lean_apply_2(x_1, lean_box(0), x_5);
x_7 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_7, 0, x_4);
lean_ctor_set(x_7, 1, x_6);

16
stage0/stdlib/Lean/Util/MonadCache.c generated
View file

@ -746,7 +746,7 @@ lean_closure_set(x_3, 0, lean_box(0));
lean_closure_set(x_3, 1, lean_box(0));
lean_closure_set(x_3, 2, x_1);
x_4 = l_StateRefT_x27_instMonadLiftStateRefT_x27___closed__1;
x_5 = l_Lean_instMonadRef___rarg(x_2, x_3, x_4);
x_5 = l_Lean_instMonadRef___rarg(x_4, x_3, x_2);
return x_5;
}
}
@ -1015,13 +1015,13 @@ _start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
lean_inc(x_1);
x_3 = lean_alloc_closure((void*)(l_StateT_instMonadFunctorStateT___boxed), 4, 3);
lean_closure_set(x_3, 0, lean_box(0));
lean_closure_set(x_3, 1, lean_box(0));
lean_closure_set(x_3, 2, x_1);
x_4 = lean_alloc_closure((void*)(l_StateT_lift___rarg), 4, 1);
lean_closure_set(x_4, 0, x_1);
x_5 = l_Lean_instMonadRef___rarg(x_2, x_3, x_4);
x_3 = lean_alloc_closure((void*)(l_StateT_lift___rarg), 4, 1);
lean_closure_set(x_3, 0, x_1);
x_4 = lean_alloc_closure((void*)(l_StateT_instMonadFunctorStateT___boxed), 4, 3);
lean_closure_set(x_4, 0, lean_box(0));
lean_closure_set(x_4, 1, lean_box(0));
lean_closure_set(x_4, 2, x_1);
x_5 = l_Lean_instMonadRef___rarg(x_3, x_4, x_2);
return x_5;
}
}

178
stage0/stdlib/Lean/Util/Trace.c generated
View file

@ -13,23 +13,22 @@
#ifdef __cplusplus
extern "C" {
#endif
lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1252____closed__2;
lean_object* l_Lean_termTrace_x21____;
size_t l_USize_add(size_t, size_t);
lean_object* l_Std_PersistentArray_foldlM___at_Lean_withNestedTraces___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_registerTraceClass(lean_object*, lean_object*);
lean_object* l_Lean_stringToMessageData(lean_object*);
extern lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__5;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_printTraces___spec__3___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_MessageData_isNest(lean_object*);
extern lean_object* l_Lean_termM_x21_____closed__2;
lean_object* l_Lean_isTracingEnabledFor___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__5;
extern lean_object* l_Lean_Parser_Syntax_addPrec___closed__2;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_12458____closed__10;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
uint8_t l_USize_decEq(size_t, size_t);
lean_object* lean_array_uget(lean_object*, size_t);
extern lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__3;
extern lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__3;
lean_object* l_Lean_MessageData_format(lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_printTraces___spec__4___rarg___lambda__1(lean_object*, lean_object*);
lean_object* l_Lean_withNestedTraces___rarg___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -43,6 +42,7 @@ lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___rarg___lamb
extern lean_object* l_Lean_initFn____x40_Lean_Util_PPExt___hyg_3____closed__3;
lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_traceCtx___rarg___lambda__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1254____closed__2;
size_t l_USize_sub(size_t, size_t);
extern lean_object* l_Array_empty___closed__1;
lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlFromMAux___at_Lean_withNestedTraces___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -113,18 +113,18 @@ lean_object* l_Lean_termTrace_x21_______closed__3;
lean_object* l_Lean_enableTracing___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_registerTraceClass___closed__2;
lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__4;
lean_object* l_Lean_termTrace_x5b_____x5d_x21_______closed__1;
lean_object* l_Lean_traceCtx___rarg___lambda__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_MessageData_isNil(lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1254____closed__3;
lean_object* l_Std_PersistentArray_foldlM___at_Lean_withNestedTraces___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Util_Trace_0__Lean_addNode___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_traceCtx___rarg___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_traceM(lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_13068____closed__13;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_printTraces___spec__4___rarg(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1252____closed__3;
extern lean_object* l_Lean_instInhabitedSourceInfo___closed__1;
lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__4;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_12458____closed__12;
lean_object* l_Lean_Syntax_getId(lean_object*);
lean_object* l_Lean_traceCtx___rarg___lambda__2___closed__1;
@ -145,7 +145,6 @@ uint8_t l_Lean_KVMap_contains(lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_withNestedTraces___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_withNestedTraces___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Meta_0__Lean_quoteName(lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__2;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_withNestedTraces___spec__4(lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_enableTracing(lean_object*);
lean_object* l_Std_PersistentArray_forMAux___at_Lean_printTraces___spec__2(lean_object*);
@ -172,6 +171,8 @@ lean_object* l_Lean_modifyTraces___rarg(lean_object*, lean_object*);
size_t l_USize_land(size_t, size_t);
lean_object* l_Lean_termTrace_x21_______closed__6;
extern lean_object* l_Lean_nullKind___closed__2;
lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__3;
lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__2;
lean_object* l_Lean_termTrace_x5b_____x5d_x21_______closed__5;
lean_object* l_Lean_instInhabitedTraceState___closed__1;
lean_object* l_ReaderT_instMonadReaderT___rarg___lambda__4___boxed(lean_object*, lean_object*, lean_object*);
@ -182,7 +183,6 @@ lean_object* l_Lean_resetTraceState(lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_printTraces___spec__3___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadTracer_trace(lean_object*);
lean_object* l_Lean_setTraceState___rarg(lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1252____closed__1;
lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlMAux___at_Lean_withNestedTraces___spec__3(lean_object*, lean_object*);
lean_object* l_Lean_instInhabitedTraceElem;
lean_object* l_Lean_enableTracing___rarg___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -194,28 +194,30 @@ lean_object* l___private_Lean_Util_Trace_0__Lean_getResetTraces___rarg___lambda_
lean_object* l_Lean_resetTraceState___rarg___lambda__1___closed__1;
lean_object* l_Lean_instMonadTrace___rarg(lean_object*, lean_object*);
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__1;
lean_object* l_Std_PersistentArray_get_x21___at___private_Lean_Util_Trace_0__Lean_TraceState_toFormat___spec__1(lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_toArray___rarg(lean_object*);
lean_object* l_Lean_Name_append(lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_withNestedTraces___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getKind(lean_object*);
extern lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__4;
lean_object* l___private_Lean_Util_Trace_0__Lean_addNode___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__1;
extern lean_object* l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__4;
lean_object* l_Lean_traceCtx___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_enableTracing___rarg___lambda__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1254____closed__1;
lean_object* l_Lean_enableTracing___rarg___lambda__2(lean_object*, uint8_t, lean_object*);
lean_object* l_Lean_withNestedTraces___rarg___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_forMAux___at_Lean_printTraces___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_register_option(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__6;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_12458____closed__8;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_12458____closed__9;
lean_object* l_Lean_printTraces(lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_13068____closed__14;
lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__6;
lean_object* l_Lean_checkTraceOption___boxed(lean_object*, lean_object*);
lean_object* l_Lean_checkTraceOption___closed__1;
lean_object* l_Lean_traceM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__5;
lean_object* l_Lean_addTrace(lean_object*);
lean_object* l_Lean_resetTraceState___rarg___lambda__1___boxed(lean_object*);
lean_object* l_IO_println___at_Lean_instEval__1___spec__1(lean_object*, lean_object*);
@ -231,18 +233,18 @@ lean_object* l_Lean_trace___rarg___lambda__1___boxed(lean_object*, lean_object*,
lean_object* l_Lean_traceCtx___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_termM_x21_____closed__3;
extern lean_object* l_prec_x28___x29___closed__7;
lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932_(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1252_(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934_(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1254_(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_termTrace_x21_______closed__7;
lean_object* l_Lean_addTrace___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_traceCtx___rarg___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__5;
extern lean_object* l_prec_x28___x29___closed__3;
lean_object* l_Lean_printTraces___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_TraceState_enabled___default;
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
lean_object* l_Lean_instMonadTrace___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_getTraces___rarg(lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__7;
lean_object* l_Lean_trace___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_traceCtx___rarg___lambda__1(lean_object*);
@ -259,12 +261,10 @@ lean_object* l_Lean_traceCtx___rarg___lambda__3(lean_object*, uint8_t, lean_obje
extern lean_object* l_myMacro____x40_Init_Notation___hyg_13985____closed__9;
lean_object* l_Lean_checkTraceOption___closed__2;
extern lean_object* l_tryFinally___rarg___closed__1;
lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__3;
uint8_t l___private_Lean_Util_Trace_0__Lean_checkTraceOptionAux(lean_object*, lean_object*);
lean_object* l_Lean_termTrace_x5b_____x5d_x21_______closed__10;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_13985____closed__8;
lean_object* l___private_Lean_Util_Trace_0__Lean_TraceState_toFormat(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__7;
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
extern lean_object* l_Std_PersistentArray_getAux___rarg___closed__1;
lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionAux___boxed(lean_object*, lean_object*);
@ -558,15 +558,15 @@ lean_object* l_Lean_instMonadTrace___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
lean_inc(x_2);
lean_inc(x_1);
lean_inc(x_2);
x_3 = lean_alloc_closure((void*)(l_Lean_instMonadTrace___rarg___lambda__1), 3, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
x_4 = lean_ctor_get(x_1, 1);
lean_closure_set(x_3, 0, x_2);
lean_closure_set(x_3, 1, x_1);
x_4 = lean_ctor_get(x_2, 1);
lean_inc(x_4);
lean_dec(x_1);
x_5 = lean_apply_2(x_2, lean_box(0), x_4);
lean_dec(x_2);
x_5 = lean_apply_2(x_1, lean_box(0), x_4);
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_3);
lean_ctor_set(x_6, 1, x_5);
@ -2592,7 +2592,7 @@ x_1 = l_Lean_termTrace_x21_______closed__7;
return x_1;
}
}
static lean_object* _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__1() {
static lean_object* _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
@ -2601,13 +2601,13 @@ x_2 = lean_string_utf8_byte_size(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__2() {
static lean_object* _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_checkTraceOption___closed__1;
x_2 = lean_unsigned_to_nat(0u);
x_3 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__1;
x_3 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__1;
x_4 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -2615,7 +2615,7 @@ lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__3() {
static lean_object* _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -2625,55 +2625,55 @@ x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__4() {
static lean_object* _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__3;
x_2 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__3;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
static lean_object* _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__5() {
static lean_object* _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__4;
x_2 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__4;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
static lean_object* _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__6() {
static lean_object* _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__5;
x_2 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__5;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
static lean_object* _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__7() {
static lean_object* _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__6;
x_2 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__6;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; uint8_t x_5;
@ -2715,8 +2715,8 @@ lean_inc(x_15);
lean_inc(x_16);
x_18 = l_Lean_addMacroScope(x_16, x_17, x_15);
x_19 = l_Lean_instInhabitedSourceInfo___closed__1;
x_20 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__2;
x_21 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__5;
x_20 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__2;
x_21 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__5;
x_22 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_22, 0, x_19);
lean_ctor_set(x_22, 1, x_20);
@ -2766,10 +2766,10 @@ x_46 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_46, 0, x_14);
lean_ctor_set(x_46, 1, x_45);
x_47 = lean_array_push(x_23, x_46);
x_48 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__4;
x_48 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__4;
x_49 = l_Lean_addMacroScope(x_16, x_48, x_15);
x_50 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__3;
x_51 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__7;
x_50 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__3;
x_51 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__7;
x_52 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_52, 0, x_19);
lean_ctor_set(x_52, 1, x_50);
@ -2838,8 +2838,8 @@ lean_inc(x_79);
lean_inc(x_80);
x_82 = l_Lean_addMacroScope(x_80, x_81, x_79);
x_83 = l_Lean_instInhabitedSourceInfo___closed__1;
x_84 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__2;
x_85 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__5;
x_84 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__2;
x_85 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__5;
x_86 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_86, 0, x_83);
lean_ctor_set(x_86, 1, x_84);
@ -2889,10 +2889,10 @@ x_110 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_110, 0, x_77);
lean_ctor_set(x_110, 1, x_109);
x_111 = lean_array_push(x_87, x_110);
x_112 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__4;
x_112 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__4;
x_113 = l_Lean_addMacroScope(x_80, x_112, x_79);
x_114 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__3;
x_115 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__7;
x_114 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__3;
x_115 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__7;
x_116 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_116, 0, x_83);
lean_ctor_set(x_116, 1, x_114);
@ -3066,7 +3066,7 @@ x_1 = l_Lean_termTrace_x5b_____x5d_x21_______closed__10;
return x_1;
}
}
static lean_object* _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1252____closed__1() {
static lean_object* _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1254____closed__1() {
_start:
{
lean_object* x_1;
@ -3074,22 +3074,22 @@ x_1 = lean_mk_string("Lean.trace");
return x_1;
}
}
static lean_object* _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1252____closed__2() {
static lean_object* _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1254____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1252____closed__1;
x_1 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1254____closed__1;
x_2 = lean_string_utf8_byte_size(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1252____closed__3() {
static lean_object* _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1254____closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1252____closed__1;
x_1 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1254____closed__1;
x_2 = lean_unsigned_to_nat(0u);
x_3 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1252____closed__2;
x_3 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1254____closed__2;
x_4 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -3097,7 +3097,7 @@ lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1252_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1254_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; uint8_t x_5;
@ -3142,13 +3142,13 @@ lean_inc(x_18);
x_19 = lean_ctor_get(x_2, 1);
lean_inc(x_19);
lean_dec(x_2);
x_20 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__3;
x_20 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__3;
lean_inc(x_18);
lean_inc(x_19);
x_21 = l_Lean_addMacroScope(x_19, x_20, x_18);
x_22 = l_Lean_instInhabitedSourceInfo___closed__1;
x_23 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1252____closed__3;
x_24 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__5;
x_23 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1254____closed__3;
x_24 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__5;
x_25 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_25, 0, x_22);
lean_ctor_set(x_25, 1, x_23);
@ -3201,10 +3201,10 @@ x_51 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_51, 0, x_17);
lean_ctor_set(x_51, 1, x_50);
x_52 = lean_array_push(x_26, x_51);
x_53 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__4;
x_53 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__4;
x_54 = l_Lean_addMacroScope(x_19, x_53, x_18);
x_55 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__3;
x_56 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__7;
x_55 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__3;
x_56 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__7;
x_57 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_57, 0, x_22);
lean_ctor_set(x_57, 1, x_55);
@ -3268,13 +3268,13 @@ lean_inc(x_84);
x_85 = lean_ctor_get(x_2, 1);
lean_inc(x_85);
lean_dec(x_2);
x_86 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__3;
x_86 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__3;
lean_inc(x_84);
lean_inc(x_85);
x_87 = l_Lean_addMacroScope(x_85, x_86, x_84);
x_88 = l_Lean_instInhabitedSourceInfo___closed__1;
x_89 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1252____closed__3;
x_90 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__5;
x_89 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1254____closed__3;
x_90 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__5;
x_91 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_91, 0, x_88);
lean_ctor_set(x_91, 1, x_89);
@ -3327,10 +3327,10 @@ x_117 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_117, 0, x_82);
lean_ctor_set(x_117, 1, x_116);
x_118 = lean_array_push(x_92, x_117);
x_119 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__4;
x_119 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__4;
x_120 = l_Lean_addMacroScope(x_85, x_119, x_84);
x_121 = l_Lean_myMacro____x40_Lean_Message___hyg_1677____closed__3;
x_122 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__7;
x_121 = l_Lean_myMacro____x40_Lean_Message___hyg_1678____closed__3;
x_122 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__7;
x_123 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_123, 0, x_88);
lean_ctor_set(x_123, 1, x_121);
@ -3398,11 +3398,11 @@ lean_inc(x_152);
x_153 = lean_ctor_get(x_2, 1);
lean_inc(x_153);
lean_dec(x_2);
x_154 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__3;
x_154 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__3;
x_155 = l_Lean_addMacroScope(x_153, x_154, x_152);
x_156 = l_Lean_instInhabitedSourceInfo___closed__1;
x_157 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1252____closed__3;
x_158 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__5;
x_157 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1254____closed__3;
x_158 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__5;
x_159 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_159, 0, x_156);
lean_ctor_set(x_159, 1, x_157);
@ -3487,11 +3487,11 @@ lean_inc(x_199);
x_200 = lean_ctor_get(x_2, 1);
lean_inc(x_200);
lean_dec(x_2);
x_201 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__3;
x_201 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__3;
x_202 = l_Lean_addMacroScope(x_200, x_201, x_199);
x_203 = l_Lean_instInhabitedSourceInfo___closed__1;
x_204 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1252____closed__3;
x_205 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__5;
x_204 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1254____closed__3;
x_205 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__5;
x_206 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_206, 0, x_203);
lean_ctor_set(x_206, 1, x_204);
@ -4372,20 +4372,20 @@ l_Lean_termTrace_x21_______closed__7 = _init_l_Lean_termTrace_x21_______closed__
lean_mark_persistent(l_Lean_termTrace_x21_______closed__7);
l_Lean_termTrace_x21____ = _init_l_Lean_termTrace_x21____();
lean_mark_persistent(l_Lean_termTrace_x21____);
l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__1 = _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__1();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__1);
l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__2 = _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__2();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__2);
l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__3 = _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__3();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__3);
l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__4 = _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__4();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__4);
l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__5 = _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__5();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__5);
l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__6 = _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__6();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__6);
l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__7 = _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__7();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Util_Trace___hyg_932____closed__7);
l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__1 = _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__1();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__1);
l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__2 = _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__2();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__2);
l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__3 = _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__3();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__3);
l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__4 = _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__4();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__4);
l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__5 = _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__5();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__5);
l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__6 = _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__6();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__6);
l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__7 = _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__7();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Util_Trace___hyg_934____closed__7);
l_Lean_termTrace_x5b_____x5d_x21_______closed__1 = _init_l_Lean_termTrace_x5b_____x5d_x21_______closed__1();
lean_mark_persistent(l_Lean_termTrace_x5b_____x5d_x21_______closed__1);
l_Lean_termTrace_x5b_____x5d_x21_______closed__2 = _init_l_Lean_termTrace_x5b_____x5d_x21_______closed__2();
@ -4408,12 +4408,12 @@ l_Lean_termTrace_x5b_____x5d_x21_______closed__10 = _init_l_Lean_termTrace_x5b__
lean_mark_persistent(l_Lean_termTrace_x5b_____x5d_x21_______closed__10);
l_Lean_termTrace_x5b_____x5d_x21____ = _init_l_Lean_termTrace_x5b_____x5d_x21____();
lean_mark_persistent(l_Lean_termTrace_x5b_____x5d_x21____);
l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1252____closed__1 = _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1252____closed__1();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1252____closed__1);
l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1252____closed__2 = _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1252____closed__2();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1252____closed__2);
l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1252____closed__3 = _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1252____closed__3();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1252____closed__3);
l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1254____closed__1 = _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1254____closed__1();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1254____closed__1);
l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1254____closed__2 = _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1254____closed__2();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1254____closed__2);
l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1254____closed__3 = _init_l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1254____closed__3();
lean_mark_persistent(l_Lean_myMacro____x40_Lean_Util_Trace___hyg_1254____closed__3);
l_Array_foldlMUnsafe_fold___at_Lean_withNestedTraces___spec__5___closed__1 = _init_l_Array_foldlMUnsafe_fold___at_Lean_withNestedTraces___spec__5___closed__1();
lean_mark_persistent(l_Array_foldlMUnsafe_fold___at_Lean_withNestedTraces___spec__5___closed__1);
return lean_io_result_mk_ok(lean_box(0));