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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2021-02-28 09:03:47 -08:00
parent ef4d5950ae
commit 4483f85495
35 changed files with 2053 additions and 656 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -12,3 +12,5 @@ import Init.Control.Except
import Init.Control.Reader
import Init.Control.Option
import Init.Control.Lawful
import Init.Control.StateCps
import Init.Control.ExceptCps

68
stage0/src/Init/Control/ExceptCps.lean generated Normal file
View file

@ -0,0 +1,68 @@
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Control.Lawful
/-
The Exception monad transformer using CPS style.
-/
def ExceptCpsT (ε : Type u) (m : Type u → Type v) (α : Type u) := (β : Type u) → (α → m β) → (ε → m β) → m β
namespace ExceptCpsT
@[inline] def run {ε α : Type u} [Monad m] (x : ExceptCpsT ε m α) : m (Except ε α) :=
x _ (fun a => pure (Except.ok a)) (fun e => pure (Except.error e))
@[inline] def runK {ε α : Type u} (x : ExceptCpsT ε m α) (s : ε) (ok : α → m β) (error : ε → m β) : m β :=
x _ ok error
@[inline] def runCatch [Monad m] (x : ExceptCpsT α m α) : m α :=
x _ pure pure
instance : Monad (ExceptCpsT ε m) where
map f x := fun _ k₁ k₂ => x _ (fun a => k₁ (f a)) k₂
pure a := fun _ k _ => k a
bind x f := fun _ k₁ k₂ => x _ (fun a => f a _ k₁ k₂) k₂
instance : LawfulMonad (ExceptCpsT σ m) := by
refine! { .. } <;> intros <;> rfl
instance : MonadExceptOf ε (ExceptCpsT ε m) where
throw e := fun _ _ k => k e
tryCatch x handle := fun _ k₁ k₂ => x _ k₁ (fun e => handle e _ k₁ k₂)
@[inline] def lift [Monad m] (x : m α) : ExceptCpsT ε m α :=
fun _ k _ => x >>= k
instance [Monad m] : MonadLift m (ExceptCpsT σ m) where
monadLift := ExceptCpsT.lift
instance [Inhabited ε] : Inhabited (ExceptCpsT ε m α) where
default := fun _ k₁ k₂ => k₂ arbitrary
@[simp] theorem run_pure [Monad m] : run (pure x : ExceptCpsT ε m α) = pure (Except.ok x) := rfl
@[simp] theorem run_lift {α ε : Type u} [Monad m] (x : m α) : run (ExceptCpsT.lift x : ExceptCpsT ε m α) = x >>= fun a => pure (Except.ok a) := rfl
@[simp] theorem run_throw [Monad m] : run (throw e : ExceptCpsT ε m β) = pure (Except.error e) := rfl
@[simp] theorem run_bind_lift [Monad m] (x : m α) (f : α → ExceptCpsT ε m β) : run (ExceptCpsT.lift x >>= f : ExceptCpsT ε m β) = x >>= fun a => run (f a) := rfl
@[simp] theorem run_bind_throw [Monad m] (e : ε) (f : α → ExceptCpsT ε m β) : run (throw e >>= f : ExceptCpsT ε m β) = run (throw e) := rfl
@[simp] theorem runCatch_pure [Monad m] : runCatch (pure x : ExceptCpsT α m α) = pure x := rfl
@[simp] theorem runCatch_lift {α : Type u} [Monad m] [LawfulMonad m] (x : m α) : runCatch (ExceptCpsT.lift x : ExceptCpsT α m α) = x := by
simp [runCatch, lift]
@[simp] theorem runCatch_throw [Monad m] : runCatch (throw a : ExceptCpsT α m α) = pure a := rfl
@[simp] theorem runCatch_bind_lift [Monad m] (x : m α) (f : α → ExceptCpsT β m β) : runCatch (ExceptCpsT.lift x >>= f : ExceptCpsT β m β) = x >>= fun a => runCatch (f a) := rfl
@[simp] theorem runCatch_bind_throw [Monad m] (e : β) (f : α → ExceptCpsT β m β) : runCatch (throw e >>= f : ExceptCpsT β m β) = pure e := rfl
end ExceptCpsT

20
stage0/src/Init/Control/Foldable.lean generated Normal file
View file

@ -0,0 +1,20 @@
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Core
/-
Typeclass for the polymorphic `foldlM` operation described in the paper.
Remark:
- `γ` is a "container" type of elements of type `α`.
- `α` is treated as an output parameter by the typeclass resolution procedure.
That is, it tries to find an instance using only `m` and `γ`.
-/
class Foldable (m : Type u → Type v) (γ : Type w₁) (α : outParam (Type w₂)) where
foldlM [Monad m] : (δ → α → m δ) → δ → γ → m δ
-- Add the alias `foldlM` for `Foldable.foldlM`
export Foldable (foldlM)

69
stage0/src/Init/Control/StateCps.lean generated Normal file
View file

