From 5c91b395d6544a489e37d824171414a433cef987 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 13 Jan 2021 18:43:16 -0800 Subject: [PATCH] chore: update stage0 --- stage0/src/Init/Coe.lean | 10 +- stage0/src/Init/Control/Basic.lean | 2 +- stage0/src/Init/Control/Reader.lean | 2 +- stage0/src/Init/Meta.lean | 2 +- stage0/src/Init/Prelude.lean | 14 +- stage0/src/Init/System/ST.lean | 2 +- stage0/src/Lean/Data/Options.lean | 4 +- stage0/src/Lean/Elab/InfoTree.lean | 2 +- stage0/src/Lean/Elab/Log.lean | 9 +- stage0/src/Lean/Elab/Util.lean | 2 +- stage0/src/Lean/Environment.lean | 5 +- stage0/src/Lean/LocalContext.lean | 2 +- stage0/src/Lean/Message.lean | 4 +- stage0/src/Lean/MetavarContext.lean | 2 +- stage0/src/Lean/ResolveName.lean | 2 +- stage0/src/Lean/Util/Trace.lean | 6 +- stage0/stdlib/Init/Coe.c | 20 +- stage0/stdlib/Init/Control/Basic.c | 10 +- stage0/stdlib/Init/Control/Reader.c | 8 +- stage0/stdlib/Init/Meta.c | 10 +- stage0/stdlib/Init/Prelude.c | 50 ++-- stage0/stdlib/Lean/Data/Options.c | 2 +- stage0/stdlib/Lean/Elab/App.c | 14 +- stage0/stdlib/Lean/Elab/Binders.c | 4 +- stage0/stdlib/Lean/Elab/InfoTree.c | 10 +- stage0/stdlib/Lean/Elab/Log.c | 22 +- stage0/stdlib/Lean/Elab/Match.c | 4 +- stage0/stdlib/Lean/Elab/PreDefinition/Main.c | 6 +- stage0/stdlib/Lean/Elab/Term.c | 74 ++--- stage0/stdlib/Lean/Elab/Util.c | 16 +- stage0/stdlib/Lean/Environment.c | 10 +- stage0/stdlib/Lean/LocalContext.c | 2 +- stage0/stdlib/Lean/Message.c | 180 ++++++------ stage0/stdlib/Lean/Meta/Basic.c | 20 +- stage0/stdlib/Lean/Meta/ExprDefEq.c | 267 ++++++++---------- stage0/stdlib/Lean/Meta/LevelDefEq.c | 34 +-- stage0/stdlib/Lean/Meta/Tactic/Intro.c | 10 +- stage0/stdlib/Lean/MetavarContext.c | 10 +- .../Lean/PrettyPrinter/Delaborator/Basic.c | 12 +- .../stdlib/Lean/PrettyPrinter/Parenthesizer.c | 68 ++--- stage0/stdlib/Lean/ResolveName.c | 12 +- stage0/stdlib/Lean/Util/MonadCache.c | 16 +- stage0/stdlib/Lean/Util/Trace.c | 178 ++++++------ 43 files changed, 547 insertions(+), 592 deletions(-) diff --git a/stage0/src/Init/Coe.lean b/stage0/src/Init/Coe.lean index ca45e9b4db..a551c061bc 100644 --- a/stage0/src/Init/Coe.lean +++ b/stage0/src/Init/Coe.lean @@ -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 diff --git a/stage0/src/Init/Control/Basic.lean b/stage0/src/Init/Control/Basic.lean index 7f3d120303..b242bbd8df 100644 --- a/stage0/src/Init/Control/Basic.lean +++ b/stage0/src/Init/Control/Basic.lean @@ -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 diff --git a/stage0/src/Init/Control/Reader.lean b/stage0/src/Init/Control/Reader.lean index 0a5e94a006..db60187815 100644 --- a/stage0/src/Init/Control/Reader.lean +++ b/stage0/src/Init/Control/Reader.lean @@ -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 diff --git a/stage0/src/Init/Meta.lean b/stage0/src/Init/Meta.lean index d07970a6ca..88290d500b 100644 --- a/stage0/src/Init/Meta.lean +++ b/stage0/src/Init/Meta.lean @@ -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 _) } diff --git a/stage0/src/Init/Prelude.lean b/stage0/src/Init/Prelude.lean index fbcb598ac9..76354368af 100644 --- a/stage0/src/Init/Prelude.lean +++ b/stage0/src/Init/Prelude.lean @@ -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 diff --git a/stage0/src/Init/System/ST.lean b/stage0/src/Init/System/ST.lean index 2e57269872..cad11f39bf 100644 --- a/stage0/src/Init/System/ST.lean +++ b/stage0/src/Init/System/ST.lean @@ -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] diff --git a/stage0/src/Lean/Data/Options.lean b/stage0/src/Lean/Data/Options.lean index f7461215b2..59342b335e 100644 --- a/stage0/src/Lean/Data/Options.lean +++ b/stage0/src/Lean/Data/Options.lean @@ -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] diff --git a/stage0/src/Lean/Elab/InfoTree.lean b/stage0/src/Lean/Elab/InfoTree.lean index da26b37f60..573f91d26e 100644 --- a/stage0/src/Lean/Elab/InfoTree.lean +++ b/stage0/src/Lean/Elab/InfoTree.lean @@ -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 _) diff --git a/stage0/src/Lean/Elab/Log.lean b/stage0/src/Lean/Elab/Log.lean index 5a3288bc58..22345f1dd0 100644 --- a/stage0/src/Lean/Elab/Log.lean +++ b/stage0/src/Lean/Elab/Log.lean @@ -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] diff --git a/stage0/src/Lean/Elab/Util.lean b/stage0/src/Lean/Elab/Util.lean index 6994b63425..f1e48ed229 100644 --- a/stage0/src/Lean/Elab/Util.lean +++ b/stage0/src/Lean/Elab/Util.lean @@ -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 _) diff --git a/stage0/src/Lean/Environment.lean b/stage0/src/Lean/Environment.lean index 2997d4ffa2..9fa22fc296 100644 --- a/stage0/src/Lean/Environment.lean +++ b/stage0/src/Lean/Environment.lean @@ -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 diff --git a/stage0/src/Lean/LocalContext.lean b/stage0/src/Lean/LocalContext.lean index 5f8b43f8df..a3fa426360 100644 --- a/stage0/src/Lean/LocalContext.lean +++ b/stage0/src/Lean/LocalContext.lean @@ -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 := diff --git a/stage0/src/Lean/Message.lean b/stage0/src/Lean/Message.lean index 5190505f0c..b970181955 100644 --- a/stage0/src/Lean/Message.lean +++ b/stage0/src/Lean/Message.lean @@ -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 diff --git a/stage0/src/Lean/MetavarContext.lean b/stage0/src/Lean/MetavarContext.lean index 01980ccf57..5ae7d7a634 100644 --- a/stage0/src/Lean/MetavarContext.lean +++ b/stage0/src/Lean/MetavarContext.lean @@ -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 _) diff --git a/stage0/src/Lean/ResolveName.lean b/stage0/src/Lean/ResolveName.lean index f9b2ace28a..9528d53b9e 100644 --- a/stage0/src/Lean/ResolveName.lean +++ b/stage0/src/Lean/ResolveName.lean @@ -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 diff --git a/stage0/src/Lean/Util/Trace.lean b/stage0/src/Lean/Util/Trace.lean index b294c5bfb4..a34d0d9832 100644 --- a/stage0/src/Lean/Util/Trace.lean +++ b/stage0/src/Lean/Util/Trace.lean @@ -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] diff --git a/stage0/stdlib/Init/Coe.c b/stage0/stdlib/Init/Coe.c index 4088f165e0..a535b189f0 100644 --- a/stage0/stdlib/Init/Coe.c +++ b/stage0/stdlib/Init/Coe.c @@ -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; } } diff --git a/stage0/stdlib/Init/Control/Basic.c b/stage0/stdlib/Init/Control/Basic.c index aa23c2695c..c47f304cfa 100644 --- a/stage0/stdlib/Init/Control/Basic.c +++ b/stage0/stdlib/Init/Control/Basic.c @@ -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); diff --git a/stage0/stdlib/Init/Control/Reader.c b/stage0/stdlib/Init/Control/Reader.c index 09e6e7e1d7..b866b29d8a 100644 --- a/stage0/stdlib/Init/Control/Reader.c +++ b/stage0/stdlib/Init/Control/Reader.c @@ -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); diff --git a/stage0/stdlib/Init/Meta.c b/stage0/stdlib/Init/Meta.c index 91655a4de9..91c95f231a 100644 --- a/stage0/stdlib/Init/Meta.c +++ b/stage0/stdlib/Init/Meta.c @@ -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); diff --git a/stage0/stdlib/Init/Prelude.c b/stage0/stdlib/Init/Prelude.c index 5b08c1c233..ee9bab7434 100644 --- a/stage0/stdlib/Init/Prelude.c +++ b/stage0/stdlib/Init/Prelude.c @@ -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); diff --git a/stage0/stdlib/Lean/Data/Options.c b/stage0/stdlib/Lean/Data/Options.c index 993b355cf3..09dd5c9590 100644 --- a/stage0/stdlib/Lean/Data/Options.c +++ b/stage0/stdlib/Lean/Data/Options.c @@ -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; } } diff --git a/stage0/stdlib/Lean/Elab/App.c b/stage0/stdlib/Lean/Elab/App.c index 58817c750b..9218b0ecde 100644 --- a/stage0/stdlib/Lean/Elab/App.c +++ b/stage0/stdlib/Lean/Elab/App.c @@ -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); diff --git a/stage0/stdlib/Lean/Elab/Binders.c b/stage0/stdlib/Lean/Elab/Binders.c index e9ccea3dab..7ebff43923 100644 --- a/stage0/stdlib/Lean/Elab/Binders.c +++ b/stage0/stdlib/Lean/Elab/Binders.c @@ -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; } diff --git a/stage0/stdlib/Lean/Elab/InfoTree.c b/stage0/stdlib/Lean/Elab/InfoTree.c index 8813654fb7..4c8b11c37b 100644 --- a/stage0/stdlib/Lean/Elab/InfoTree.c +++ b/stage0/stdlib/Lean/Elab/InfoTree.c @@ -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); diff --git a/stage0/stdlib/Lean/Elab/Log.c b/stage0/stdlib/Lean/Elab/Log.c index a40d6b3971..21351a8331 100644 --- a/stage0/stdlib/Lean/Elab/Log.c +++ b/stage0/stdlib/Lean/Elab/Log.c @@ -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); diff --git a/stage0/stdlib/Lean/Elab/Match.c b/stage0/stdlib/Lean/Elab/Match.c index 1ab9e4379d..847f830fb4 100644 --- a/stage0/stdlib/Lean/Elab/Match.c +++ b/stage0/stdlib/Lean/Elab/Match.c @@ -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) diff --git a/stage0/stdlib/Lean/Elab/PreDefinition/Main.c b/stage0/stdlib/Lean/Elab/PreDefinition/Main.c index 6da1e395d6..dde4aa8b15 100644 --- a/stage0/stdlib/Lean/Elab/PreDefinition/Main.c +++ b/stage0/stdlib/Lean/Elab/PreDefinition/Main.c @@ -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) { diff --git a/stage0/stdlib/Lean/Elab/Term.c b/stage0/stdlib/Lean/Elab/Term.c index 578c62754f..f68144e9c6 100644 --- a/stage0/stdlib/Lean/Elab/Term.c +++ b/stage0/stdlib/Lean/Elab/Term.c @@ -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; } diff --git a/stage0/stdlib/Lean/Elab/Util.c b/stage0/stdlib/Lean/Elab/Util.c index 8d7ae4731c..63b024d7ff 100644 --- a/stage0/stdlib/Lean/Elab/Util.c +++ b/stage0/stdlib/Lean/Elab/Util.c @@ -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); diff --git a/stage0/stdlib/Lean/Environment.c b/stage0/stdlib/Lean/Environment.c index 0cf7c3f426..365102bec2 100644 --- a/stage0/stdlib/Lean/Environment.c +++ b/stage0/stdlib/Lean/Environment.c @@ -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); diff --git a/stage0/stdlib/Lean/LocalContext.c b/stage0/stdlib/Lean/LocalContext.c index ec65a5d399..2630d717c3 100644 --- a/stage0/stdlib/Lean/LocalContext.c +++ b/stage0/stdlib/Lean/LocalContext.c @@ -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; } } diff --git a/stage0/stdlib/Lean/Message.c b/stage0/stdlib/Lean/Message.c index 19ba4bbbaa..72c091a031 100644 --- a/stage0/stdlib/Lean/Message.c +++ b/stage0/stdlib/Lean/Message.c @@ -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(); diff --git a/stage0/stdlib/Lean/Meta/Basic.c b/stage0/stdlib/Lean/Meta/Basic.c index 251c980964..9fa48bc59f 100644 --- a/stage0/stdlib/Lean/Meta/Basic.c +++ b/stage0/stdlib/Lean/Meta/Basic.c @@ -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: { diff --git a/stage0/stdlib/Lean/Meta/ExprDefEq.c b/stage0/stdlib/Lean/Meta/ExprDefEq.c index a74ad2bb03..51e6e8ed56 100644 --- a/stage0/stdlib/Lean/Meta/ExprDefEq.c +++ b/stage0/stdlib/Lean/Meta/ExprDefEq.c @@ -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(); diff --git a/stage0/stdlib/Lean/Meta/LevelDefEq.c b/stage0/stdlib/Lean/Meta/LevelDefEq.c index de57d89579..ff6335ad1a 100644 --- a/stage0/stdlib/Lean/Meta/LevelDefEq.c +++ b/stage0/stdlib/Lean/Meta/LevelDefEq.c @@ -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; } diff --git a/stage0/stdlib/Lean/Meta/Tactic/Intro.c b/stage0/stdlib/Lean/Meta/Tactic/Intro.c index b022551c4e..22fc41e445 100644 --- a/stage0/stdlib/Lean/Meta/Tactic/Intro.c +++ b/stage0/stdlib/Lean/Meta/Tactic/Intro.c @@ -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; } diff --git a/stage0/stdlib/Lean/MetavarContext.c b/stage0/stdlib/Lean/MetavarContext.c index 8362d132c3..355773ff5c 100644 --- a/stage0/stdlib/Lean/MetavarContext.c +++ b/stage0/stdlib/Lean/MetavarContext.c @@ -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); diff --git a/stage0/stdlib/Lean/PrettyPrinter/Delaborator/Basic.c b/stage0/stdlib/Lean/PrettyPrinter/Delaborator/Basic.c index 9bdaf9449b..98ef0e6562 100644 --- a/stage0/stdlib/Lean/PrettyPrinter/Delaborator/Basic.c +++ b/stage0/stdlib/Lean/PrettyPrinter/Delaborator/Basic.c @@ -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; } diff --git a/stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c b/stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c index d4ed9296e5..2e8c1f4158 100644 --- a/stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c +++ b/stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c @@ -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; diff --git a/stage0/stdlib/Lean/ResolveName.c b/stage0/stdlib/Lean/ResolveName.c index 9f3723ce49..c55678d862 100644 --- a/stage0/stdlib/Lean/ResolveName.c +++ b/stage0/stdlib/Lean/ResolveName.c @@ -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); diff --git a/stage0/stdlib/Lean/Util/MonadCache.c b/stage0/stdlib/Lean/Util/MonadCache.c index 303bcd6bda..cf1b4455ca 100644 --- a/stage0/stdlib/Lean/Util/MonadCache.c +++ b/stage0/stdlib/Lean/Util/MonadCache.c @@ -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; } } diff --git a/stage0/stdlib/Lean/Util/Trace.c b/stage0/stdlib/Lean/Util/Trace.c index f5b85fefe4..c9194e6b35 100644 --- a/stage0/stdlib/Lean/Util/Trace.c +++ b/stage0/stdlib/Lean/Util/Trace.c @@ -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));