@ -0,0 +1,69 @@
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Control.Lawful
/-
The State monad transformer using CPS style.
-/
def StateCpsT (σ : Type u) (m : Type u → Type v) (α : Type u) := (δ : Type u) → σ → (α → σ → m δ) → m δ
namespace StateCpsT
@[inline] def run {α σ : Type u} {m : Type u → Type v} [Monad m] (x : StateCpsT σ m α) (s : σ) : m (α × σ) :=
x _ s fun a s => pure (a, s)
@[inline] def run' {α σ : Type u} {m : Type u → Type v} [Monad m] (x : StateCpsT σ m α) (s : σ) : m α :=
(·.1) <$> run x s
@[inline] def runK {α σ : Type u} {m : Type u → Type v} (x : StateCpsT σ m α) (s : σ) (k : α → σ → m β) : m β :=
x _ s k
instance : Monad (StateCpsT σ m) where
map f x := fun δ s k => x δ s fun a s => k (f a) s
pure a := fun δ s k => k a s
bind x f := fun δ s k => x δ s fun a s => f a δ s k
instance : LawfulMonad (StateCpsT σ m) := by
refine! { .. } <;> intros <;> rfl
instance : MonadStateOf σ (StateCpsT σ m) where
get := fun δ s k => k s s
set s := fun δ _ k => k ⟨⟩ s
modifyGet f := fun _ s k => let (a, s) := f s; k a s
@[inline] protected def lift [Monad m] (x : m α) : StateCpsT σ m α :=
fun _ s k => x >>= (k . s)
instance [Monad m] : MonadLift m (StateCpsT σ m) where
monadLift := StateCpsT.lift
@[simp] theorem run'_eq [Monad m] (x : StateCpsT σ m α) (s : σ) : x.run' s = (·.1) <$> run x s := rfl
@[simp] theorem run_get [Monad m] (s : σ) : (get : StateCpsT σ m σ).run s = pure (s, s) := rfl
@[simp] theorem run_set [Monad m] (s s' : σ) : (set s' : StateCpsT σ m PUnit).run s = pure (⟨⟩, s') := rfl
@[simp] theorem run_modify [Monad m] (f : σ → σ) (s : σ) : (modify f : StateCpsT σ m PUnit).run s = pure (⟨⟩, f s) := rfl
@[simp] theorem run_lift {α σ : Type u} [Monad m] (x : m α) (s : σ) : (StateCpsT.lift x : StateCpsT σ m α).run s = x >>= fun a => pure (a, s) := rfl
@[simp] theorem run_bind_pure {α σ : Type u} [Monad m] (a : α) (f : α → StateCpsT σ m β) (s : σ) : (pure a >>= f).run s = (f a).run s := rfl
@[simp] theorem run_bind_lift {α σ : Type u} [Monad m] (x : m α) (f : α → StateCpsT σ m β) (s : σ) : (StateCpsT.lift x >>= f).run s = x >>= fun a => (f a).run s := rfl
@[simp] theorem run_bind_get {σ : Type u} [Monad m] (f : σ → StateCpsT σ m β) (s : σ) : (get >>= f).run s = (f s).run s := rfl
@[simp] theorem run_bind_set {σ : Type u} [Monad m] (f : PUnit → StateCpsT σ m β) (s s' : σ) : (set s' >>= f).run s = (f ⟨⟩).run s' := rfl
@[simp] theorem run_bind_modify {σ : Type u} [Monad m] (f : σ → σ) (g : PUnit → StateCpsT σ m β) (s : σ) : (modify f >>= g).run s = (g ⟨⟩).run (f s) := rfl
@[simp] theorem run_monadLift {σ : Type u} [Monad m] [MonadLiftT n m] (x : n α) (s : σ) : (monadLift x : StateCpsT σ m α).run s = (monadLift x : m α) >>= fun a => pure (a, s) := rfl
@[simp] theorem run_pure [Monad m] (a : α) (s : σ) : (pure a : StateCpsT σ m α).run s = pure (a, s) := rfl
end StateCpsT

10
stage0/src/Init/Data/List/Control.lean generated
View file

@ -5,6 +5,7 @@ Author: Leonardo de Moura
-/
prelude
import Init.Control.Basic
import Init.Control.Foldable
import Init.Data.List.Basic
namespace List
@ -149,4 +150,13 @@ def findSomeM? {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f
instance : ForIn m (List α) α where
forIn := List.forIn
instance : Foldable m (List α) α where
foldlM := List.foldlM
-- Add two simplification lemmas for `foldlM` over lists
@[simp] theorem foldlM_nil [Monad m] (f : δ → α → m δ) (d : δ) : foldlM f d ([] : List α) = pure d :=
rfl
@[simp] theorem foldlM_cons [Monad m] (f : δ → α → m δ) (d : δ) (a : α) (as : List α) : foldlM f d (a::as) = f d a >>= fun d => foldlM f d as :=
rfl
end List

16
stage0/src/Init/Data/Range.lean generated
View file

@ -5,6 +5,7 @@ Authors: Leonardo de Moura
-/
prelude
import Init.Meta
import Init.Control.Foldable
namespace Std
-- We put `Range` in `Init` because we want the notation `[i:j]` without importing `Std`
@ -28,12 +29,21 @@ universes u v
| ForInStep.yield b => loop i (j + range.step) b
loop range.stop range.start init
@[inline] protected def foldlM {β : Type u} {m : Type u → Type v} [Monad m] (f : β → Nat → m β) (init : β) (range : Range) : m β :=
range.forIn init (fun i b => return ForInStep.yield (← f b i))
instance : ForIn m Range Nat where
forIn := Range.forIn
@[inline] protected def foldlM {β : Type u} {m : Type u → Type v} [Monad m] (f : β → Nat → m β) (init : β) (range : Range) : m β :=
let rec @[specialize] loop (i : Nat) (j : Nat) (b : β) : m β := do
if j ≥ range.stop then
pure b
else match i with
| 0 => pure b
| i+1 => loop i (j + range.step) (← f b j)
loop range.stop range.start init
instance : Foldable m Range Nat where
foldlM := Range.foldlM
syntax:max "[" ":" term "]" : term
syntax:max "[" term ":" term "]" : term
syntax:max "[" ":" term ":" term "]" : term

26
stage0/src/library/compiler/specialize.cpp generated
View file

@ -869,7 +869,7 @@ class specialize_fn {
return r;
}
comp_decl mk_new_decl(comp_decl const & pre_decl, buffer<expr> const & fvars, buffer<expr> const & fvar_vals, spec_ctx & ctx) {
optional<comp_decl> mk_new_decl(comp_decl const & pre_decl, buffer<expr> const & fvars, buffer<expr> const & fvar_vals, spec_ctx & ctx) {
lean_assert(fvars.size() == fvar_vals.size());
name n = pre_decl.fst();
expr code = pre_decl.snd();
@ -889,8 +889,8 @@ class specialize_fn {
}
}
code = m_lctx.mk_lambda(new_let_decls, code);
// lean_trace(name("compiler", "spec_info"), tout() << "STEP 1 " << n << "\n" << code << "\n";);
code = abstract_spec_ctx(ctx, code);
lean_trace(name("compiler", "spec_info"), tout() << "specialized code " << n << "\n" << trace_pp_expr(code) << "\n";);
lean_assert(!has_fvar(code));
/* We add the auxiliary declaration `n` as a "meta" axiom to the environment.
This is a hack to make sure we can use `csimp` to simplify `code` and
@ -905,10 +905,18 @@ class specialize_fn {
type checker that takes the types of auxiliary declarations such as `n` into account.
A custom type checker would be extra work, but it has other benefits. For example,
it could have better support for type errors introduced by `csimp`. */
{
try {
expr type = cheap_beta_reduce(type_checker(m_st).infer(code));
declaration aux_ax = mk_axiom(n, names(), type, true /* meta */);
m_st.env() = env().add(aux_ax, false);
} catch (exception &) {
/* We may fail to infer the type of code, since it may be recursive
This is a workaround. When we re-implement the compiler in Lean,
we should write code to infer type that tolerates undefined constants,
*AnyType*, etc.
We just do not specialize when we cannot infer the type. */
return optional<comp_decl>();
}
code = eta_expand_specialization(code);
// lean_trace(name("compiler", "spec_info"), tout() << "STEP 2 " << n << "\n" << code << "\n";);
@ -917,7 +925,7 @@ class specialize_fn {
lean_trace(name("compiler", "specialize"), tout() << "new code " << n << "\n" << trace_pp_expr(code) << "\n";);
comp_decl new_decl(n, code);
m_new_decls.push_back(new_decl);
return new_decl;
return optional<comp_decl>(new_decl);
}
optional<expr> get_closed(expr const & e) {
@ -1046,12 +1054,16 @@ class specialize_fn {
return none_expr();
buffer<comp_decl> new_decls;
for (comp_decl const & pre_decl : ctx.m_pre_decls) {
new_decls.push_back(mk_new_decl(pre_decl, fvars, fvar_vals, ctx));
if (respecialize) {
m_to_respecialize.insert(pre_decl.fst());
if (auto new_decl_opt = mk_new_decl(pre_decl, fvars, fvar_vals, ctx)) {
new_decls.push_back(*new_decl_opt);
} else {
return none_expr();
}
}
if (respecialize) {
for (comp_decl const & new_decl : new_decls) {
m_to_respecialize.insert(new_decl.fst());
}
m_st.env() = update_spec_info(env(), new_decls);
}
if (gcache_enabled) {

2
stage0/stdlib/CMakeLists.txt generated
View file

File diff suppressed because one or more lines are too long

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

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Control
// Imports: Init.Control.Basic Init.Control.State Init.Control.StateRef Init.Control.Id Init.Control.Except Init.Control.Reader Init.Control.Option Init.Control.Lawful
// Imports: Init.Control.Basic Init.Control.State Init.Control.StateRef Init.Control.Id Init.Control.Except Init.Control.Reader Init.Control.Option Init.Control.Lawful Init.Control.StateCps Init.Control.ExceptCps
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -21,6 +21,8 @@ lean_object* initialize_Init_Control_Except(lean_object*);
lean_object* initialize_Init_Control_Reader(lean_object*);
lean_object* initialize_Init_Control_Option(lean_object*);
lean_object* initialize_Init_Control_Lawful(lean_object*);
lean_object* initialize_Init_Control_StateCps(lean_object*);
lean_object* initialize_Init_Control_ExceptCps(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Control(lean_object* w) {
lean_object * res;
@ -50,6 +52,12 @@ lean_dec_ref(res);
res = initialize_Init_Control_Lawful(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Control_StateCps(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Control_ExceptCps(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

576
stage0/stdlib/Init/Control/ExceptCps.c generated Normal file
View file

@ -0,0 +1,576 @@
// Lean compiler output
// Module: Init.Control.ExceptCps
// Imports: Init.Control.Lawful
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
#ifdef __cplusplus
extern "C" {
#endif
lean_object* l_ExceptCpsT_lift___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instMonadExceptCpsT___lambda__9(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instMonadExceptOfExceptCpsT___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_lift(lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instMonadExceptOfExceptCpsT___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instInhabitedExceptCpsT___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instMonadExceptCpsT___lambda__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instMonadExceptCpsT___closed__1;
lean_object* l_ExceptCpsT_instMonadLiftExceptCpsT(lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instMonadExceptCpsT___closed__6;
lean_object* l_observing___rarg___lambda__1(lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instMonadExceptCpsT___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instMonadExceptCpsT___closed__8;
lean_object* l_ExceptCpsT_instMonadLiftExceptCpsT___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_instMonadReaderT___rarg___lambda__7___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instMonadExceptCpsT___closed__2;
lean_object* l_ExceptCpsT_instMonadLiftExceptCpsT___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instMonadExceptCpsT___closed__4;
lean_object* l_ExceptCpsT_instMonadExceptCpsT___lambda__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_runCatch(lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instMonadExceptCpsT___closed__9;
lean_object* l_ExceptCpsT_runK___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instMonadExceptCpsT___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instMonadExceptOfExceptCpsT___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instMonadExceptCpsT___lambda__11(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instMonadExceptCpsT___lambda__12(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_run___rarg(lean_object*, lean_object*);
lean_object* l_ExceptCpsT_runK(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_run(lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instInhabitedExceptCpsT(lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instMonadExceptCpsT___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instMonadExceptCpsT___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instMonadExceptCpsT___lambda__7(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_runK___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instInhabitedExceptCpsT___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instMonadExceptCpsT___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instMonadExceptCpsT___lambda__8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instMonadExceptCpsT___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instMonadExceptCpsT___closed__10;
lean_object* l_ExceptCpsT_lift___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instMonadExceptOfExceptCpsT___closed__3;
lean_object* l_ExceptCpsT_instMonadExceptCpsT___lambda__10(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instMonadExceptCpsT___closed__3;
lean_object* l_ExceptCpsT_instMonadExceptOfExceptCpsT(lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instMonadExceptOfExceptCpsT___closed__1;
lean_object* l_ExceptCpsT_runCatch___rarg(lean_object*, lean_object*);
lean_object* l_observing___rarg___lambda__2(lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instMonadExceptOfExceptCpsT___closed__2;
lean_object* l_ExceptCpsT_instMonadExceptCpsT(lean_object*, lean_object*);
lean_object* l_ExceptCpsT_instMonadExceptCpsT___closed__7;
lean_object* l_ExceptCpsT_instMonadExceptCpsT___closed__5;
lean_object* l_ExceptCpsT_run___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);
x_3 = lean_alloc_closure((void*)(l_observing___rarg___lambda__1), 2, 1);
lean_closure_set(x_3, 0, x_1);
x_4 = lean_alloc_closure((void*)(l_observing___rarg___lambda__2), 2, 1);
lean_closure_set(x_4, 0, x_1);
x_5 = lean_apply_3(x_2, lean_box(0), x_3, x_4);
return x_5;
}
}
lean_object* l_ExceptCpsT_run(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_ExceptCpsT_run___rarg), 2, 0);
return x_4;
}
}
lean_object* l_ExceptCpsT_runK___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = lean_apply_3(x_1, lean_box(0), x_3, x_4);
return x_5;
}
}
lean_object* l_ExceptCpsT_runK(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = lean_alloc_closure((void*)(l_ExceptCpsT_runK___rarg___boxed), 4, 0);
return x_5;
}
}
lean_object* l_ExceptCpsT_runK___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_ExceptCpsT_runK___rarg(x_1, x_2, x_3, x_4);
lean_dec(x_2);
return x_5;
}
}
lean_object* l_ExceptCpsT_runCatch___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);
lean_inc(x_3);
lean_dec(x_1);
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
lean_dec(x_3);
x_5 = lean_apply_1(x_4, lean_box(0));
lean_inc(x_5);
x_6 = lean_apply_3(x_2, lean_box(0), x_5, x_5);
return x_6;
}
}
lean_object* l_ExceptCpsT_runCatch(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_ExceptCpsT_runCatch___rarg), 2, 0);
return x_3;
}
}
lean_object* l_ExceptCpsT_instMonadExceptCpsT___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_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);
return x_5;
}
}
lean_object* l_ExceptCpsT_instMonadExceptCpsT___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8; lean_object* x_9;
x_8 = lean_alloc_closure((void*)(l_ExceptCpsT_instMonadExceptCpsT___lambda__1), 3, 2);
lean_closure_set(x_8, 0, x_3);
lean_closure_set(x_8, 1, x_6);
x_9 = lean_apply_3(x_4, lean_box(0), x_8, x_7);
return x_9;
}
}
lean_object* l_ExceptCpsT_instMonadExceptCpsT___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8; lean_object* x_9;
x_8 = lean_alloc_closure((void*)(l_ReaderT_instMonadReaderT___rarg___lambda__7___boxed), 3, 2);
lean_closure_set(x_8, 0, x_6);
lean_closure_set(x_8, 1, x_3);
x_9 = lean_apply_3(x_4, lean_box(0), x_8, x_7);
return x_9;
}
}
lean_object* l_ExceptCpsT_instMonadExceptCpsT___lambda__4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = lean_apply_1(x_4, x_2);
return x_6;
}
}
lean_object* l_ExceptCpsT_instMonadExceptCpsT___lambda__5(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6;
x_5 = lean_alloc_closure((void*)(l_ExceptCpsT_instMonadExceptCpsT___lambda__1), 3, 2);
lean_closure_set(x_5, 0, x_4);
lean_closure_set(x_5, 1, x_1);
x_6 = lean_apply_3(x_2, lean_box(0), x_5, x_3);
return x_6;
}
}
lean_object* l_ExceptCpsT_instMonadExceptCpsT___lambda__6(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8; lean_object* x_9;
lean_inc(x_7);
x_8 = lean_alloc_closure((void*)(l_ExceptCpsT_instMonadExceptCpsT___lambda__5), 4, 3);
lean_closure_set(x_8, 0, x_6);
lean_closure_set(x_8, 1, x_4);
lean_closure_set(x_8, 2, x_7);
x_9 = lean_apply_3(x_3, lean_box(0), x_8, x_7);
return x_9;
}
}
lean_object* l_ExceptCpsT_instMonadExceptCpsT___lambda__7(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6;
x_5 = lean_alloc_closure((void*)(l_ReaderT_instMonadReaderT___rarg___lambda__7___boxed), 3, 2);
lean_closure_set(x_5, 0, x_1);
lean_closure_set(x_5, 1, x_4);
x_6 = lean_apply_3(x_2, lean_box(0), x_5, x_3);
return x_6;
}
}
lean_object* l_ExceptCpsT_instMonadExceptCpsT___lambda__8(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8; lean_object* x_9;
lean_inc(x_7);
x_8 = lean_alloc_closure((void*)(l_ExceptCpsT_instMonadExceptCpsT___lambda__7), 4, 3);
lean_closure_set(x_8, 0, x_6);
lean_closure_set(x_8, 1, x_4);
lean_closure_set(x_8, 2, x_7);
x_9 = lean_apply_3(x_3, lean_box(0), x_8, x_7);
return x_9;
}
}
lean_object* l_ExceptCpsT_instMonadExceptCpsT___lambda__9(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = lean_apply_3(x_1, lean_box(0), x_2, x_3);
return x_5;
}
}
lean_object* l_ExceptCpsT_instMonadExceptCpsT___lambda__10(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8; lean_object* x_9;
lean_inc(x_7);
x_8 = lean_alloc_closure((void*)(l_ExceptCpsT_instMonadExceptCpsT___lambda__9___boxed), 4, 3);
lean_closure_set(x_8, 0, x_4);
lean_closure_set(x_8, 1, x_6);
lean_closure_set(x_8, 2, x_7);
x_9 = lean_apply_3(x_3, lean_box(0), x_8, x_7);
return x_9;
}
}
lean_object* l_ExceptCpsT_instMonadExceptCpsT___lambda__11(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = lean_apply_4(x_1, x_4, lean_box(0), x_2, x_3);
return x_5;
}
}
lean_object* l_ExceptCpsT_instMonadExceptCpsT___lambda__12(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8; lean_object* x_9;
lean_inc(x_7);
x_8 = lean_alloc_closure((void*)(l_ExceptCpsT_instMonadExceptCpsT___lambda__11), 4, 3);
lean_closure_set(x_8, 0, x_4);
lean_closure_set(x_8, 1, x_6);
lean_closure_set(x_8, 2, x_7);
x_9 = lean_apply_3(x_3, lean_box(0), x_8, x_7);
return x_9;
}
}
static lean_object* _init_l_ExceptCpsT_instMonadExceptCpsT___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_ExceptCpsT_instMonadExceptCpsT___lambda__2), 7, 0);
return x_1;
}
}
static lean_object* _init_l_ExceptCpsT_instMonadExceptCpsT___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_ExceptCpsT_instMonadExceptCpsT___lambda__3), 7, 0);
return x_1;
}
}
static lean_object* _init_l_ExceptCpsT_instMonadExceptCpsT___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_ExceptCpsT_instMonadExceptCpsT___closed__1;
x_2 = l_ExceptCpsT_instMonadExceptCpsT___closed__2;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_ExceptCpsT_instMonadExceptCpsT___closed__4() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_ExceptCpsT_instMonadExceptCpsT___lambda__4___boxed), 5, 0);
return x_1;
}
}
static lean_object* _init_l_ExceptCpsT_instMonadExceptCpsT___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_ExceptCpsT_instMonadExceptCpsT___lambda__6), 7, 0);
return x_1;
}
}
static lean_object* _init_l_ExceptCpsT_instMonadExceptCpsT___closed__6() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_ExceptCpsT_instMonadExceptCpsT___lambda__8), 7, 0);
return x_1;
}
}
static lean_object* _init_l_ExceptCpsT_instMonadExceptCpsT___closed__7() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_ExceptCpsT_instMonadExceptCpsT___lambda__10), 7, 0);
return x_1;
}
}
static lean_object* _init_l_ExceptCpsT_instMonadExceptCpsT___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_ExceptCpsT_instMonadExceptCpsT___closed__3;
x_2 = l_ExceptCpsT_instMonadExceptCpsT___closed__4;
x_3 = l_ExceptCpsT_instMonadExceptCpsT___closed__5;
x_4 = l_ExceptCpsT_instMonadExceptCpsT___closed__6;
x_5 = l_ExceptCpsT_instMonadExceptCpsT___closed__7;
x_6 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_6, 0, x_1);
lean_ctor_set(x_6, 1, x_2);
lean_ctor_set(x_6, 2, x_3);
lean_ctor_set(x_6, 3, x_4);
lean_ctor_set(x_6, 4, x_5);
return x_6;
}
}
static lean_object* _init_l_ExceptCpsT_instMonadExceptCpsT___closed__9() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_ExceptCpsT_instMonadExceptCpsT___lambda__12), 7, 0);
return x_1;
}
}
static lean_object* _init_l_ExceptCpsT_instMonadExceptCpsT___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_ExceptCpsT_instMonadExceptCpsT___closed__8;
x_2 = l_ExceptCpsT_instMonadExceptCpsT___closed__9;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* l_ExceptCpsT_instMonadExceptCpsT(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_ExceptCpsT_instMonadExceptCpsT___closed__10;
return x_3;
}
}
lean_object* l_ExceptCpsT_instMonadExceptCpsT___lambda__4___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = l_ExceptCpsT_instMonadExceptCpsT___lambda__4(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_5);
return x_6;
}
}
lean_object* l_ExceptCpsT_instMonadExceptCpsT___lambda__9___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_ExceptCpsT_instMonadExceptCpsT___lambda__9(x_1, x_2, x_3, x_4);
lean_dec(x_4);
return x_5;
}
}
lean_object* l_ExceptCpsT_instMonadExceptOfExceptCpsT___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = lean_apply_1(x_5, x_2);
return x_6;
}
}
lean_object* l_ExceptCpsT_instMonadExceptOfExceptCpsT___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7; lean_object* x_8;
lean_inc(x_5);
x_7 = lean_alloc_closure((void*)(l_ExceptCpsT_instMonadExceptCpsT___lambda__11), 4, 3);
lean_closure_set(x_7, 0, x_3);
lean_closure_set(x_7, 1, x_5);
lean_closure_set(x_7, 2, x_6);
x_8 = lean_apply_3(x_2, lean_box(0), x_5, x_7);
return x_8;
}
}
static lean_object* _init_l_ExceptCpsT_instMonadExceptOfExceptCpsT___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_ExceptCpsT_instMonadExceptOfExceptCpsT___lambda__1___boxed), 5, 0);
return x_1;
}
}
static lean_object* _init_l_ExceptCpsT_instMonadExceptOfExceptCpsT___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_ExceptCpsT_instMonadExceptOfExceptCpsT___lambda__2), 6, 0);
return x_1;
}
}
static lean_object* _init_l_ExceptCpsT_instMonadExceptOfExceptCpsT___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_ExceptCpsT_instMonadExceptOfExceptCpsT___closed__1;
x_2 = l_ExceptCpsT_instMonadExceptOfExceptCpsT___closed__2;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* l_ExceptCpsT_instMonadExceptOfExceptCpsT(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_ExceptCpsT_instMonadExceptOfExceptCpsT___closed__3;
return x_3;
}
}
lean_object* l_ExceptCpsT_instMonadExceptOfExceptCpsT___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = l_ExceptCpsT_instMonadExceptOfExceptCpsT___lambda__1(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_4);
return x_6;
}
}
lean_object* l_ExceptCpsT_lift___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7;
x_6 = lean_ctor_get(x_1, 1);
lean_inc(x_6);
lean_dec(x_1);
x_7 = lean_apply_4(x_6, lean_box(0), lean_box(0), x_2, x_4);
return x_7;
}
}
lean_object* l_ExceptCpsT_lift(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_ExceptCpsT_lift___rarg___boxed), 5, 0);
return x_4;
}
}
lean_object* l_ExceptCpsT_lift___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = l_ExceptCpsT_lift___rarg(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_5);
return x_6;
}
}
lean_object* l_ExceptCpsT_instMonadLiftExceptCpsT___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7; lean_object* x_8;
x_7 = lean_ctor_get(x_1, 1);
lean_inc(x_7);
lean_dec(x_1);
x_8 = lean_apply_4(x_7, lean_box(0), lean_box(0), x_3, x_5);
return x_8;
}
}
lean_object* l_ExceptCpsT_instMonadLiftExceptCpsT(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_ExceptCpsT_instMonadLiftExceptCpsT___rarg___boxed), 6, 0);
return x_3;
}
}
lean_object* l_ExceptCpsT_instMonadLiftExceptCpsT___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7;
x_7 = l_ExceptCpsT_instMonadLiftExceptCpsT___rarg(x_1, x_2, x_3, x_4, x_5, x_6);
lean_dec(x_6);
return x_7;
}
}
lean_object* l_ExceptCpsT_instInhabitedExceptCpsT___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = lean_apply_1(x_4, x_1);
return x_5;
}
}
lean_object* l_ExceptCpsT_instInhabitedExceptCpsT(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_ExceptCpsT_instInhabitedExceptCpsT___rarg___boxed), 4, 0);
return x_4;
}
}
lean_object* l_ExceptCpsT_instInhabitedExceptCpsT___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_ExceptCpsT_instInhabitedExceptCpsT___rarg(x_1, x_2, x_3, x_4);
lean_dec(x_3);
return x_5;
}
}
lean_object* initialize_Init_Control_Lawful(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Control_ExceptCps(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init_Control_Lawful(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_ExceptCpsT_instMonadExceptCpsT___closed__1 = _init_l_ExceptCpsT_instMonadExceptCpsT___closed__1();
lean_mark_persistent(l_ExceptCpsT_instMonadExceptCpsT___closed__1);
l_ExceptCpsT_instMonadExceptCpsT___closed__2 = _init_l_ExceptCpsT_instMonadExceptCpsT___closed__2();
lean_mark_persistent(l_ExceptCpsT_instMonadExceptCpsT___closed__2);
l_ExceptCpsT_instMonadExceptCpsT___closed__3 = _init_l_ExceptCpsT_instMonadExceptCpsT___closed__3();
lean_mark_persistent(l_ExceptCpsT_instMonadExceptCpsT___closed__3);
l_ExceptCpsT_instMonadExceptCpsT___closed__4 = _init_l_ExceptCpsT_instMonadExceptCpsT___closed__4();
lean_mark_persistent(l_ExceptCpsT_instMonadExceptCpsT___closed__4);
l_ExceptCpsT_instMonadExceptCpsT___closed__5 = _init_l_ExceptCpsT_instMonadExceptCpsT___closed__5();
lean_mark_persistent(l_ExceptCpsT_instMonadExceptCpsT___closed__5);
l_ExceptCpsT_instMonadExceptCpsT___closed__6 = _init_l_ExceptCpsT_instMonadExceptCpsT___closed__6();
lean_mark_persistent(l_ExceptCpsT_instMonadExceptCpsT___closed__6);
l_ExceptCpsT_instMonadExceptCpsT___closed__7 = _init_l_ExceptCpsT_instMonadExceptCpsT___closed__7();
lean_mark_persistent(l_ExceptCpsT_instMonadExceptCpsT___closed__7);
l_ExceptCpsT_instMonadExceptCpsT___closed__8 = _init_l_ExceptCpsT_instMonadExceptCpsT___closed__8();
lean_mark_persistent(l_ExceptCpsT_instMonadExceptCpsT___closed__8);
l_ExceptCpsT_instMonadExceptCpsT___closed__9 = _init_l_ExceptCpsT_instMonadExceptCpsT___closed__9();
lean_mark_persistent(l_ExceptCpsT_instMonadExceptCpsT___closed__9);
l_ExceptCpsT_instMonadExceptCpsT___closed__10 = _init_l_ExceptCpsT_instMonadExceptCpsT___closed__10();
lean_mark_persistent(l_ExceptCpsT_instMonadExceptCpsT___closed__10);
l_ExceptCpsT_instMonadExceptOfExceptCpsT___closed__1 = _init_l_ExceptCpsT_instMonadExceptOfExceptCpsT___closed__1();
lean_mark_persistent(l_ExceptCpsT_instMonadExceptOfExceptCpsT___closed__1);
l_ExceptCpsT_instMonadExceptOfExceptCpsT___closed__2 = _init_l_ExceptCpsT_instMonadExceptOfExceptCpsT___closed__2();
lean_mark_persistent(l_ExceptCpsT_instMonadExceptOfExceptCpsT___closed__2);
l_ExceptCpsT_instMonadExceptOfExceptCpsT___closed__3 = _init_l_ExceptCpsT_instMonadExceptOfExceptCpsT___closed__3();
lean_mark_persistent(l_ExceptCpsT_instMonadExceptOfExceptCpsT___closed__3);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus
}
#endif

29
stage0/stdlib/Init/Control/Foldable.c generated Normal file
View file

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

589
stage0/stdlib/Init/Control/StateCps.c generated Normal file
View file

@ -0,0 +1,589 @@
// Lean compiler output
// Module: Init.Control.StateCps
// Imports: Init.Control.Lawful
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
#ifdef __cplusplus
extern "C" {
#endif
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__10___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__8(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadStateOfStateCpsT___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_StateRefT_x27_run___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadStateCpsT___closed__6;
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadStateOfStateCpsT(lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadLiftStateCpsT(lean_object*, lean_object*);
lean_object* l_StateCpsT_lift___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_lift(lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__13(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_runK___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadStateOfStateCpsT___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadStateCpsT___closed__7;
lean_object* l_StateCpsT_instMonadStateOfStateCpsT_match__1___rarg(lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadStateOfStateCpsT___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadStateCpsT(lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__10(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadStateCpsT___closed__10;
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__12(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_runK(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadStateOfStateCpsT___closed__2;
lean_object* l_StateCpsT_instMonadStateOfStateCpsT___closed__1;
lean_object* l_StateCpsT_run_x27___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadStateOfStateCpsT___closed__4;
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadStateOfStateCpsT___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_run_x27(lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadStateCpsT___closed__3;
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__11(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_run(lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadStateCpsT___closed__8;
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__6(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadStateOfStateCpsT___closed__3;
lean_object* l_StateCpsT_run_x27___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadStateCpsT___closed__5;
lean_object* l_StateCpsT_run___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__9(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadStateCpsT___closed__4;
lean_object* l_ReaderT_instMonadExceptOfReaderT___rarg___lambda__2(lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadStateCpsT___closed__2;
extern lean_object* l_tryFinally___rarg___closed__1;
lean_object* l_StateCpsT_instMonadStateOfStateCpsT_match__1(lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadLiftStateCpsT___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateCpsT_instMonadStateCpsT___closed__9;
lean_object* l_StateCpsT_instMonadStateCpsT___closed__1;
lean_object* l_StateCpsT_run___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5;
x_4 = lean_alloc_closure((void*)(l_StateRefT_x27_run___rarg___lambda__1), 3, 1);
lean_closure_set(x_4, 0, x_1);
x_5 = lean_apply_3(x_2, lean_box(0), x_3, x_4);
return x_5;
}
}
lean_object* l_StateCpsT_run(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_StateCpsT_run___rarg), 3, 0);
return x_4;
}
}
lean_object* l_StateCpsT_run_x27___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = lean_ctor_get(x_1, 1);
lean_inc(x_4);
lean_dec(x_1);
x_5 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_5, 0, x_2);
lean_ctor_set(x_5, 1, x_3);
x_6 = lean_apply_2(x_4, lean_box(0), x_5);
return x_6;
}
}
lean_object* l_StateCpsT_run_x27___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_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;
x_4 = lean_ctor_get(x_1, 0);
lean_inc(x_4);
lean_dec(x_1);
x_5 = lean_ctor_get(x_4, 0);
lean_inc(x_5);
x_6 = lean_ctor_get(x_5, 0);
lean_inc(x_6);
lean_dec(x_5);
x_7 = lean_alloc_closure((void*)(l_StateCpsT_run_x27___rarg___lambda__1), 3, 1);
lean_closure_set(x_7, 0, x_4);
x_8 = lean_apply_3(x_2, lean_box(0), x_3, x_7);
x_9 = l_tryFinally___rarg___closed__1;
x_10 = lean_apply_4(x_6, lean_box(0), lean_box(0), x_9, x_8);
return x_10;
}
}
lean_object* l_StateCpsT_run_x27(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_StateCpsT_run_x27___rarg), 3, 0);
return x_4;
}
}
lean_object* l_StateCpsT_runK___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_apply_3(x_1, lean_box(0), x_2, x_3);
return x_4;
}
}
lean_object* l_StateCpsT_runK(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = lean_alloc_closure((void*)(l_StateCpsT_runK___rarg), 3, 0);
return x_5;
}
}
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6;
x_5 = lean_apply_1(x_1, x_3);
x_6 = lean_apply_2(x_2, x_5, x_4);
return x_6;
}
}
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8; lean_object* x_9;
x_8 = lean_alloc_closure((void*)(l_StateCpsT_instMonadStateCpsT___lambda__1), 4, 2);
lean_closure_set(x_8, 0, x_3);
lean_closure_set(x_8, 1, x_7);
x_9 = lean_apply_3(x_4, lean_box(0), x_6, x_8);
return x_9;
}
}
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = lean_apply_2(x_1, x_2, x_4);
return x_5;
}
}
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8; lean_object* x_9;
x_8 = lean_alloc_closure((void*)(l_StateCpsT_instMonadStateCpsT___lambda__3___boxed), 4, 2);
lean_closure_set(x_8, 0, x_7);
lean_closure_set(x_8, 1, x_3);
x_9 = lean_apply_3(x_4, lean_box(0), x_6, x_8);
return x_9;
}
}
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__5(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = lean_apply_2(x_5, x_2, x_4);
return x_6;
}
}
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__6(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6;
x_5 = lean_alloc_closure((void*)(l_StateCpsT_instMonadStateCpsT___lambda__1), 4, 2);
lean_closure_set(x_5, 0, x_3);
lean_closure_set(x_5, 1, x_1);
x_6 = lean_apply_3(x_2, lean_box(0), x_4, x_5);
return x_6;
}
}
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__7(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8; lean_object* x_9;
x_8 = lean_alloc_closure((void*)(l_StateCpsT_instMonadStateCpsT___lambda__6), 4, 2);
lean_closure_set(x_8, 0, x_7);
lean_closure_set(x_8, 1, x_4);
x_9 = lean_apply_3(x_3, lean_box(0), x_6, x_8);
return x_9;
}
}
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__8(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6;
x_5 = lean_alloc_closure((void*)(l_StateCpsT_instMonadStateCpsT___lambda__3___boxed), 4, 2);
lean_closure_set(x_5, 0, x_1);
lean_closure_set(x_5, 1, x_3);
x_6 = lean_apply_3(x_2, lean_box(0), x_4, x_5);
return x_6;
}
}
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__9(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8; lean_object* x_9;
x_8 = lean_alloc_closure((void*)(l_StateCpsT_instMonadStateCpsT___lambda__8), 4, 2);
lean_closure_set(x_8, 0, x_7);
lean_closure_set(x_8, 1, x_4);
x_9 = lean_apply_3(x_3, lean_box(0), x_6, x_8);
return x_9;
}
}
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__10(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = lean_apply_3(x_1, lean_box(0), x_4, x_2);
return x_5;
}
}
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__11(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8; lean_object* x_9;
x_8 = lean_alloc_closure((void*)(l_StateCpsT_instMonadStateCpsT___lambda__10___boxed), 4, 2);
lean_closure_set(x_8, 0, x_4);
lean_closure_set(x_8, 1, x_7);
x_9 = lean_apply_3(x_3, lean_box(0), x_6, x_8);
return x_9;
}
}
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__12(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = lean_apply_4(x_1, x_3, lean_box(0), x_4, x_2);
return x_5;
}
}
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__13(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8; lean_object* x_9;
x_8 = lean_alloc_closure((void*)(l_StateCpsT_instMonadStateCpsT___lambda__12), 4, 2);
lean_closure_set(x_8, 0, x_4);
lean_closure_set(x_8, 1, x_7);
x_9 = lean_apply_3(x_3, lean_box(0), x_6, x_8);
return x_9;
}
}
static lean_object* _init_l_StateCpsT_instMonadStateCpsT___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_StateCpsT_instMonadStateCpsT___lambda__2), 7, 0);
return x_1;
}
}
static lean_object* _init_l_StateCpsT_instMonadStateCpsT___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_StateCpsT_instMonadStateCpsT___lambda__4), 7, 0);
return x_1;
}
}
static lean_object* _init_l_StateCpsT_instMonadStateCpsT___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_StateCpsT_instMonadStateCpsT___closed__1;
x_2 = l_StateCpsT_instMonadStateCpsT___closed__2;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_StateCpsT_instMonadStateCpsT___closed__4() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_StateCpsT_instMonadStateCpsT___lambda__5), 5, 0);
return x_1;
}
}
static lean_object* _init_l_StateCpsT_instMonadStateCpsT___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_StateCpsT_instMonadStateCpsT___lambda__7), 7, 0);
return x_1;
}
}
static lean_object* _init_l_StateCpsT_instMonadStateCpsT___closed__6() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_StateCpsT_instMonadStateCpsT___lambda__9), 7, 0);
return x_1;
}
}
static lean_object* _init_l_StateCpsT_instMonadStateCpsT___closed__7() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_StateCpsT_instMonadStateCpsT___lambda__11), 7, 0);
return x_1;
}
}
static lean_object* _init_l_StateCpsT_instMonadStateCpsT___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_StateCpsT_instMonadStateCpsT___closed__3;
x_2 = l_StateCpsT_instMonadStateCpsT___closed__4;
x_3 = l_StateCpsT_instMonadStateCpsT___closed__5;
x_4 = l_StateCpsT_instMonadStateCpsT___closed__6;
x_5 = l_StateCpsT_instMonadStateCpsT___closed__7;
x_6 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_6, 0, x_1);
lean_ctor_set(x_6, 1, x_2);
lean_ctor_set(x_6, 2, x_3);
lean_ctor_set(x_6, 3, x_4);
lean_ctor_set(x_6, 4, x_5);
return x_6;
}
}
static lean_object* _init_l_StateCpsT_instMonadStateCpsT___closed__9() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_StateCpsT_instMonadStateCpsT___lambda__13), 7, 0);
return x_1;
}
}
static lean_object* _init_l_StateCpsT_instMonadStateCpsT___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_StateCpsT_instMonadStateCpsT___closed__8;
x_2 = l_StateCpsT_instMonadStateCpsT___closed__9;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* l_StateCpsT_instMonadStateCpsT(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_StateCpsT_instMonadStateCpsT___closed__10;
return x_3;
}
}
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_StateCpsT_instMonadStateCpsT___lambda__3(x_1, x_2, x_3, x_4);
lean_dec(x_3);
return x_5;
}
}
lean_object* l_StateCpsT_instMonadStateCpsT___lambda__10___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_StateCpsT_instMonadStateCpsT___lambda__10(x_1, x_2, x_3, x_4);
lean_dec(x_3);
return x_5;
}
}
lean_object* l_StateCpsT_instMonadStateOfStateCpsT_match__1___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_3 = lean_ctor_get(x_1, 0);
lean_inc(x_3);
x_4 = lean_ctor_get(x_1, 1);
lean_inc(x_4);
lean_dec(x_1);
x_5 = lean_apply_2(x_2, x_3, x_4);
return x_5;
}
}
lean_object* l_StateCpsT_instMonadStateOfStateCpsT_match__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_StateCpsT_instMonadStateOfStateCpsT_match__1___rarg), 2, 0);
return x_4;
}
}
lean_object* l_StateCpsT_instMonadStateOfStateCpsT___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
lean_inc(x_2);
x_4 = lean_apply_2(x_3, x_2, x_2);
return x_4;
}
}
lean_object* l_StateCpsT_instMonadStateOfStateCpsT___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6;
x_5 = lean_box(0);
x_6 = lean_apply_2(x_4, x_5, x_1);
return x_6;
}
}
lean_object* l_StateCpsT_instMonadStateOfStateCpsT___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_6 = lean_apply_1(x_2, x_4);
x_7 = lean_ctor_get(x_6, 0);
lean_inc(x_7);
x_8 = lean_ctor_get(x_6, 1);
lean_inc(x_8);
lean_dec(x_6);
x_9 = lean_apply_2(x_5, x_7, x_8);
return x_9;
}
}
static lean_object* _init_l_StateCpsT_instMonadStateOfStateCpsT___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_StateCpsT_instMonadStateOfStateCpsT___lambda__1), 3, 0);
return x_1;
}
}
static lean_object* _init_l_StateCpsT_instMonadStateOfStateCpsT___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_StateCpsT_instMonadStateOfStateCpsT___lambda__2___boxed), 4, 0);
return x_1;
}
}
static lean_object* _init_l_StateCpsT_instMonadStateOfStateCpsT___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_StateCpsT_instMonadStateOfStateCpsT___lambda__3), 5, 0);
return x_1;
}
}
static lean_object* _init_l_StateCpsT_instMonadStateOfStateCpsT___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_StateCpsT_instMonadStateOfStateCpsT___closed__1;
x_2 = l_StateCpsT_instMonadStateOfStateCpsT___closed__2;
x_3 = l_StateCpsT_instMonadStateOfStateCpsT___closed__3;
x_4 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
lean_object* l_StateCpsT_instMonadStateOfStateCpsT(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_StateCpsT_instMonadStateOfStateCpsT___closed__4;
return x_3;
}
}
lean_object* l_StateCpsT_instMonadStateOfStateCpsT___lambda__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_StateCpsT_instMonadStateOfStateCpsT___lambda__2(x_1, x_2, x_3, x_4);
lean_dec(x_3);
return x_5;
}
}
lean_object* l_StateCpsT_lift___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = lean_ctor_get(x_1, 1);
lean_inc(x_6);
lean_dec(x_1);
x_7 = lean_alloc_closure((void*)(l_ReaderT_instMonadExceptOfReaderT___rarg___lambda__2), 3, 2);
lean_closure_set(x_7, 0, x_5);
lean_closure_set(x_7, 1, x_4);
x_8 = lean_apply_4(x_6, lean_box(0), lean_box(0), x_2, x_7);
return x_8;
}
}
lean_object* l_StateCpsT_lift(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_StateCpsT_lift___rarg), 5, 0);
return x_4;
}
}
lean_object* l_StateCpsT_instMonadLiftStateCpsT___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_ctor_get(x_1, 1);
lean_inc(x_7);
lean_dec(x_1);
x_8 = lean_alloc_closure((void*)(l_ReaderT_instMonadExceptOfReaderT___rarg___lambda__2), 3, 2);
lean_closure_set(x_8, 0, x_6);
lean_closure_set(x_8, 1, x_5);
x_9 = lean_apply_4(x_7, lean_box(0), lean_box(0), x_3, x_8);
return x_9;
}
}
lean_object* l_StateCpsT_instMonadLiftStateCpsT(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_StateCpsT_instMonadLiftStateCpsT___rarg), 6, 0);
return x_3;
}
}
lean_object* initialize_Init_Control_Lawful(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Control_StateCps(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init_Control_Lawful(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_StateCpsT_instMonadStateCpsT___closed__1 = _init_l_StateCpsT_instMonadStateCpsT___closed__1();
lean_mark_persistent(l_StateCpsT_instMonadStateCpsT___closed__1);
l_StateCpsT_instMonadStateCpsT___closed__2 = _init_l_StateCpsT_instMonadStateCpsT___closed__2();
lean_mark_persistent(l_StateCpsT_instMonadStateCpsT___closed__2);
l_StateCpsT_instMonadStateCpsT___closed__3 = _init_l_StateCpsT_instMonadStateCpsT___closed__3();
lean_mark_persistent(l_StateCpsT_instMonadStateCpsT___closed__3);
l_StateCpsT_instMonadStateCpsT___closed__4 = _init_l_StateCpsT_instMonadStateCpsT___closed__4();
lean_mark_persistent(l_StateCpsT_instMonadStateCpsT___closed__4);
l_StateCpsT_instMonadStateCpsT___closed__5 = _init_l_StateCpsT_instMonadStateCpsT___closed__5();
lean_mark_persistent(l_StateCpsT_instMonadStateCpsT___closed__5);
l_StateCpsT_instMonadStateCpsT___closed__6 = _init_l_StateCpsT_instMonadStateCpsT___closed__6();
lean_mark_persistent(l_StateCpsT_instMonadStateCpsT___closed__6);
l_StateCpsT_instMonadStateCpsT___closed__7 = _init_l_StateCpsT_instMonadStateCpsT___closed__7();
lean_mark_persistent(l_StateCpsT_instMonadStateCpsT___closed__7);
l_StateCpsT_instMonadStateCpsT___closed__8 = _init_l_StateCpsT_instMonadStateCpsT___closed__8();
lean_mark_persistent(l_StateCpsT_instMonadStateCpsT___closed__8);
l_StateCpsT_instMonadStateCpsT___closed__9 = _init_l_StateCpsT_instMonadStateCpsT___closed__9();
lean_mark_persistent(l_StateCpsT_instMonadStateCpsT___closed__9);
l_StateCpsT_instMonadStateCpsT___closed__10 = _init_l_StateCpsT_instMonadStateCpsT___closed__10();
lean_mark_persistent(l_StateCpsT_instMonadStateCpsT___closed__10);
l_StateCpsT_instMonadStateOfStateCpsT___closed__1 = _init_l_StateCpsT_instMonadStateOfStateCpsT___closed__1();
lean_mark_persistent(l_StateCpsT_instMonadStateOfStateCpsT___closed__1);
l_StateCpsT_instMonadStateOfStateCpsT___closed__2 = _init_l_StateCpsT_instMonadStateOfStateCpsT___closed__2();
lean_mark_persistent(l_StateCpsT_instMonadStateOfStateCpsT___closed__2);
l_StateCpsT_instMonadStateOfStateCpsT___closed__3 = _init_l_StateCpsT_instMonadStateOfStateCpsT___closed__3();
lean_mark_persistent(l_StateCpsT_instMonadStateOfStateCpsT___closed__3);
l_StateCpsT_instMonadStateOfStateCpsT___closed__4 = _init_l_StateCpsT_instMonadStateOfStateCpsT___closed__4();
lean_mark_persistent(l_StateCpsT_instMonadStateOfStateCpsT___closed__4);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus
}
#endif

24
stage0/stdlib/Init/Data/List/Control.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Data.List.Control
// Imports: Init.Control.Basic Init.Data.List.Basic
// Imports: Init.Control.Basic Init.Control.Foldable Init.Data.List.Basic
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -53,6 +53,7 @@ lean_object* l_List_forIn_loop___rarg___lambda__1(lean_object*, lean_object*, le
lean_object* l_List_anyM_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_List_anyM_match__1(lean_object*);
lean_object* l_List_forA___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_instFoldableList(lean_object*, lean_object*, lean_object*);
lean_object* l_List_allM___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_filterAuxM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_mapM_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -61,6 +62,7 @@ lean_object* l_List_filterMapM_loop___rarg___lambda__1(lean_object*, lean_object
lean_object* l_List_mapA(lean_object*);
lean_object* l_List_forIn_loop___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_instForInList___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_instFoldableList___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_filterM___rarg___lambda__1(lean_object*, lean_object*);
lean_object* l_List_anyM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_firstM(lean_object*);
@ -1532,7 +1534,24 @@ x_4 = lean_alloc_closure((void*)(l_List_instForInList___rarg), 4, 0);
return x_4;
}
}
lean_object* l_List_instFoldableList___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_List_foldlM___rarg(x_1, lean_box(0), lean_box(0), x_2, x_3, x_4);
return x_5;
}
}
lean_object* l_List_instFoldableList(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_List_instFoldableList___rarg), 4, 0);
return x_4;
}
}
lean_object* initialize_Init_Control_Basic(lean_object*);
lean_object* initialize_Init_Control_Foldable(lean_object*);
lean_object* initialize_Init_Data_List_Basic(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Data_List_Control(lean_object* w) {
@ -1542,6 +1561,9 @@ _G_initialized = true;
res = initialize_Init_Control_Basic(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Control_Foldable(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_List_Basic(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

938
stage0/stdlib/Init/Data/Range.c generated
View file

File diff suppressed because it is too large Load diff

40
stage0/stdlib/Lean/Compiler/IR/EmitC.c generated
View file

@ -65,6 +65,7 @@ lean_object* lean_nat_div(lean_object*, lean_object*);
lean_object* l_Lean_IR_EmitC_throwUnknownVar___rarg___closed__1;
lean_object* l_Std_RBNode_insert___at_Lean_NameSet_insert___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_EmitC_emitMainFn___lambda__4___closed__2;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
lean_object* l_Lean_IR_EmitC_emitInitFn___closed__10;
lean_object* l_Lean_IR_EmitC_declareVars___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_EmitC_emitCase___closed__2;
@ -214,7 +215,6 @@ lean_object* l_Lean_IR_EmitC_emitJmp___closed__1;
lean_object* l_Lean_IR_EmitC_getDecl_match__1(lean_object*);
lean_object* l_Lean_IR_EmitC_toCInitName___closed__1;
lean_object* l_Lean_IR_EmitC_leanMainFn___closed__1;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
lean_object* l_Lean_IR_EmitC_main(lean_object*, lean_object*);
extern lean_object* l_Char_quoteCore___closed__2;
lean_object* l_Lean_IR_EmitC_emit___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -3149,7 +3149,7 @@ lean_object* l_Lean_IR_EmitC_emitMainFn___lambda__1(lean_object* x_1, lean_objec
_start:
{
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; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; uint8_t x_26;
x_5 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_5 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_6 = lean_string_append(x_4, x_5);
x_7 = l___private_Init_Data_Format_Basic_0__Std_Format_pushNewline___closed__1;
x_8 = lean_string_append(x_6, x_7);
@ -3332,7 +3332,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_2 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
@ -4492,7 +4492,7 @@ static lean_object* _init_l_Lean_IR_EmitC_emitFileFooter___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_2 = l_Lean_IR_EmitC_emitFileHeader___closed__3;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -6997,7 +6997,7 @@ lean_dec(x_39);
x_40 = l_Lean_IR_EmitC_emitReset___closed__4;
x_41 = lean_string_append(x_38, x_40);
x_42 = lean_string_append(x_41, x_14);
x_43 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_43 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_44 = lean_string_append(x_42, x_43);
x_45 = lean_string_append(x_44, x_14);
x_46 = lean_box(0);
@ -7014,7 +7014,7 @@ lean_dec(x_36);
x_48 = l_Lean_IR_EmitC_emitReset___closed__4;
x_49 = lean_string_append(x_47, x_48);
x_50 = lean_string_append(x_49, x_14);
x_51 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_51 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_52 = lean_string_append(x_50, x_51);
x_53 = lean_string_append(x_52, x_14);
x_54 = lean_box(0);
@ -7049,7 +7049,7 @@ lean_object* l_Lean_IR_EmitC_emitReuse___lambda__1(lean_object* x_1, lean_object
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_6 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_6 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_7 = lean_string_append(x_5, x_6);
x_8 = l___private_Init_Data_Format_Basic_0__Std_Format_pushNewline___closed__1;
x_9 = lean_string_append(x_7, x_8);
@ -10640,7 +10640,7 @@ lean_dec(x_17);
x_21 = lean_ctor_get(x_20, 1);
lean_inc(x_21);
lean_dec(x_20);
x_22 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_22 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_23 = lean_string_append(x_21, x_22);
x_24 = lean_string_append(x_23, x_15);
x_25 = lean_box(0);
@ -11365,7 +11365,7 @@ lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_
x_9 = lean_ctor_get(x_7, 1);
x_10 = lean_ctor_get(x_7, 0);
lean_dec(x_10);
x_11 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_11 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_12 = lean_string_append(x_9, x_11);
x_13 = l___private_Init_Data_Format_Basic_0__Std_Format_pushNewline___closed__1;
x_14 = lean_string_append(x_12, x_13);
@ -11380,7 +11380,7 @@ lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean
x_16 = lean_ctor_get(x_7, 1);
lean_inc(x_16);
lean_dec(x_7);
x_17 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_17 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_18 = lean_string_append(x_16, x_17);
x_19 = l___private_Init_Data_Format_Basic_0__Std_Format_pushNewline___closed__1;
x_20 = lean_string_append(x_18, x_19);
@ -12208,7 +12208,7 @@ lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24;
lean_dec(x_18);
lean_dec(x_17);
lean_dec(x_4);
x_21 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_21 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_22 = lean_string_append(x_16, x_21);
x_23 = lean_string_append(x_22, x_15);
x_24 = lean_box(0);
@ -12226,7 +12226,7 @@ lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29;
lean_dec(x_18);
lean_dec(x_17);
lean_dec(x_4);
x_26 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_26 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_27 = lean_string_append(x_16, x_26);
x_28 = lean_string_append(x_27, x_15);
x_29 = lean_box(0);
@ -12254,7 +12254,7 @@ lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean
x_35 = lean_ctor_get(x_33, 1);
x_36 = lean_ctor_get(x_33, 0);
lean_dec(x_36);
x_37 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_37 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_38 = lean_string_append(x_35, x_37);
x_39 = lean_string_append(x_38, x_15);
lean_ctor_set(x_33, 1, x_39);
@ -12267,7 +12267,7 @@ lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean
x_40 = lean_ctor_get(x_33, 1);
lean_inc(x_40);
lean_dec(x_33);
x_41 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_41 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_42 = lean_string_append(x_40, x_41);
x_43 = lean_string_append(x_42, x_15);
x_44 = lean_alloc_ctor(0, 2, 0);
@ -12321,7 +12321,7 @@ lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean
lean_dec(x_55);
lean_dec(x_54);
lean_dec(x_4);
x_58 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_58 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_59 = lean_string_append(x_53, x_58);
x_60 = lean_string_append(x_59, x_52);
x_61 = lean_box(0);
@ -12340,7 +12340,7 @@ lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean
lean_dec(x_55);
lean_dec(x_54);
lean_dec(x_4);
x_64 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_64 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_65 = lean_string_append(x_53, x_64);
x_66 = lean_string_append(x_65, x_52);
x_67 = lean_box(0);
@ -12371,7 +12371,7 @@ if (lean_is_exclusive(x_72)) {
lean_dec_ref(x_72);
x_74 = lean_box(0);
}
x_75 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_75 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_76 = lean_string_append(x_73, x_75);
x_77 = lean_string_append(x_76, x_52);
if (lean_is_scalar(x_74)) {
@ -12761,7 +12761,7 @@ lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean
x_16 = lean_ctor_get(x_14, 1);
x_17 = lean_ctor_get(x_14, 0);
lean_dec(x_17);
x_18 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_18 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_19 = lean_string_append(x_16, x_18);
x_20 = lean_string_append(x_19, x_9);
x_21 = lean_box(0);
@ -12775,7 +12775,7 @@ lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean
x_22 = lean_ctor_get(x_14, 1);
lean_inc(x_22);
lean_dec(x_14);
x_23 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_23 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_24 = lean_string_append(x_22, x_23);
x_25 = lean_string_append(x_24, x_9);
x_26 = lean_box(0);
@ -12838,7 +12838,7 @@ if (lean_is_exclusive(x_36)) {
lean_dec_ref(x_36);
x_38 = lean_box(0);
}
x_39 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_39 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_40 = lean_string_append(x_37, x_39);
x_41 = lean_string_append(x_40, x_9);
x_42 = lean_box(0);

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

@ -29,6 +29,7 @@ lean_object* l_Lean_IR_formatFnBodyHead___closed__29;
lean_object* l_Lean_IR_instToFormatDecl(lean_object*);
lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatExpr___closed__7;
lean_object* l_Std_fmt___at_Lean_Position_instToFormatPosition___spec__1(lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatExpr___closed__8;
lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatExpr___closed__17;
lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatExpr___closed__3;
@ -83,7 +84,6 @@ lean_object* l_Lean_Name_toStringWithSep(lean_object*, lean_object*);
lean_object* l_Lean_IR_formatFnBodyHead___closed__23;
lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatExpr___closed__21;
lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatArg___closed__1;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
lean_object* l_Lean_IR_formatFnBodyHead___closed__1;
extern lean_object* l_Lean_IR_instToStringVarId___closed__1;
lean_object* l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatExpr___closed__6;
@ -2268,7 +2268,7 @@ static lean_object* _init_l___private_Lean_Compiler_IR_Format_0__Lean_IR_formatI
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;

6
stage0/stdlib/Lean/Data/Json/Printer.c generated
View file

@ -19,6 +19,7 @@ size_t l_USize_add(size_t, size_t);
lean_object* l___private_Lean_Data_Json_Printer_0__Lean_Json_escapeAux___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Json_escape(lean_object*);
lean_object* lean_nat_div(lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
lean_object* l_Lean_Json_render___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_term_x5b___x5d___closed__9;
lean_object* lean_array_uget(lean_object*, size_t);
@ -44,7 +45,6 @@ extern lean_object* l_instReprBool___closed__4;
lean_object* l_Lean_Json_render___closed__8;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_13855____closed__9;
lean_object* l___private_Lean_Data_Json_Printer_0__Lean_Json_escapeAux(lean_object*, uint32_t);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
lean_object* l_Lean_Json_render___closed__1;
extern lean_object* l_Char_quoteCore___closed__2;
lean_object* l_Lean_Json_render___closed__2;
@ -514,7 +514,7 @@ static lean_object* _init_l_Lean_Json_render___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
@ -811,7 +811,7 @@ x_28 = l_String_intercalate(x_27, x_26);
x_29 = l_addParenHeuristic___closed__1;
x_30 = lean_string_append(x_29, x_28);
lean_dec(x_28);
x_31 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_31 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_32 = lean_string_append(x_30, x_31);
return x_32;
}

6
stage0/stdlib/Lean/Data/Lsp/Basic.c generated
View file

@ -220,6 +220,7 @@ extern lean_object* l_term_x5b___x5d___closed__5;
lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonPosition____x40_Lean_Data_Lsp_Basic___hyg_185____closed__1;
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonRange____x40_Lean_Data_Lsp_Basic___hyg_387____spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Lsp_instBEqCancelParams;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_600____closed__1;
lean_object* l_Lean_JsonNumber_fromNat(lean_object*);
lean_object* l_Lean_Json_getObjValD(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentRegistrationOptions____x40_Lean_Data_Lsp_Basic___hyg_1522_(lean_object*);
@ -263,7 +264,6 @@ extern lean_object* l_prec_x28___x29___closed__7;
lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1265____closed__1;
lean_object* l_Lean_Lsp_instToJsonWorkDoneProgressEnd;
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonMarkupContent____x40_Lean_Data_Lsp_Basic___hyg_1660____spec__1(lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_552____closed__1;
extern lean_object* l_prec_x28___x29___closed__3;
lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonCommand____x40_Lean_Data_Lsp_Basic___hyg_750____boxed(lean_object*);
lean_object* l_Lean_Lsp_instToJsonTextEditBatch(lean_object*);
@ -996,7 +996,7 @@ lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_obj
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonPosition____x40_Lean_Data_Lsp_Basic___hyg_185_(x_2);
x_4 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_552____closed__1;
x_4 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_600____closed__1;
x_5 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_5, 0, x_4);
lean_ctor_set(x_5, 1, x_3);
@ -1056,7 +1056,7 @@ lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonRange____x40_Le
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_552____closed__1;
x_2 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_600____closed__1;
x_3 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonRange____x40_Lean_Data_Lsp_Basic___hyg_387____spec__1(x_1, x_2);
if (lean_obj_tag(x_3) == 0)
{

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

@ -24,6 +24,7 @@ lean_object* l_Lean_Elab_checkNotAlreadyDeclared___rarg___lambda__3(lean_object*
lean_object* l_Lean_Elab_applyVisibility___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_checkNotAlreadyDeclared___rarg___lambda__3___closed__2;
lean_object* l_Lean_Elab_expandOptDocComment_x3f(lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
lean_object* l_Lean_addDocString_x27___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_checkNotAlreadyDeclared___rarg___lambda__3___closed__1;
lean_object* l_Lean_Elab_instToFormatModifiers___closed__1;
@ -67,7 +68,6 @@ lean_object* l_Lean_Elab_elabModifiers___rarg___lambda__2___boxed(lean_object*,
lean_object* l_Lean_Elab_applyVisibility_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_instToFormatModifiers___closed__8;
extern lean_object* l_Lean_Parser_Term_scoped___elambda__1___closed__4;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
lean_object* l_Lean_Elab_applyVisibility_match__1(lean_object*);
uint8_t l_Lean_Elab_Modifiers_isNoncomputable___default;
lean_object* l_Lean_Elab_expandDeclId___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1142,7 +1142,7 @@ static lean_object* _init_l_Lean_Elab_instToFormatModifiers___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;

20
stage0/stdlib/Lean/Elab/Deriving/FromToJson.c generated
View file

@ -19,6 +19,7 @@ size_t l_USize_add(size_t, size_t);
lean_object* l_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler_match__1(lean_object*);
extern lean_object* l_Lean_Parser_Term_doIdDecl___elambda__1___closed__1;
lean_object* l_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___lambda__1___closed__13;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
lean_object* l_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler___closed__1;
lean_object* l_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___lambda__1___closed__11;
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___spec__1___closed__7;
@ -40,10 +41,12 @@ extern lean_object* l_myMacro____x40_Init_Notation___hyg_14424____closed__11;
lean_object* l_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___lambda__1___closed__4;
lean_object* lean_st_ref_get(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___lambda__1___boxed__const__1;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__5;
lean_object* l_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler___lambda__1___closed__14;
lean_object* l_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___lambda__1___closed__8;
lean_object* l_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler___lambda__1___closed__5;
lean_object* l_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___lambda__1___closed__17;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__15;
lean_object* l_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___lambda__1___closed__6;
extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1136____closed__5;
@ -56,13 +59,13 @@ lean_object* l_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___lambda__1
lean_object* lean_string_utf8_byte_size(lean_object*);
extern lean_object* l_myMacro____x40_Init_NotationExtra___hyg_5658____closed__10;
extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1136____closed__33;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__3;
lean_object* l_Lean_Elab_Term_getMainModule___rarg(lean_object*, lean_object*);
uint8_t l_USize_decLt(size_t, size_t);
extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_826____closed__9;
lean_object* l_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___lambda__1___closed__1;
lean_object* l_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler___lambda__1___closed__10;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__5;
lean_object* l_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___lambda__1___closed__3;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_12938____closed__14;
lean_object* l_Lean_Name_toStringWithSep(lean_object*, lean_object*);
@ -73,10 +76,10 @@ lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Deriving_FromToJson_mkFromJso
extern lean_object* l_myMacro____x40_Init_Notation___hyg_13855____closed__9;
lean_object* l_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___lambda__1___closed__15;
extern lean_object* l_term___x3c_x7c_____closed__3;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_2191____closed__3;
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___spec__1___closed__6;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_12938____closed__5;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___spec__1___closed__5;
lean_object* l_Lean_Elab_Deriving_FromToJson_mkJsonField___lambda__1___boxed(lean_object*);
lean_object* l_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler___lambda__1___closed__3;
@ -111,18 +114,15 @@ lean_object* l_Lean_Elab_Command_elabCommand(lean_object*, lean_object*, lean_ob
lean_object* l_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___lambda__1___closed__14;
lean_object* l_Lean_Elab_Deriving_mkHeader___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_bind___at_Lean_Elab_Term_instMonadLogTermElabM___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
lean_object* l_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___lambda__1___closed__12;
size_t lean_usize_of_nat(lean_object*);
extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1136____closed__7;
lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_doReturn___elambda__1___closed__2;
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___spec__1___closed__4;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__15;
extern lean_object* l___private_Init_Meta_0__Lean_quoteOption___rarg___closed__1;
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___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*, lean_object*, lean_object*);
extern lean_object* l_Lean_nullKind___closed__2;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__3;
lean_object* l_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler_match__1(lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___spec__1___closed__8;
uint8_t l_UInt32_decEq(uint32_t, uint32_t);
@ -2381,10 +2381,10 @@ lean_inc(x_17);
x_18 = lean_ctor_get(x_14, 1);
lean_inc(x_18);
lean_dec(x_14);
x_19 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__3;
x_19 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__3;
lean_inc(x_4);
x_20 = lean_name_mk_string(x_4, x_19);
x_21 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__5;
x_21 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__5;
lean_inc(x_4);
x_22 = lean_name_mk_string(x_4, x_21);
lean_inc(x_1);
@ -2585,7 +2585,7 @@ static lean_object* _init_l_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHand
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__15;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__15;
x_2 = l_myMacro____x40_Init_Notation___hyg_12938____closed__5;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -2871,12 +2871,12 @@ x_159 = lean_array_push(x_150, x_158);
x_160 = l_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler___lambda__1___closed__16;
x_161 = lean_array_push(x_159, x_160);
x_162 = lean_array_push(x_161, x_57);
x_163 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_163 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_164 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_164, 0, x_38);
lean_ctor_set(x_164, 1, x_163);
x_165 = lean_array_push(x_162, x_164);
x_166 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
x_166 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
x_167 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_167, 0, x_166);
lean_ctor_set(x_167, 1, x_165);

4
stage0/stdlib/Lean/Elab/Deriving/Inhabited.c generated
View file

@ -23,6 +23,7 @@ lean_object* l_List_map___at___private_Lean_Elab_Deriving_Inhabited_0__Lean_Elab
lean_object* l_Lean_registerTraceClass(lean_object*, lean_object*);
lean_object* l_Lean_stringToMessageData(lean_object*);
extern lean_object* l_instReprSigma___rarg___closed__2;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
extern lean_object* l_Lean_Meta_forallTelescopeCompatibleAux___rarg___lambda__3___closed__4;
lean_object* l___private_Lean_Elab_Deriving_Inhabited_0__Lean_Elab_mkInhabitedInstanceUsing_addLocalInstancesForParamsAux___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_instBinder;
@ -83,7 +84,6 @@ extern lean_object* l_myMacro____x40_Init_Notation___hyg_12938____closed__14;
lean_object* l_Std_Range_forIn_loop___at___private_Lean_Elab_Deriving_Inhabited_0__Lean_Elab_mkInhabitedInstanceUsing_mkInstanceCmd_x3f___spec__1___closed__4;
lean_object* l_Std_Range_forIn_loop___at___private_Lean_Elab_Deriving_Inhabited_0__Lean_Elab_mkInhabitedInstanceUsing_mkInstanceCmdWith___spec__7___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_myMacro____x40_Init_Notation___hyg_13855____closed__9;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
lean_object* l_Std_Range_forIn_loop___at___private_Lean_Elab_Deriving_Inhabited_0__Lean_Elab_mkInhabitedInstanceUsing_mkInstanceCmd_x3f___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*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_myMacro____x40_Init_NotationExtra___hyg_5658____closed__16;
lean_object* l___private_Lean_Elab_Deriving_Inhabited_0__Lean_Elab_mkInhabitedInstanceUsing_mkInstanceCmd_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -4808,7 +4808,7 @@ lean_ctor_set(x_49, 0, x_46);
lean_ctor_set(x_49, 1, x_2);
lean_inc(x_49);
x_50 = lean_array_push(x_48, x_49);
x_51 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_51 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_52 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_52, 0, x_36);
lean_ctor_set(x_52, 1, x_51);

4
stage0/stdlib/Lean/Elab/Deriving/Util.c generated
View file

@ -22,6 +22,7 @@ lean_object* lean_erase_macro_scopes(lean_object*);
lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Deriving_mkInstImplicitBinders___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_mkInstanceCmds___spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_instReprSigma___rarg___closed__2;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
lean_object* l_Lean_LocalDecl_userName(lean_object*);
extern lean_object* l_Lean_Parser_Term_instBinder;
lean_object* l_Subarray_forInUnsafe_loop___at_Lean_Elab_Deriving_mkDiscrs___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -75,7 +76,6 @@ lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Deriving_instBinderF;
lean_object* l_List_forIn_loop___at_Lean_Elab_Deriving_mkContext___spec__4___closed__2;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_13855____closed__9;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_14424____closed__4;
lean_object* l_Lean_Elab_Deriving_mkInductArgNames(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Deriving_mkHeader___rarg___boxed__const__1;
@ -771,7 +771,7 @@ lean_ctor_set(x_32, 1, x_30);
x_33 = lean_array_push(x_28, x_32);
x_34 = l_myMacro____x40_Init_Notation___hyg_1398____closed__8;
x_35 = lean_array_push(x_33, x_34);
x_36 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_36 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_37 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_37, 0, x_19);
lean_ctor_set(x_37, 1, x_36);

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

@ -283,6 +283,7 @@ lean_object* l_Lean_Syntax_mkApp(lean_object*, lean_object*);
lean_object* l___private_Lean_Expr_0__Lean_Expr_getAppArgsAux(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_ToDepElimPattern_mkLocalDeclFor_match__2(lean_object*);
lean_object* l_Lean_LocalDecl_value(lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
uint8_t l_Lean_Name_hasMacroScopes(lean_object*);
lean_object* l_Lean_Elab_Term_elabMatchAltView(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_tryPostponeIfNoneOrMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -477,7 +478,6 @@ lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_ToDepElimPattern_thro
lean_object* l_ReaderT_bind___at_Lean_Elab_Term_instMonadLogTermElabM___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_CollectPatternVars_CtorApp_processCtorApp_match__3(lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___lambda__1___closed__2;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
lean_object* l_Lean_Meta_whnf(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_mkInaccessible(lean_object*);
uint8_t l_Array_anyMUnsafe_any___at_Lean_Elab_Term_elabMatch_elabMatchDefault___spec__1(lean_object*, size_t, size_t);
@ -9700,7 +9700,7 @@ x_32 = lean_name_eq(x_10, x_31);
if (x_32 == 0)
{
lean_object* x_33; uint8_t x_34;
x_33 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
x_33 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
x_34 = lean_name_eq(x_10, x_33);
if (x_34 == 0)
{
@ -11128,7 +11128,7 @@ x_375 = lean_name_eq(x_10, x_374);
if (x_375 == 0)
{
lean_object* x_376; uint8_t x_377;
x_376 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
x_376 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
x_377 = lean_name_eq(x_10, x_376);
if (x_377 == 0)
{
@ -12091,7 +12091,7 @@ x_575 = lean_name_eq(x_10, x_574);
if (x_575 == 0)
{
lean_object* x_576; uint8_t x_577;
x_576 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
x_576 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
x_577 = lean_name_eq(x_10, x_576);
if (x_577 == 0)
{
@ -13088,7 +13088,7 @@ x_790 = lean_name_eq(x_10, x_789);
if (x_790 == 0)
{
lean_object* x_791; uint8_t x_792;
x_791 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
x_791 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
x_792 = lean_name_eq(x_10, x_791);
if (x_792 == 0)
{
@ -14164,7 +14164,7 @@ x_1019 = lean_name_eq(x_10, x_1018);
if (x_1019 == 0)
{
lean_object* x_1020; uint8_t x_1021;
x_1020 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
x_1020 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
x_1021 = lean_name_eq(x_10, x_1020);
if (x_1021 == 0)
{

30
stage0/stdlib/Lean/Elab/MutualDef.c generated
View file

@ -47,6 +47,7 @@ lean_object* l_Lean_Meta_forallBoundedTelescope___at___private_Lean_Elab_MutualD
lean_object* l_Lean_setEnv___at_Lean_Elab_Term_evalExpr___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_elabAttr___rarg___lambda__8___closed__2;
lean_object* l_Lean_Elab_Term_getLetRecsToLift___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__14___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_withUsed_match__1___rarg(lean_object*, lean_object*);
lean_object* l_Lean_LocalDecl_userName(lean_object*);
@ -123,6 +124,7 @@ lean_object* l_Array_sequenceMap___at_myMacro____x40_Init_NotationExtra___hyg_51
lean_object* l_List_mapM___at_Lean_Elab_Term_elabMutualDef___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_registerFailedToInferDefTypeInfo___closed__3;
uint8_t lean_name_eq(lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__5;
lean_object* l_Lean_LocalContext_get_x21(lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Term_mkAuxName___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_checkKinds___closed__2;
@ -190,6 +192,7 @@ lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_check___lambda__7
uint8_t l_Lean_LocalContext_contains(lean_object*, lean_object*);
uint8_t l_Lean_Elab_DefKind_isExample(uint8_t);
lean_object* l_Std_RBNode_fold___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkFreeVarMap___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__3;
lean_object* l_Lean_Elab_Term_MutualClosure_insertReplacementForMainFns___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_USize_decLt(size_t, size_t);
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___spec__1___lambda__1___closed__5;
@ -205,7 +208,6 @@ lean_object* l_Lean_throwError___at_Lean_Elab_Command_elabMutualDef___spec__10(l
lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_myMacro____x40_Init_Notation___hyg_109____spec__1(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_whereDecls_formatter___closed__2;
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkClosureForAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__5;
lean_object* l_Lean_Elab_elabAttr___at_Lean_Elab_Command_elabMutualDef___spec__4(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_isTheorem___boxed(lean_object*);
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_FixPoint_getUsedFVarsMap___rarg(lean_object*);
@ -218,7 +220,6 @@ extern lean_object* l_myMacro____x40_Init_Notation___hyg_13855____closed__9;
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_getFunName___closed__2;
lean_object* l_Lean_mkAppN(lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_MutualClosure_main___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
lean_object* l_Lean_Elab_Command_elabMutualDef___lambda__1(lean_object*, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__14___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkInitialUsedFVarsMap___spec__3___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
@ -232,6 +233,7 @@ lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_levelMVarToParamH
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkClosureForAux___closed__2;
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_getFunName___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_withFunLocalDecls_loop(lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_check___lambda__4___closed__1;
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_withUsed(lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_runTermElabM___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -353,7 +355,6 @@ lean_object* l_Lean_Elab_Command_elabMutualDef___lambda__1___boxed(lean_object*,
lean_object* l_Std_RBNode_fold___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkFreeVarMap___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_preprocess(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_indexOfAux___at_Lean_LocalContext_erase___spec__3(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__16;
extern lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1137____closed__2;
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_pushLocalDecl(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_revert___spec__4(size_t, size_t, lean_object*);
@ -413,7 +414,6 @@ lean_object* l_Lean_Elab_Term_collectUsedFVars(lean_object*, lean_object*, lean_
lean_object* lean_expr_update_let(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_checkModifiers___lambda__1___closed__3;
lean_object* l_Lean_Elab_Term_MutualClosure_FixPoint_State_usedFVarsMap___default;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
lean_object* l_List_forM___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_checkLetRecsToLiftTypes___spec__2___closed__4;
lean_object* l_Lean_mkFVar(lean_object*);
uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
@ -448,7 +448,6 @@ lean_object* l_Lean_Elab_elabAttr___at_Lean_Elab_Command_elabMutualDef___spec__4
lean_object* l_Array_feraseIdx___rarg(lean_object*, lean_object*);
lean_object* l_List_forM___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_checkLetRecsToLiftTypes___spec__2___closed__1;
extern lean_object* l_Lean_nullKind___closed__2;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__3;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabFunValues___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_checkModifiers___closed__1;
@ -580,6 +579,7 @@ lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_13855____closed__7;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabFunValues___spec__3(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_MutualClosure_getModifiersForLetRecs___boxed(lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__16;
lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_elabModifiers___at_Lean_Elab_Command_elabMutualDef___spec__1___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabMutualDef___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -5770,10 +5770,10 @@ if (x_36 == 0)
{
lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51;
x_37 = lean_ctor_get(x_35, 0);
x_38 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__3;
x_38 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__3;
lean_inc(x_1);
x_39 = lean_name_mk_string(x_1, x_38);
x_40 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__5;
x_40 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__5;
x_41 = lean_name_mk_string(x_1, x_40);
x_42 = lean_array_push(x_15, x_4);
x_43 = l_myMacro____x40_Init_Notation___hyg_1398____closed__8;
@ -5802,10 +5802,10 @@ x_53 = lean_ctor_get(x_35, 1);
lean_inc(x_53);
lean_inc(x_52);
lean_dec(x_35);
x_54 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__3;
x_54 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__3;
lean_inc(x_1);
x_55 = lean_name_mk_string(x_1, x_54);
x_56 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__5;
x_56 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__5;
x_57 = lean_name_mk_string(x_1, x_56);
x_58 = lean_array_push(x_15, x_4);
x_59 = l_myMacro____x40_Init_Notation___hyg_1398____closed__8;
@ -6598,15 +6598,15 @@ x_60 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_60, 0, x_56);
lean_ctor_set(x_60, 1, x_59);
x_61 = lean_array_push(x_52, x_60);
x_62 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__16;
x_62 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__16;
x_63 = lean_array_push(x_61, x_62);
x_64 = lean_array_push(x_63, x_51);
x_65 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_65 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_66 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_66, 0, x_46);
lean_ctor_set(x_66, 1, x_65);
x_67 = lean_array_push(x_64, x_66);
x_68 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
x_68 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
x_69 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_69, 0, x_68);
lean_ctor_set(x_69, 1, x_67);
@ -6644,15 +6644,15 @@ x_85 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_85, 0, x_81);
lean_ctor_set(x_85, 1, x_84);
x_86 = lean_array_push(x_77, x_85);
x_87 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__16;
x_87 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__16;
x_88 = lean_array_push(x_86, x_87);
x_89 = lean_array_push(x_88, x_76);
x_90 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_90 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_91 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_91, 0, x_70);
lean_ctor_set(x_91, 1, x_90);
x_92 = lean_array_push(x_89, x_91);
x_93 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
x_93 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
x_94 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_94, 0, x_93);
lean_ctor_set(x_94, 1, x_92);

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

@ -242,11 +242,13 @@ lean_object* l_List_mapM___rarg(lean_object*, lean_object*, lean_object*, lean_o
extern lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppLValsAux_loop___closed__2;
lean_object* l_Lean_Elab_Term_StructInst_Struct_allDefault_match__2(lean_object*);
lean_object* l_Lean_ConstantInfo_levelParams(lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
lean_object* l_Lean_Elab_Term_tryPostponeIfNoneOrMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_foldl___at_Lean_Elab_Term_StructInst_DefaultFields_collectStructNames___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Term_StructInst_throwFailedToElabField___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabTermEnsuringType(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__6;
lean_object* l_Lean_mkProj(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_FieldVal_toSyntax___closed__1;
lean_object* l_Lean_Elab_Term_StructInst_instToStringStruct;
@ -401,7 +403,6 @@ lean_object* l_List_mapM___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_S
lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_mkFieldMap___closed__1;
lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_toFieldLHS_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_mkCtorHeaderAux___boxed(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_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
lean_object* l_Lean_Meta_whnf(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_isModifyOp_x3f_match__1(lean_object*);
lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_mkCtorHeaderAux___closed__2;
@ -625,7 +626,6 @@ lean_object* l_Lean_Elab_Term_StructInst_trySynthStructInstance_x3f___boxed(lean
lean_object* l_Lean_Elab_Term_StructInst_instInhabitedFieldVal(lean_object*);
lean_object* l_List_mapM___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_expandNumLitFields___spec__3___closed__6;
lean_object* l_Array_findIdx_x3f_loop___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__6;
lean_object* l_Lean_throwError___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_getFieldIdx___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_12336____closed__12;
lean_object* l_Lean_throwError___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_elabStruct___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -859,7 +859,7 @@ _start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_Elab_macroAttribute;
x_3 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
x_3 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
x_4 = l___regBuiltin_Lean_Elab_Term_StructInst_expandStructInstExpectedType___closed__1;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
@ -3099,7 +3099,7 @@ lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean
x_44 = l_Lean_Syntax_mkApp___closed__1;
x_45 = lean_array_push(x_44, x_43);
x_46 = lean_array_push(x_45, x_41);
x_47 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__6;
x_47 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__6;
x_48 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_48, 0, x_47);
lean_ctor_set(x_48, 1, x_46);
@ -27946,7 +27946,7 @@ _start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_Elab_Term_termElabAttribute;
x_3 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
x_3 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
x_4 = l___regBuiltin_Lean_Elab_Term_StructInst_elabStructInst___closed__1;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;

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

@ -70,7 +70,6 @@ extern lean_object* l_Lean_mkAttributeImplOfConstant___closed__1;
lean_object* l_Std_PersistentHashMap_findAux___at_Lean_Elab_getMacros___spec__3(lean_object*, size_t, lean_object*);
lean_object* l___private_Lean_Elab_Util_0__Lean_Elab_evalSyntaxConstantUnsafe(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_mkMacroAttributeUnsafe___closed__6;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_865____closed__1;
lean_object* l_Lean_Elab_checkSyntaxNodeKind___closed__2;
lean_object* lean_array_fget(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
@ -102,6 +101,7 @@ lean_object* l_Lean_Elab_getMacros(lean_object*, lean_object*, lean_object*, lea
extern lean_object* l_IO_instInhabitedError___closed__1;
lean_object* l_Lean_Syntax_getId(lean_object*);
lean_object* l_Lean_Syntax_prettyPrint(lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_913____closed__1;
lean_object* l_Lean_Elab_mkUnusedBaseName_loop(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Environment_contains(lean_object*, lean_object*);
lean_object* l_Lean_Elab_liftMacroM___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -2798,7 +2798,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_1077____closed__1;
x_2 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_865____closed__1;
x_2 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_913____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}

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

@ -224,7 +224,6 @@ lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_checkTypesAndAssign___
uint8_t l_Array_anyMUnsafe_any___at_Lean_Meta_CheckAssignment_checkMVar___spec__22(lean_object*, lean_object*, size_t, size_t);
lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_mkLambdaFVarsWithLetDeps_hasLetDeclsInBetween___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_CheckAssignment_assignToConstFun(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_865____closed__1;
lean_object* l_StateRefT_x27_lift___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Meta_CheckAssignment_check(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Expr_0__Lean_Expr_getAppArgsAux(lean_object*, lean_object*, lean_object*);
@ -347,6 +346,7 @@ lean_object* l_Lean_Meta_CheckAssignment_State_cache___default___closed__1;
uint8_t l_Array_anyMUnsafe_any___at_Lean_Meta_CheckAssignment_checkMVar___spec__43(lean_object*, lean_object*, size_t, size_t);
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unfoldReducibeDefEq___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
size_t l_Lean_Expr_hash(lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_913____closed__1;
lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_unstuckMVar___closed__3;
lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlMAux___at_Lean_Meta_CheckAssignment_checkMVar___spec__54(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_CheckAssignment_checkMVar___closed__3;
@ -55572,7 +55572,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_isExprDefEq___closed__2;
x_2 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_865____closed__1;
x_2 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_913____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}

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

@ -82,7 +82,6 @@ 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*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_865____closed__1;
lean_object* l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__16;
lean_object* l_StateRefT_x27_instMonadExceptOfStateRefT_x27___rarg(lean_object*);
lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_strictOccursMax_visit_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -130,6 +129,7 @@ lean_object* l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed
lean_object* l_Lean_Meta_decLevel(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getDecLevel(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_LevelDefEq_0__Lean_Meta_postponedToMessageData___spec__3(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_913____closed__1;
uint8_t l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_strictOccursMax_visit(lean_object*, lean_object*);
lean_object* l_Lean_Meta_isLevelDefEqAux___closed__2;
lean_object* l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__2;
@ -3225,7 +3225,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_isLevelDefEqAux___closed__2;
x_2 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_865____closed__1;
x_2 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_913____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -19366,7 +19366,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_processPostponedStep___closed__2;
x_2 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_865____closed__1;
x_2 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_913____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}

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

@ -34,6 +34,7 @@ lean_object* lean_mk_empty_array_with_capacity(lean_object*);
lean_object* l_Std_fmt___at_Lean_Position_instToFormatPosition___spec__1(lean_object*);
lean_object* lean_nat_div(lean_object*, lean_object*);
lean_object* l_Lean_PersistentEnvExtension_getModuleEntries___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMajorPosIfAuxRecursor_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_mkRecursorInfoAux___spec__2___lambda__1___boxed(lean_object**);
extern lean_object* l_term_x5b___x5d___closed__9;
@ -115,7 +116,6 @@ lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Meta_RecursorInfo_0__Lea
lean_object* l_Lean_Meta_RecursorInfo_instToStringRecursorInfo___closed__2;
lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMotiveLevel___closed__1;
lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2185____closed__6;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_mkRecursorInfoAux_match__1___rarg(lean_object*, lean_object*);
lean_object* l_List_toStringAux___at_Lean_Meta_RecursorInfo_instToStringRecursorInfo___spec__2___closed__1;
lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1418,7 +1418,7 @@ x_82 = lean_string_append(x_80, x_81);
x_83 = lean_string_append(x_82, x_40);
lean_dec(x_40);
x_84 = lean_string_append(x_83, x_7);
x_85 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_85 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_86 = lean_string_append(x_84, x_85);
return x_86;
}

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

@ -163,7 +163,6 @@ lean_object* l_ReaderT_instMonadLiftReaderT___rarg___boxed(lean_object*, lean_ob
lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfMinors_loop___rarg___lambda__1___closed__1;
lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemmaProof_match__1(lean_object*);
lean_object* l_Lean_getConstInfoInduct___at_Lean_Meta_mkSizeOfFns___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_865____closed__1;
lean_object* l_StateRefT_x27_lift___rarg___boxed(lean_object*, lean_object*);
lean_object* l___private_Lean_Expr_0__Lean_Expr_getAppArgsAux(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_genSizeOfSpec;
@ -238,6 +237,7 @@ lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_SizeOf_0__Lean_Me
lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkMinorProof___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_natAdd_x3f(lean_object*);
lean_object* l_Lean_Meta_withLocalDecl___at___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemma___spec__6___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_913____closed__1;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_reduceMatcher_x3f___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfSpecTheorem___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*, lean_object*);
lean_object* l_List_mapM___at___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemma___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -8311,7 +8311,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkMinorProof___closed__7;
x_2 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_865____closed__1;
x_2 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_913____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}

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

@ -214,6 +214,7 @@ lean_object* l_Lean_Parser_Term_matchAltsWhereDecls_formatter___closed__5;
lean_object* l_Lean_Parser_Term_attrInstance_parenthesizer___closed__4;
lean_object* l_Lean_Parser_Term_funImplicitBinder_formatter___closed__1;
lean_object* l___regBuiltin_Lean_Parser_Term_ensureTypeOf_parenthesizer(lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
lean_object* l_Lean_Parser_Term_optEllipsis___elambda__1___closed__9;
extern lean_object* l_Lean_Parser_Level_num_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_instBinder_parenthesizer___closed__1;
@ -227,6 +228,7 @@ lean_object* l_Lean_Parser_Level_quot_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Term_matchDiscr___closed__1;
lean_object* l___regBuiltin_Lean_Parser_Term_num_formatter___closed__1;
lean_object* l_Lean_Parser_Term_forInMacro___closed__3;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__14;
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Term___hyg_68____closed__2;
lean_object* l_Lean_Parser_Term_explicitUniv_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_binderType___elambda__1___closed__1;
@ -660,6 +662,7 @@ lean_object* l_Lean_Parser_Level_quot_formatter___closed__5;
lean_object* l___regBuiltin_Lean_Parser_Term_quotedName_formatter___closed__1;
lean_object* l___regBuiltin_Lean_Parser_Term_namedPattern_formatter___closed__1;
lean_object* l_Lean_Parser_Term_funImplicitBinder___elambda__1___closed__5;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__5;
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Term___hyg_3929____closed__3;
lean_object* l_Lean_Parser_Term_sorry_formatter___closed__3;
lean_object* l_Lean_Parser_Term_app_parenthesizer___closed__1;
@ -718,6 +721,7 @@ lean_object* l_Lean_Parser_Term_parser_x21___elambda__1___closed__2;
lean_object* l_Lean_Parser_scientificLit___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_cdot___closed__4;
lean_object* l_Lean_Parser_Term_pipeProj_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__15;
lean_object* l_Lean_Parser_Term_bracketedBinder_formatter___closed__1;
lean_object* l_Lean_Parser_Term_type_parenthesizer___closed__7;
lean_object* l_Lean_Parser_orelseFn(lean_object*, lean_object*, lean_object*, lean_object*);
@ -809,6 +813,7 @@ lean_object* l_Lean_Parser_Term_hole_formatter___closed__2;
lean_object* l_Lean_Parser_Term_borrowed_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Command_docComment___elambda__1___closed__12;
lean_object* l_Lean_Parser_Term_namedArgument___elambda__1___closed__9;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__1;
lean_object* l_Lean_Parser_Term_assert___elambda__1___closed__10;
lean_object* l___regBuiltinParser_Lean_Parser_Term_let(lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_toggleInsideQuot_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -980,6 +985,7 @@ lean_object* l_Lean_Parser_Tactic_tacticSeq_formatter(lean_object*, lean_object*
lean_object* l_Lean_PrettyPrinter_Formatter_checkStackTop_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__11;
lean_object* l_Lean_Parser_Term_letRecDecl;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__3;
lean_object* l_Lean_Parser_many_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_structInstLVal___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_stateRefT_formatter___closed__3;
@ -1079,7 +1085,6 @@ lean_object* l_Lean_Parser_Term_inaccessible;
lean_object* l_Lean_Parser_Term_attr_quot_parenthesizer___closed__4;
lean_object* l_Lean_Parser_Term_binderTactic___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_whereDecls_formatter___closed__2;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__14;
lean_object* l_Lean_Parser_Term_structInst_formatter___closed__8;
lean_object* l___regBuiltin_Lean_Parser_Term_type_formatter(lean_object*);
lean_object* l_Lean_Parser_Term_noindex___closed__2;
@ -1091,7 +1096,6 @@ lean_object* l_Lean_Parser_Term_sort___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_attrInstance___closed__5;
extern lean_object* l_Lean_Parser_mkAntiquot___closed__3;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__5;
lean_object* l_Lean_Parser_Term_sorry___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_structInst_formatter___closed__17;
lean_object* l_Lean_Parser_Term_suffices___elambda__1___closed__2;
@ -1168,6 +1172,7 @@ lean_object* l_Lean_Parser_Term_basicFun_formatter(lean_object*, lean_object*, l
lean_object* l_Lean_Parser_Term_typeOf___elambda__1___closed__7;
lean_object* l_Lean_Parser_Term_assert___closed__2;
lean_object* l_Lean_Parser_Term_app_parenthesizer___closed__3;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__4;
lean_object* l_Lean_Parser_Tactic_tacticSeq1Indented_formatter___closed__3;
lean_object* l_Lean_Parser_Term_matchAlts___elambda__1___closed__1;
lean_object* l_Lean_Parser_Tactic_tacticSeqBracketed___elambda__1___closed__6;
@ -1198,7 +1203,6 @@ lean_object* l_Lean_Parser_Term_cdot___closed__3;
lean_object* l_Lean_Parser_Term_simpleBinder___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_fun_formatter___closed__5;
lean_object* l_Lean_Parser_Term_prop___elambda__1___closed__9;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
lean_object* l_Lean_Parser_Term_typeSpec_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Parser_Tactic_quot_formatter___closed__1;
lean_object* l_Lean_Parser_Term_structInst_parenthesizer___closed__8;
@ -1291,6 +1295,7 @@ lean_object* l_Lean_Parser_Term_paren___closed__3;
lean_object* l___regBuiltin_Lean_Parser_Term_have_formatter___closed__1;
lean_object* l_Lean_Parser_Term_cdot_formatter___closed__4;
lean_object* l_Lean_Parser_Term_ensureTypeOf___closed__9;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
lean_object* l_Lean_Parser_Term_anonymousCtor_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Term_structInstLVal___elambda__1___closed__8;
lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__5;
@ -1354,6 +1359,7 @@ lean_object* l_Lean_Parser_Term_emptyC___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_type___elambda__1___closed__15;
lean_object* l_Lean_Parser_Term_attributes___closed__3;
lean_object* l_Lean_Parser_Term_matchAlt_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__6;
extern lean_object* l_Lean_initFn____x40_Lean_Parser_Extra___hyg_938____closed__17;
lean_object* l_Lean_Parser_Term_structInst_formatter___closed__2;
lean_object* l_Lean_Parser_Term_match___elambda__1___closed__14;
@ -2149,7 +2155,6 @@ lean_object* l_Lean_Parser_Term_noindex_formatter___closed__3;
lean_object* l_Lean_Parser_Term_ensureTypeOf_formatter___closed__5;
lean_object* l_Lean_Parser_Term_basicFun___closed__6;
lean_object* l_Lean_Parser_Term_fun___closed__4;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__1;
lean_object* l_Lean_Parser_Term_typeAscription___elambda__1___closed__8;
lean_object* l_Lean_Parser_Term_panic_formatter___closed__4;
lean_object* l_Lean_Parser_Term_forInMacro_formatter___closed__3;
@ -2281,7 +2286,6 @@ extern lean_object* l_term_x7b_____x3a___x2f_x2f___x7d___closed__13;
lean_object* l_Lean_Parser_Term_instBinder___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_ellipsis___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_show___closed__7;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
lean_object* l_Lean_Parser_Term_dynamicQuot___elambda__1___closed__8;
lean_object* l_Lean_Parser_Term_borrowed_formatter___closed__2;
lean_object* l_Lean_Parser_Term_arrayRef___elambda__1___closed__1;
@ -2431,7 +2435,6 @@ lean_object* l_Lean_Parser_Term_explicit___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_funImplicitBinder___closed__5;
lean_object* l_Lean_Parser_Term_letDecl___closed__4;
lean_object* l___regBuiltin_Lean_Parser_Term_let_x21_formatter(lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__15;
extern lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__5;
lean_object* l_Lean_Parser_Tactic_tacticSeqBracketed_parenthesizer___closed__10;
lean_object* l_Lean_Parser_Term_whereDecls_formatter___closed__4;
@ -2465,7 +2468,6 @@ extern lean_object* l_Lean_Parser_antiquotNestedExpr_formatter___closed__2;
lean_object* l_Lean_Parser_Term_arrow_formatter___closed__1;
lean_object* l_Lean_Parser_Term_binderDefault___closed__4;
lean_object* l_Lean_Parser_Term_inaccessible_formatter___closed__4;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__3;
lean_object* l___regBuiltin_Lean_Parser_Term_emptyC_formatter___closed__1;
lean_object* l_Lean_Parser_Term_matchAltsWhereDecls___closed__3;
lean_object* l_Lean_Parser_Term_structInstLVal___closed__2;
@ -3650,7 +3652,6 @@ extern lean_object* l_rawNatLit___closed__5;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_notFollowedBy_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_mkAntiquot_parenthesizer___rarg___closed__1;
lean_object* l_Lean_Parser_Term_haveAssign_formatter___closed__3;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__6;
lean_object* l_Lean_Parser_Term_funBinder_parenthesizer___closed__4;
lean_object* l_Lean_Parser_Term_binderTactic___elambda__1___closed__11;
extern lean_object* l_Lean_expandExplicitBindersAux_loop___closed__4;
@ -4006,7 +4007,6 @@ lean_object* l_Lean_Parser_Tactic_quotSeq_formatter___closed__1;
lean_object* l_Lean_Parser_Term_tparser_x21___elambda__1___closed__9;
lean_object* l_Lean_Parser_Tactic_tacticSeq_parenthesizer___closed__3;
extern lean_object* l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__2;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__4;
lean_object* l_Lean_Parser_Level_quot_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_emptyC_formatter___closed__1;
lean_object* l_Lean_Parser_ppDedent_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -4916,7 +4916,7 @@ static lean_object* _init_l_Lean_Parser_Tactic_tacticSeqBracketed___elambda__1__
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_2 = l_String_trim(x_1);
return x_2;
}
@ -5791,7 +5791,7 @@ static lean_object* _init_l_Lean_Parser_Tactic_tacticSeqBracketed_formatter___cl
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_2 = lean_alloc_closure((void*)(l_Lean_Parser_symbol_formatter), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
@ -15309,7 +15309,7 @@ static lean_object* _init_l_Lean_Parser_Term_structInstLVal___elambda__1___close
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__6;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__6;
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
@ -15319,7 +15319,7 @@ static lean_object* _init_l_Lean_Parser_Term_structInstLVal___elambda__1___close
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__5;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__5;
x_2 = l_Lean_Parser_Term_structInstLVal___elambda__1___closed__1;
x_3 = 1;
x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
@ -15481,7 +15481,7 @@ static lean_object* _init_l_Lean_Parser_Term_structInstLVal___elambda__1___close
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__6;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__6;
x_2 = l_Lean_Parser_Term_structInstLVal___elambda__1___closed__15;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_nodeFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
@ -15554,7 +15554,7 @@ static lean_object* _init_l_Lean_Parser_Term_structInstLVal___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__6;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__6;
x_2 = l_Lean_Parser_Term_structInstLVal___closed__3;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
@ -15614,7 +15614,7 @@ static lean_object* _init_l_Lean_Parser_Term_structInstField___elambda__1___clos
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__4;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__4;
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
@ -15624,7 +15624,7 @@ static lean_object* _init_l_Lean_Parser_Term_structInstField___elambda__1___clos
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__3;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__3;
x_2 = l_Lean_Parser_Term_structInstField___elambda__1___closed__1;
x_3 = 1;
x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
@ -15647,7 +15647,7 @@ static lean_object* _init_l_Lean_Parser_Term_structInstField___elambda__1___clos
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__4;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__4;
x_2 = l_Lean_Parser_Term_structInstField___elambda__1___closed__3;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_nodeFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
@ -15696,7 +15696,7 @@ static lean_object* _init_l_Lean_Parser_Term_structInstField___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__4;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__4;
x_2 = l_Lean_Parser_Term_structInstField___closed__1;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
@ -15756,7 +15756,7 @@ static lean_object* _init_l_Lean_Parser_Term_optEllipsis___elambda__1___closed__
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__15;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__15;
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
@ -15766,7 +15766,7 @@ static lean_object* _init_l_Lean_Parser_Term_optEllipsis___elambda__1___closed__
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__14;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__14;
x_2 = l_Lean_Parser_Term_optEllipsis___elambda__1___closed__1;
x_3 = 1;
x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
@ -15839,7 +15839,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_optEllipsis___elambda__1___closed__8;
x_2 = lean_ctor_get(x_1, 1);
lean_inc(x_2);
x_3 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__15;
x_3 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__15;
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_nodeFn), 4, 2);
lean_closure_set(x_4, 0, x_3);
lean_closure_set(x_4, 1, x_2);
@ -15878,7 +15878,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_optEllipsis___elambda__1___closed__8;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__15;
x_3 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__15;
x_4 = l_Lean_Parser_nodeInfo(x_3, x_2);
return x_4;
}
@ -15937,7 +15937,7 @@ static lean_object* _init_l_Lean_Parser_Term_structInst___elambda__1___closed__1
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
@ -15947,7 +15947,7 @@ static lean_object* _init_l_Lean_Parser_Term_structInst___elambda__1___closed__2
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__1;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__1;
x_2 = l_Lean_Parser_Term_structInst___elambda__1___closed__1;
x_3 = 1;
x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
@ -16313,7 +16313,7 @@ static lean_object* _init_l_Lean_Parser_Term_structInst___elambda__1___closed__3
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
x_2 = l_Lean_Parser_Term_structInst___elambda__1___closed__34;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_nodeFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
@ -16427,7 +16427,7 @@ static lean_object* _init_l_Lean_Parser_Term_structInst___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
x_2 = l_Lean_Parser_Term_structInst___closed__7;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
@ -16488,7 +16488,7 @@ _start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_term___u2218_____closed__6;
x_3 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
x_3 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Term_structInst;
x_6 = lean_unsigned_to_nat(1000u);
@ -16563,7 +16563,7 @@ static lean_object* _init_l_Lean_Parser_Term_structInstLVal_formatter___closed__
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__5;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__5;
x_2 = l_Lean_Parser_Term_structInstLVal___elambda__1___closed__1;
x_3 = 1;
x_4 = lean_box(x_3);
@ -16686,7 +16686,7 @@ static lean_object* _init_l_Lean_Parser_Term_structInstLVal_formatter___closed__
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__6;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__6;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Term_structInstLVal_formatter___closed__11;
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
@ -16710,7 +16710,7 @@ static lean_object* _init_l_Lean_Parser_Term_structInstField_formatter___closed_
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__3;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__3;
x_2 = l_Lean_Parser_Term_structInstField___elambda__1___closed__1;
x_3 = 1;
x_4 = lean_box(x_3);
@ -16745,7 +16745,7 @@ static lean_object* _init_l_Lean_Parser_Term_structInstField_formatter___closed_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__4;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__4;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Term_structInstField_formatter___closed__3;
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
@ -16780,7 +16780,7 @@ static lean_object* _init_l_Lean_Parser_Term_optEllipsis_formatter___closed__1()
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__14;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__14;
x_2 = l_Lean_Parser_Term_optEllipsis___elambda__1___closed__1;
x_3 = 1;
x_4 = lean_box(x_3);
@ -16815,7 +16815,7 @@ static lean_object* _init_l_Lean_Parser_Term_optEllipsis_formatter___closed__4()
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__15;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__15;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Term_optEllipsis_formatter___closed__3;
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
@ -16839,7 +16839,7 @@ static lean_object* _init_l_Lean_Parser_Term_structInst_formatter___closed__1()
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__1;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__1;
x_2 = l_Lean_Parser_Term_structInst___elambda__1___closed__1;
x_3 = 1;
x_4 = lean_box(x_3);
@ -17046,7 +17046,7 @@ static lean_object* _init_l_Lean_Parser_Term_structInst_formatter___closed__20()
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Term_structInst_formatter___closed__19;
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
@ -17079,7 +17079,7 @@ _start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_PrettyPrinter_formatterAttribute;
x_3 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
x_3 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
x_4 = l___regBuiltin_Lean_Parser_Term_structInst_formatter___closed__1;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
@ -17271,7 +17271,7 @@ static lean_object* _init_l_Lean_Parser_Term_structInstLVal_parenthesizer___clos
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__6;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__6;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Term_structInstLVal_parenthesizer___closed__11;
x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
@ -17328,7 +17328,7 @@ static lean_object* _init_l_Lean_Parser_Term_structInstField_parenthesizer___clo
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__4;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__4;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Term_structInstField_parenthesizer___closed__3;
x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
@ -17365,7 +17365,7 @@ static lean_object* _init_l_Lean_Parser_Term_optEllipsis_parenthesizer___closed_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__15;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__15;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Tactic_tacticSeqBracketed_parenthesizer___closed__3;
x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
@ -17552,7 +17552,7 @@ static lean_object* _init_l_Lean_Parser_Term_structInst_parenthesizer___closed__
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Term_structInst_parenthesizer___closed__15;
x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
@ -17585,7 +17585,7 @@ _start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_PrettyPrinter_parenthesizerAttribute;
x_3 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
x_3 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
x_4 = l___regBuiltin_Lean_Parser_Term_structInst_parenthesizer___closed__1;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;

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

@ -55,6 +55,7 @@ extern lean_object* l_Lean_PrettyPrinter_Delaborator_getExprKind___closed__2;
lean_object* l_Lean_PrettyPrinter_Delaborator_delabProjectionApp_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_delabLit_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_PrettyPrinter_Delaborator_delabMVar___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
extern lean_object* l_addParenHeuristic___closed__2;
lean_object* l_Lean_PrettyPrinter_Delaborator_delabLam_match__1___rarg(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_anyMUnsafe_any___at_Lean_PrettyPrinter_Delaborator_delabForall___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -164,6 +165,7 @@ lean_object* l_Lean_Meta_forallTelescope___at___private_Lean_PrettyPrinter_Delab
lean_object* l_Lean_PrettyPrinter_Delaborator_withMDataExpr___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabDo(lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_delabForall_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__15;
lean_object* l_Lean_PrettyPrinter_Delaborator_delabSort(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_instInhabitedNat;
extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1136____closed__28;
@ -253,6 +255,7 @@ lean_object* l_Array_zip___rarg(lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabMVar___closed__1;
extern lean_object* l_Lean_PrettyPrinter_Delaborator_getExprKind___closed__11;
lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppMatch___closed__3;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__4;
lean_object* l_Lean_PrettyPrinter_Delaborator_delabOfScientific_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_delabListToArray___closed__1;
lean_object* l_Lean_PrettyPrinter_Delaborator_delabStructureInstance___closed__2;
@ -263,7 +266,6 @@ lean_object* l_Lean_PrettyPrinter_Delaborator_delabFVar___closed__2;
lean_object* l_Lean_PrettyPrinter_Delaborator_withProj___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_delabIte___closed__2;
lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfScientific(lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
lean_object* l_Array_anyMUnsafe_any___at_Lean_PrettyPrinter_Delaborator_hasIdent___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_delabMData_match__3(lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_14424____closed__4;
@ -278,6 +280,7 @@ lean_object* l_Lean_Syntax_mkApp(lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_delabDo___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabTuple___closed__2;
lean_object* l___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_skippingBinders_loop___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppExplicit(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBNode_setBlack___rarg(lean_object*);
lean_object* l_Lean_Meta_withLetDecl___at_Lean_PrettyPrinter_Delaborator_delabLetE___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -289,6 +292,7 @@ lean_object* l_Lean_PrettyPrinter_Delaborator_delabDIte_delabBranch_match__1(lea
lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_withBindingDomain___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_delabOfScientific___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__6;
lean_object* l_Lean_Meta_forallTelescope___at___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_delabPatterns___spec__2___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_delabBinders(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_delabMVar___closed__3;
@ -472,7 +476,6 @@ lean_object* l_Lean_PrettyPrinter_Delaborator_delabOfNat___lambda__1(lean_object
lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppMatch_match__1___rarg(lean_object*, lean_object*, lean_object*);
uint8_t l_Array_anyMUnsafe_any___at_Lean_PrettyPrinter_Delaborator_delabForall___spec__3(lean_object*, lean_object*, size_t, size_t);
extern lean_object* l_Lean_PrettyPrinter_Delaborator_getExprKind___closed__10;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
lean_object* l___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_delabBinders_match__1___rarg(lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabSort___closed__1;
lean_object* l_Array_mapMUnsafe_map___at_Lean_PrettyPrinter_Delaborator_delabAppMatch___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -498,7 +501,6 @@ lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabFVar(lean_object
lean_object* l_Lean_PrettyPrinter_Delaborator_withBindingBodyUnusedName___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppWithUnexpander_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_skippingBinders_loop_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__15;
lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabListToArray___closed__1;
extern lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__5;
lean_object* l_Lean_PrettyPrinter_Delaborator_getParamKinds___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -738,7 +740,6 @@ lean_object* l_Lean_PrettyPrinter_Delaborator_delabLam___lambda__3(lean_object*,
lean_object* l_Lean_PrettyPrinter_Delaborator_delabDo___lambda__2___closed__1;
lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppWithUnexpander___closed__1;
lean_object* l_Lean_throwError___at_Lean_PrettyPrinter_Delaborator_delabAppMatch___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__6;
extern lean_object* l_Lean_expandExplicitBindersAux_loop___closed__4;
lean_object* l_Lean_PrettyPrinter_Delaborator_delabSort_match__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_pure___at_Lean_PrettyPrinter_Delaborator_instMonadQuotationDelabM___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -814,7 +815,6 @@ lean_object* l___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyP
lean_object* l___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_unresolveUsingNamespace___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_AssocList_find_x3f___at_Lean_PrettyPrinter_Delaborator_delabAppWithUnexpander___spec__6___boxed(lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabProjectionApp(lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__4;
uint8_t l_Lean_Expr_isLet(lean_object*);
uint8_t l_Lean_isStructure(lean_object*, lean_object*);
extern lean_object* l_term_x5b___x5d___closed__3;
@ -2947,7 +2947,7 @@ x_44 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_44, 0, x_43);
lean_ctor_set(x_44, 1, x_42);
x_45 = lean_array_push(x_25, x_44);
x_46 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_46 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_47 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_47, 0, x_19);
lean_ctor_set(x_47, 1, x_46);
@ -3003,7 +3003,7 @@ x_77 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_77, 0, x_76);
lean_ctor_set(x_77, 1, x_75);
x_78 = lean_array_push(x_58, x_77);
x_79 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_79 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_80 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_80, 0, x_51);
lean_ctor_set(x_80, 1, x_79);
@ -3105,7 +3105,7 @@ x_120 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_120, 0, x_119);
lean_ctor_set(x_120, 1, x_118);
x_121 = lean_array_push(x_101, x_120);
x_122 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_122 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_123 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_123, 0, x_93);
lean_ctor_set(x_123, 1, x_122);
@ -14328,7 +14328,7 @@ lean_ctor_set(x_64, 1, x_62);
x_65 = lean_array_push(x_61, x_64);
x_66 = l_myMacro____x40_Init_Notation___hyg_1398____closed__8;
x_67 = lean_array_push(x_65, x_66);
x_68 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_68 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_69 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_69, 0, x_56);
lean_ctor_set(x_69, 1, x_68);
@ -14379,7 +14379,7 @@ x_89 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_89, 0, x_82);
lean_ctor_set(x_89, 1, x_88);
x_90 = lean_array_push(x_84, x_89);
x_91 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_91 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_92 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_92, 0, x_75);
lean_ctor_set(x_92, 1, x_91);
@ -14746,7 +14746,7 @@ lean_ctor_set(x_188, 1, x_186);
x_189 = lean_array_push(x_185, x_188);
x_190 = l_myMacro____x40_Init_Notation___hyg_1398____closed__8;
x_191 = lean_array_push(x_189, x_190);
x_192 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_192 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_193 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_193, 0, x_180);
lean_ctor_set(x_193, 1, x_192);
@ -14797,7 +14797,7 @@ x_213 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_213, 0, x_206);
lean_ctor_set(x_213, 1, x_212);
x_214 = lean_array_push(x_208, x_213);
x_215 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_215 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_216 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_216, 0, x_199);
lean_ctor_set(x_216, 1, x_215);
@ -16086,7 +16086,7 @@ x_147 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_147, 0, x_140);
lean_ctor_set(x_147, 1, x_146);
x_148 = lean_array_push(x_142, x_147);
x_149 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_149 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_150 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_150, 0, x_133);
lean_ctor_set(x_150, 1, x_149);
@ -20234,7 +20234,7 @@ x_28 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_28, 0, x_27);
lean_ctor_set(x_28, 1, x_3);
x_29 = lean_array_push(x_26, x_28);
x_30 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__6;
x_30 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__6;
x_31 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_31, 0, x_30);
lean_ctor_set(x_31, 1, x_29);
@ -20245,7 +20245,7 @@ lean_ctor_set(x_34, 0, x_21);
lean_ctor_set(x_34, 1, x_33);
x_35 = lean_array_push(x_32, x_34);
x_36 = lean_array_push(x_35, x_17);
x_37 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__4;
x_37 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__4;
x_38 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_38, 0, x_37);
lean_ctor_set(x_38, 1, x_36);
@ -20279,7 +20279,7 @@ x_50 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_50, 0, x_49);
lean_ctor_set(x_50, 1, x_3);
x_51 = lean_array_push(x_48, x_50);
x_52 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__6;
x_52 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__6;
x_53 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_53, 0, x_52);
lean_ctor_set(x_53, 1, x_51);
@ -20290,7 +20290,7 @@ lean_ctor_set(x_56, 0, x_42);
lean_ctor_set(x_56, 1, x_55);
x_57 = lean_array_push(x_54, x_56);
x_58 = lean_array_push(x_57, x_17);
x_59 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__4;
x_59 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__4;
x_60 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_60, 0, x_59);
lean_ctor_set(x_60, 1, x_58);
@ -20406,7 +20406,7 @@ x_89 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_89, 0, x_88);
lean_ctor_set(x_89, 1, x_3);
x_90 = lean_array_push(x_87, x_89);
x_91 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__6;
x_91 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__6;
x_92 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_92, 0, x_91);
lean_ctor_set(x_92, 1, x_90);
@ -20417,7 +20417,7 @@ lean_ctor_set(x_95, 0, x_80);
lean_ctor_set(x_95, 1, x_94);
x_96 = lean_array_push(x_93, x_95);
x_97 = lean_array_push(x_96, x_77);
x_98 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__4;
x_98 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__4;
x_99 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_99, 0, x_98);
lean_ctor_set(x_99, 1, x_97);
@ -20540,12 +20540,12 @@ lean_ctor_set(x_31, 1, x_30);
x_32 = lean_array_push(x_19, x_31);
lean_inc(x_1);
x_33 = lean_array_push(x_1, x_18);
x_34 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__15;
x_34 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__15;
x_35 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_35, 0, x_34);
lean_ctor_set(x_35, 1, x_33);
x_36 = lean_array_push(x_32, x_35);
x_37 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_37 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
lean_inc(x_13);
x_38 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_38, 0, x_13);
@ -20562,7 +20562,7 @@ lean_ctor_set(x_40, 0, x_17);
lean_ctor_set(x_40, 1, x_39);
x_41 = lean_array_push(x_36, x_40);
x_42 = lean_array_push(x_41, x_38);
x_43 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
x_43 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
x_44 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_44, 0, x_43);
lean_ctor_set(x_44, 1, x_42);
@ -20589,7 +20589,7 @@ lean_ctor_set(x_52, 0, x_17);
lean_ctor_set(x_52, 1, x_51);
x_53 = lean_array_push(x_36, x_52);
x_54 = lean_array_push(x_53, x_38);
x_55 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
x_55 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
x_56 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_56, 0, x_55);
lean_ctor_set(x_56, 1, x_54);
@ -20645,12 +20645,12 @@ lean_ctor_set(x_76, 1, x_75);
x_77 = lean_array_push(x_64, x_76);
lean_inc(x_1);
x_78 = lean_array_push(x_1, x_63);
x_79 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__15;
x_79 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__15;
x_80 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_80, 0, x_79);
lean_ctor_set(x_80, 1, x_78);
x_81 = lean_array_push(x_77, x_80);
x_82 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_82 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
lean_inc(x_57);
x_83 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_83, 0, x_57);
@ -20667,7 +20667,7 @@ lean_ctor_set(x_85, 0, x_62);
lean_ctor_set(x_85, 1, x_84);
x_86 = lean_array_push(x_81, x_85);
x_87 = lean_array_push(x_86, x_83);
x_88 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
x_88 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
x_89 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_89, 0, x_88);
lean_ctor_set(x_89, 1, x_87);
@ -20696,7 +20696,7 @@ lean_ctor_set(x_98, 0, x_62);
lean_ctor_set(x_98, 1, x_97);
x_99 = lean_array_push(x_81, x_98);
x_100 = lean_array_push(x_99, x_83);
x_101 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
x_101 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
x_102 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_102, 0, x_101);
lean_ctor_set(x_102, 1, x_100);
@ -20758,12 +20758,12 @@ lean_ctor_set(x_31, 1, x_30);
x_32 = lean_array_push(x_19, x_31);
lean_inc(x_1);
x_33 = lean_array_push(x_1, x_18);
x_34 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__15;
x_34 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__15;
x_35 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_35, 0, x_34);
lean_ctor_set(x_35, 1, x_33);
x_36 = lean_array_push(x_32, x_35);
x_37 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_37 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
lean_inc(x_13);
x_38 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_38, 0, x_13);
@ -20780,7 +20780,7 @@ lean_ctor_set(x_40, 0, x_17);
lean_ctor_set(x_40, 1, x_39);
x_41 = lean_array_push(x_36, x_40);
x_42 = lean_array_push(x_41, x_38);
x_43 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
x_43 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
x_44 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_44, 0, x_43);
lean_ctor_set(x_44, 1, x_42);
@ -20807,7 +20807,7 @@ lean_ctor_set(x_52, 0, x_17);
lean_ctor_set(x_52, 1, x_51);
x_53 = lean_array_push(x_36, x_52);
x_54 = lean_array_push(x_53, x_38);
x_55 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
x_55 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
x_56 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_56, 0, x_55);
lean_ctor_set(x_56, 1, x_54);
@ -20863,12 +20863,12 @@ lean_ctor_set(x_76, 1, x_75);
x_77 = lean_array_push(x_64, x_76);
lean_inc(x_1);
x_78 = lean_array_push(x_1, x_63);
x_79 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__15;
x_79 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__15;
x_80 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_80, 0, x_79);
lean_ctor_set(x_80, 1, x_78);
x_81 = lean_array_push(x_77, x_80);
x_82 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_82 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
lean_inc(x_57);
x_83 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_83, 0, x_57);
@ -20885,7 +20885,7 @@ lean_ctor_set(x_85, 0, x_62);
lean_ctor_set(x_85, 1, x_84);
x_86 = lean_array_push(x_81, x_85);
x_87 = lean_array_push(x_86, x_83);
x_88 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
x_88 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
x_89 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_89, 0, x_88);
lean_ctor_set(x_89, 1, x_87);
@ -20914,7 +20914,7 @@ lean_ctor_set(x_98, 0, x_62);
lean_ctor_set(x_98, 1, x_97);
x_99 = lean_array_push(x_81, x_98);
x_100 = lean_array_push(x_99, x_83);
x_101 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__2;
x_101 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__2;
x_102 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_102, 0, x_101);
lean_ctor_set(x_102, 1, x_100);

6
stage0/stdlib/Leanpkg/Toml.c generated
View file

@ -30,6 +30,7 @@ lean_object* l_Lean_Parser_mkParserContext(lean_object*, lean_object*);
lean_object* l_Toml_keyVal___closed__4;
lean_object* l_Toml_ofSyntax_toKey___closed__3;
lean_object* l_Toml_inlineTable;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
lean_object* l_Toml_table___closed__4;
lean_object* l_Toml_keyVal___closed__2;
lean_object* l_Toml_key___closed__1;
@ -96,7 +97,6 @@ lean_object* l_Lean_Name_toStringWithSep(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_SepArray_ofElems(lean_object*, lean_object*);
lean_object* l_Toml_inlineTable___closed__3;
lean_object* l_Lean_ScopedEnvExtension_getState___at_Lean_Parser_isParserCategory___spec__1(lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
extern lean_object* l_Lean_initFn____x40_Lean_Parser_Extra___hyg_938____closed__8;
lean_object* l_Toml_keyCat_quot;
lean_object* l_Array_zipWithAux___at_Toml_ofSyntax_toTable___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -1102,7 +1102,7 @@ static lean_object* _init_l_Toml_inlineTable___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_1 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_2 = lean_alloc_ctor(5, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
@ -1900,7 +1900,7 @@ x_15 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_15, 0, x_14);
lean_ctor_set(x_15, 1, x_13);
x_16 = lean_array_push(x_12, x_15);
x_17 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_17 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_18 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_18, 0, x_4);
lean_ctor_set(x_18, 1, x_17);

4
stage0/stdlib/Std/Data/PersistentArray.c generated
View file

@ -48,6 +48,7 @@ lean_object* lean_mk_empty_array_with_capacity(lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Std_PersistentArray_toList___spec__9(lean_object*);
lean_object* lean_nat_div(lean_object*, lean_object*);
lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlFromMAux___at_Std_PersistentArray_toArray___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlFromMAux___at_Std_PersistentArray_filter___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlFromMAux___at_Std_PersistentArray_foldl___spec__2___rarg(lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l_Array_findSomeRevM_x3f_find___at_Std_PersistentArray_findSomeRev_x3f___spec__4___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -188,7 +189,6 @@ lean_object* l_Array_foldlMUnsafe_fold___at_Std_PersistentArray_foldl___spec__6(
lean_object* l_Array_foldlMUnsafe_fold___at_Std_PersistentArray_filter___spec__4___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_forIn_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Std_PersistentArray_foldl___spec__6___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
lean_object* l_Std_PersistentArray_anyM___at_Std_PersistentArray_all___spec__1___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Std_PersistentArray_toArray___spec__6___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_anyMUnsafe_any___at_Std_PersistentArray_allM___spec__5___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -12222,7 +12222,7 @@ lean_dec(x_1);
x_14 = l_Nat_repr(x_13);
x_15 = lean_string_append(x_12, x_14);
lean_dec(x_14);
x_16 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_16 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_17 = lean_string_append(x_15, x_16);
return x_17;
}

4
stage0/stdlib/Std/Data/PersistentHashMap.c generated
View file

@ -22,6 +22,7 @@ lean_object* l_Std_PersistentHashMap_insertAtCollisionNode___rarg(lean_object*,
lean_object* l_Array_indexOfAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
lean_object* l_Std_PersistentHashMap_findEntryAux(lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
lean_object* l_Std_PersistentHashMap_root___default___closed__1;
lean_object* l_Std_PersistentHashMap_foldlMAux_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_USize_decEq(size_t, size_t);
@ -84,7 +85,6 @@ lean_object* l_Std_PersistentHashMap_foldlMAux_traverse___at_Std_PersistentHashM
size_t l_Std_PersistentHashMap_maxDepth;
lean_object* l_Std_PersistentHashMap_containsAux___rarg(lean_object*, lean_object*, size_t, lean_object*);
lean_object* l_Std_PersistentHashMap_collectStats_match__1(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
lean_object* l_Std_PersistentHashMap_eraseAux_match__4___rarg(lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_eraseAux_match__2(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_empty___rarg(lean_object*, lean_object*);
@ -4523,7 +4523,7 @@ lean_dec(x_1);
x_19 = l_Nat_repr(x_18);
x_20 = lean_string_append(x_17, x_19);
lean_dec(x_19);
x_21 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_323____closed__22;
x_21 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_371____closed__22;
x_22 = lean_string_append(x_20, x_21);
return x_22;
}