diff --git a/tmp/lean4.md b/tmp/lean4.md
deleted file mode 100644
index ad936902ed..0000000000
--- a/tmp/lean4.md
+++ /dev/null
@@ -1,502 +0,0 @@
-Design notes for Lean4
-----------------------
-
-# Goals
-
-- Move more code from C++ to Lean.
-- New compiler and C++ code generator.
-- New runtime (support for unboxed values and FFI).
-- New parser and macro expander (in Lean).
-- New monad for accessing primitives that are only available in C++ (e.g., `type_context`).
-- Fix critical issues (e.g., issue #1601).
-- Fix language design issues.
-- Reduce clutter in the core lib and code base.
-
-# Plan
-
-- Create Lean4 branch
-- Disable most tests (they will be incrementally added back as we make progress on Lean4).
-- Dramatically reduce the size of core lib. We should only keep the basics that
-are needed to execute Lean programs. Remove most theorems and lemmas,
-algebraic hierarchy, all non basic tactics, etc. Motivations: reduce clutter,
-and increase agility. We will copy `library` into `old_library` and incrementally
-rebuild core lib.
-- Remove dead C++ code, and disable all but the most basic tactics.
-- Add abstraction layers to isolate modules. Example: module manager should not depend on the parser;
-  equation compiler should not depend on the elaborator.
-- Make Lean object thread safe (see Memory management section for performance issues),
-and remove related clutter. Example: we will not need ts_vm_obj anymore.
-Remove unnecessary closure objects that were added for the previous C++ code generator
-that was discontinued.
-- Split tactic state into backtrackable and non-backtrackable parts using the
-new monad transformers. The plan is to have the following monads for meta programming:
-  a) `elab`: it is morally state_t and except_t where the state is `elab_state`.
-     `elab_state` is defined in C++, and contains: `environment`, cache data structures,
-     `name_generator`, `options` and `metavar_context`. Only `metavar_context` is backtrackable, and
-     we define `<|>` as
-     ```
-     meta def elab.orelse {α : Type} (e₁ : elab α) (e₂ : elab α) : elab α :=
-     ⟨λ s, let mctx := s.get_mvar_ctx in
-        match e₁.run s with
-        | elab_result.exception α ex s' := e₂.run (s'.set_mvar_ctx mctx)
-        | r                             := r
-        end⟩
-     ```
-     Note that, `elab_state` is used linearly in the definition above, and we just save
-     `metavar_context`.
-
-  b) `tactic`: it built on top of `elab` using `state_t`. In the new state we store
-      the list of goals (i.e., metavariables) and the main metavariable.
-
-  We will implement (most of) the C++ primitive tactics in the `elab` monad.
-  One of the motivations for the approach above is that C++ and Lean code use `elab` in very similar ways.
-  For example, the `type_context` object in C++ just gets a reference for the `elab_state` object.
-
-  Remark: `elab` monad will be defined in Lean, but we will mark it private. All tactics that
-  have access to the private definition will use `elab_state` linearly. The idea is to make sure
-  we can use destructive updates when implementing C++ primitive tactics. This is a big
-  advantage with respect to the approach used in Lean3 where we keep creating (and deleting) `tactic_state` objects
-  all over the place.
-
-  We have considered splitting `elab` into two monads. The first one `elab_core` would have a state
-  without `metavar_context`. `elab_core` would morally be `except_t ex (state elab_core_state)`. And then,
-  `elab` would be defined as `state_t metavar_context elab_core`. So, `metavar_context` would be backtrackable
-  for free, and we would not need to define a custom `orelse`. This change is fine on the Lean side, but it would
-  be messy when programming in C++ because we would have to continue to propagate the `metavar_context` manually as
-  we do in Lean3. Recall that a few bugs in Lean3 are due to incorrect propagation of the `metavar_context`. These bugs
-  will all disappear with the new design.
-  We also have additional performance overhead with the `elab`+`elab_core` approach.
-  For example, we want to support the following API:
-  ```
-  mk_type_context : elab type_context
-  infer_type : type_context -> expr -> elab expr
-  whnf : type_context -> expr -> elab expr
-  ...
-  ```
-  If we use `elab`+`elab_core` approach, the `infer_type` primitive would have to be implemented as:
-  ```
-  vm_obj infer_type(vm_obj const & ctx, vm_obj const & e, vm_obj const & mctx, vm_obj const & s) {
-  try {
-    ctx.set_mctx(mctx); // copy current metavar_context to ctx
-    auto r = ctx.infer(e);
-    return mk_success_result(r, ctx.mctx(), s); // build result using updated metavar_context
-  } catch (exception & ex) {
-    ....
-  } }
-  ```
-  In the `elab` only approach, we save one argument `mctx`, and we don't have to copy the `metavar_context`.
-
-- Implement support objects in Lean: options, format, structure trace messages, syntax object, etc.
-- Add parser infrastructure in Lean.
-- Compiler and C++ code generator. The C++ code generator will avoid many bootstrapping
-problems we have. The idea is to write several Lean modules in Lean, emit C++ code, save
-the generated C++ code in our repo.
-- New IR with support for non uniform memory layout for Lean objects (see details on the #backend
-Slack channel).
-- Develop a tool in Lean that given a Lean inductive datatype (or structure) generates C++
-code for retrieving fields and creating Lean objects. The goal is to isolate primitives implemented
-in C++ from the way we represent Lean objects in memory. For example, most Lean functions implemented
-in C++ use the C++ function `cfield` which assumes objects have a uniform memory layout.
-- Develop a tool for generating glue code for interfacing Lean and C++ code. Again, the goal
-is to isolate the primitives from the way we handle boxed/unboxed values.
-For example, suppose we have a builtin function `foo` that takes two Lean `bool` values.
-Right now, this function takes boxed values `c_foo(vm_obj const & a, vm_obj const & b)`.
-It feels weird to have to box a Lean value to be able to invoke the builtin implementation for `foo`.
-After we have the tool, we would write `c_foo(bool a, bool b)` and describe its signature in a Lean file.
-The tool then generates the wrappers for invoking `c_foo` from the interpreter and generated C++ code.
-
-# Language and library issues
-
-- `private` declarations are not reliable. Users can easily subvert them
-using meta programming. This is problematic for several optimizations
-we want to use. For example, suppose we define a state-like monad
-where every primitive uses the state linearly. The code
-generator cannot rely on that since users can currently access
-the internal implementation, and use the state in a non linear way.
-This is just an example. We have many more.
-
-- `parameter`s are currently simulated in Lean. For example,
-when we declare `foo` in a section with a parameter `A`,
-`foo` is automatically abstracted and an alias `foo => @foo A` is created.
-This creates many problems, most of them are documented in the issue tracker.
-This approach has one advantage: users can use the abstracted (`_root_.foo`)
-and non-abstracted (`foo`) version simultaneously. Another advantage is that
-we don't have to type check `foo` more than once in the kernel.
-That being said, the disadvantages far outweigh the advantages.
-We plan to go back to the approach used in Lean1 and Coq.
-
-- Coercion resolution (see issue #1402).
-
-- Name resolution for `[ ... ] tactic blocks.
-The `[ ... ] notation allows us to use interactive tactic notation
-when writing reusable tactics. This is very convenient, but the current
-implementation uses dynamic name resolution, and is a source of many
-bugs.
-
-- `if-then-else` using `bool` instead of `Prop`.
-As soon as we started programming with Lean (version 3), it became clear
-that `if-then-else` with `Prop` creates more problems that it solves.
-The elaborator already has support for a coercion from `Prop` to `bool`
-(for decidable propositions). The dependent `if H : p then t else e`
-may look cute, but it is unnecessary now that we have `match`.
-
-- `decidable` type class. A recurrent problem in Lean occurs when
-users perform dependent elimination on `decidable` instances.
-The problem occurs when we have `[h : decidable p]` in the context
-and a goal `G[@f p h]`, that is, a goal containing the term `@f p h`.
-Then, we perform `cases h`, and obtain `G[@f p (dedicable.is_true h')]` in
-one branch and `G[@f p (decidable.is_false h)]` in another. Then, we apply a
-lemma that gives us `G[@f p h]` where `h` is the synthesized instance,
-but we cannot use it to close the goal because we get a type error.
-We have discussed this problem with Tahina and he pointed out that
-we should never perform dependent elimination on type class instances in proofs,
-and that this is an anti-idiom. He told us that every type class is a
-structure in Coq. That is, everything is wrapped in a structure.
-In Coq, they would use a custom eliminator for performing case analysis
-on decidable instances. They don't face this problem because the custom eliminator
-is more convenient to use them manually destructing the wrapper structure,
-and then the actual data. He also strongly suggested that we
-should decouple the program that computes whether a proposition is true or false
-from the proof the result is correct. The Lean type class combines both in one single definition.
-He said this will be a problem in the future for users that want to compute in the kernel.
- The kernel computations will have to deal with these proof terms. In Coq, `decidable` is now defined as:
-```
-Class Decidable (P : Prop) := {
-  Decidable_witness : bool;
-  Decidable_spec : Decidable_witness = true <-> P
-}.
-```
-He strongly recommended we define `decidable` using this approach.
-He said this is not the original definition used in Coq. The first one was a structure wrapping a
-sum type (which is closer to our definition), and the Coq developers had to change it
-because of performance problems in proofs by reflection.
-
-- Interactive tactics. In Lean4 we will have a much more extensible and flexible
-parser, and it will be written in Lean. We will be able to write a custom parser for the tactic
-interactive mode. So, the current argument-type driven parser we use will not
-be needed anymore.
-
-- Quotations. Do we need all of them? I find the one with three backticks very inconvenient to use.
-Moreover, as soon as we implement the new parser, we will want quotations for building
-the new syntactic object and Lean expressions.
-
-# Compiler
-
-- The new compiler will use a System-F like intermediate representation.
-It will be similar to Haskell core language. Inductive datatypes will be represented
-using a constant for each constructor and a `cases` eliminator. If `cases` is encoded
-using a expr-macro, we can easily support `default/other` case.
-
-- Code inlining will occur at the System-F level after we have applied
-simplifications.  This is relevant for the performance issues we have
-observed when a long chain of functions need to be unfolded (e.g., new
-monad transformer library).
-
-- The first compilation step applies compiler specific simplification rules provided by users.
-For example, we will be able to mark `map g (map f l) = map (g o f) l` as an optimization
-rule for the compiler.
-
-Issue: many opportunities for applying simplification rules only appear after we have inlined
-definitions. However, we want to inline after we have converted into System-F and have
-erased computationally irrelevant code and applied basic simplifications (e.g., erase trivial structures).
-This is a problem since user provided simplification rules are not applicable here since they have
-been described at the Lean level.
-
-- Basic types (scalars, bool, char, uint32, uint64, int64, int32, ...) and C++ types
-can be stored in unboxed form. The unboxed version are prefixed with `#` as they do
-in Haskell.
-
-- When we convert a Lean function to System-F, we will generate two versions: boxed and unboxed.
-The boxed version is needed when passing this function to polymorphic higher-order functions.
-As in Haskell, polymorphic functions always take boxed values.
-Both versions are stored in the Lean environment as `meta` functions.
-Example: the function `def inc (a : int32) := a + 1` is converted into two versions
-`meta def _SystemF.boxed.inc (a : int32) := a + 1`, and `meta def _SystemF.unboxed.inc (a : #int32) := a #+ #1`.
-Now, suppose we want to compile `twice inc a` where `def twice {A : Type} (f : A -> A) (a : A) := f (f a)`.
-Then, since `twice` is polymorphic, we need to pass `inc` boxed version, and we generate
-`@_SystemF.boxed.twice int32 _SystemF.boxed.inc a`.
-
-- We want to implement monomorphisation as an additional optimization step. The idea is specialize functions like `twice`.
-In the previous example, monomorphisation would generate `@_SystemF.unboxed.twice_int32 (f : #int32 -> #int32) (a : #int32)`.
-We are considering caching monomorphised functions into the .olean files. If we do this, we have to consider the situation
-where more than one .olean contains the same monomorphised function. We see two options: we have a canonical way to generate
-names for monomorphised functions; we generate unique names, and accept the fact the environment will contain duplicates.
-It is just a space issue.
-Remark: see comment `closure` bullet point below. We may not use unboxed values in closures.
-
-- In Lean3, `name`, `level` and `expr` are all implemented in C++. To expose these objects in Lean, we have to wrap them
-using a subclass of `vm_external`. This generates a significant performance overhead. For example, suppose we have a lean
-function that traverses a big expression; for each visited expression `e`, we need to create a `vm_expr` object for wrapping `e`.
-Moreover, we have two layers of reference counting: one at `expr` and another at `vm_obj`.
-This design decision is fine in Lean3 because the most expensive tasks are implemented in C++, and Lean code is only
-used to "glue" together existing procedures implemented in C++. This is not the case in Lean4.
-So, in Lean4, all these objects will be implemented directly in Lean.
-As described above, we will have a tool that will generate C++ functions for creating and accessing these objects.
-We believe this will not affect much how we code in C++, and it will eliminate a lot of boilerplate code we currently use.
-
-# Object memory layout
-
-- Constructor objects: they will contain pointers and unboxed data. We will use all-pointers first approach, and the header will contain 8 bytes:
-  a) reference counter: 4 bytes
-  b) kind: 1 byte
-  c) tag (aka constructor index): 1 byte
-  d) size (aka number of pointer objects): 2 bytes
-  After the header we have `size` pointers and then all unboxed data. In debug mode, we want to store the size of the space used for
-  unboxed data, and use this information for implementing sanity checks.
-  Remark: the header of all composite Lean objects start with the reference counter and `kind`.
-  Note that this representation supports only inductive datatypes with at most 256 constructors and 2^16 pointer fields.
-  This is sufficient for our needs.
-  If one day we want to support inductive datatypes with more than 256 constructors and/or 2^16 pointer fields, we can add
-  a new kind of constructor object, and add new opcodes for manipulating them. We say this new kind is a "fat" constructor object
-  since its header is bigger.
-
-- Array: we support arrays of pointers and arrays of unboxed data. We will have opcodes for reading and updating arrays.
-The updates are destructive when the array reference counter is 1.
-
-- Closures: we need two kinds of closures: one that stores the bytecode id (for interpreted code); and another that stores a function pointer (for compiled code).
-We need to decide whether we will support closures that store unboxed data or not. The simple solution is to support only boxed data
-in closures. This may not be a huge performance overhead since many higher order functions such as `map` and `fold` will
-be specialized during the monomorphisaton step, and we will not even create the closures.
-A possible compromise is to support unboxed data only for closures that store function pointers. The idea is the following, whenever we emit C++ code for a function,
-we also generate a `run` function for it s.t. given the closure data, it invokes the function. Then, we store the pointer to the `run` function in the closure.
-For example, suppose we have generated
-```
-vm_obj foo(bool b1, vm_obj o, bool b2) { ... }
-```
-Then, we would also generate
-```
-vm_obj run_foo(closure_data d) {
-  return foo(get_closure_bool(8, d), get_closure_obj(0, d), get_closure_bool(9, d));
-}
-```
-`get_closure_bool(offset, d)` retrieves the Boolean stored at the given offset in `d`.
-Note that, as in constructor objects, unboxed data is stored after pointers at `closure_data`.
-So, we use `get_closure_bool(8, d)` to retrieve `b` which is stored after `o` (the pointer to `o` consumes 8 bytes) in `d`.
-It is not clear this approach is a good one since we would always need to create a `closure_data` object that contains all arguments
-before executing a closure. It is not clear how to support the optimization we use in Lean3 that avoids the allocation of the last `closure_data`
-in most cases (https://github.com/leanprover/lean/blob/master/src/library/vm/vm.cpp#L1698).
-
-- MPZ (multiprecision integers)
-
-- String. Remark: internally it is not an array of char, but an array of bytes encoded in UTF8. The key difference with respect to Lean3 is that it will
-not use the `vm_external` wrapper approach, but have an object kind for strings.
-
-# IR
-
-- Register based.
-- Explicit reference counting instructions. We use reference counting for: composite objects, closures and
-  C++ unboxed data (e.g., `expr`). Remark: for each C++ primitive the VM needs to know how to increase/decrease the reference counter.
-- Support for unboxed values.
-- Instructions for accessing unboxed values in non-uniform structures.
-  We will have instructions for operations such as `get_scalar_<sz>(obj, offset)`,
-  where `obj` is a (potentially non-uniform) Lean object, `offset` is the offset
-  inside of this object, and `sz` is the number of bytes needed to store the object.
-  In practice, we would have `get_scalar_1`, `get_scalar_2`, `get_scalar_4` and `get_scalar_8`.
-  These scalars are unboxed. We would have registers for storing the different kinds of scalars,
-  and basic operations on them (e.g., comparison, arithmetic, etc). So, we will
-  have instructions such as `GETS_<sz> r_o r_i offset` where `r_o` and `r_i` are registers, and
-  it corresponds to `r_o := get_scalar_<sz>(r_i, offset)`. Moreover, `r_o` must be a scalar
-  register of size `sz` and `r_i` is a register for storing Lean objects.
-
-Remark: for each constructor datatype, we will have a table that maps fields to the
-operation needed to retrieve them. We will use this table when converting the SystemF
-representation into the IR.
-
-Open issue: should we use SSA or SIL?
-BTW, most of the benefits of SSA/SIL seem to be irrelevant for Lean.
-The paper https://arxiv.org/pdf/1507.05762.pdf send by Nuno describes the pros/cons for SSA.
-Most of them seem to be related to static analysis procedures. I think we will need very few
-static analysis steps, most optimizations will be implemented at System-F before we convert the code into IR.
-
-# VM
-
-- We need a new VM for the new IR.
-
-- The VM should be able to invoke primitives hand written in C++ and
-C++ code emitted by the Lean compiler.
-
-- A few hand written C++ primitives and C++ code emitted by the Lean compiler
-need to invoke Lean functions. We should be careful to avoid a mismatch here where
-a C++ function F for Lean version `X` is trying to invoke bytecode for
-a Lean function G for version `X+1`. If we allow this to happen the system
-may crash because the data representation for version `X+1` may be
-different from version `X`.
-
-We can try to address this issue by breaking core lib into two parts.
-The first part (bootstrapping) contains all the infrastructure needed by the parser, compiler,
-tactic framework, and Lean runtime. If we make a change here, we should
-compile it again using the previously emitted C++ code, and then generate
-a new version of the C++ code, compile it, and check whether it works or not.
-In principle, it is not safe to invoke bytecode generated during the current compilation
-from previously emitted C++ code since they may be using different representations.
-Of course, the changes may be harmless, but to avoid problems we should minimize
-the number of tactics used in this part of the core lib. Ideally, tactics should
-not be used in the bootstrapping part.
-
-We may also emit C++ code for non essential functionality that is implemented in Lean,
-and then link it with the Lean executable. Example: a decision procedure, a parser extension.
-The idea is to provide a more efficient version to users. Here we can use a more
-relaxed approach since this functionality is not part of the compiler. We can store a hash code
-for each of these functions. When we import the .olean file that generated the function
-we compare whether the hash code there matches the one in the emitted C++ code.
-If it does, we use the C++ version, otherwise we use the bytecode.
-
-# Explicit reference counting
-
-As described above, we will have opcodes for increasing/decreasing `vm_obj`s reference counters.
-In Lean3, we perform too many unnecessary increments/decrements.
-A function is responsible for decreasing the reference counter of each argument (i.e., it consumes the argument), and
-for increasing the reference counter of the result. Each argument should be viewed as a resource that is consumed by the function.
-Many optimizations are possible. For example, consider the function
-```
-def proj2 (a : A) (b : B) := b
-```
-A naive compilation into bytecode would produce:
-```
-def proj2 a b :=
-  r := b;
-  inc r;
-  dec a;
-  dec b;
-  return r
-```
-This can be optimized as
-```
-def proj2 a b :=
-  dec a;
-  return b
-```
-We need to explicitly decrement `a` because it was not use by `proj2`.
-The function
-```
-def ex1 (x : X) (y : Y) :=
-  let v1 := f x x,
-      v2 := f x y
-  in h v1 v2
-```
-is compiled as
-```
-def ex1 x y :=
-  inc x;
-  inc x;
-  v1 := f x x;
-  v2 := f x y;
-  r  := h v1 v2;
-  return r
-```
-The reference counter for `x` is incremented twice because it is used 3 times in this function.
-Note that, we don't have to decrement `v1` nor `v2` since they are consumed by `h`.
-We can an instruction `inc2 x` for executing `inc x; inc x` in a single step.
-Now consider a map-like function
-```
-def my_map : list A -> list A
-| []     := []
-| (h::t) := g h :: my_map t
-```
-This function will be compiled as
-```
-def my_map t :=
-switch (cidx t) {
-case 0:
-  return t;
-case 1:
-  h1 := get#0 t;
-  t1 := get#1 t;
-  dec t;
-  h2 := g h1;
-  t2 := my_map t2;
-  r  := mk_list_cons h2 t2;
-  return r
-}
-```
-The instruction `get#<idx> t` returns the field `idx` of the object `t`. It bumps the reference counter of the resulting object, but does not update the reference counter of `t`.
-`mk_list_cons h2 t2` is a function that creates a constructor object with tag `#1` and two pointers `h2` and `t2`. We don't need to decrement
-the reference counters of `h2` and `t2` since they were "consumed" by `mk_list_cons`. We can inline `mk_list_cons` too.
-We can also add a special `dec` instruction for reusing memory cells, and write `my_map` as:
-```
-def my_map t :=
-switch (cidx t) {
-case 0:
-  return t;
-case 1:
-  h1 := get#0 t;
-  t1 := get#1 t;
-  t_cell := dec_core t;
-  h2 := g h1;
-  t2 := my_map t2;
-  r  := mk_list_cons_reusing h2 t2 t_cell;
-  return r
-}
-```
-The `dec_core t` instruction decrements the reference counter of `t`, but does not delete the memory cell if it is zero.
-Then, `mk_list_cons_reusing` will reuse `t`'s memory cell if the counter is 0, and will create a new cell otherwise.
-With this trick, `my_map` will not allocate any constructor object if the input list is not shared.
-To avoid memory leaks, we have to make sure that in each path after `dec_core t`, `t_cell` is used in a `mk_*_reusing` function
-and/or we explicitly delete it using `del t_cell`.
-When the reference counter of `t` is one in `case 1`, the `get#0 t` and `get#1 t` unnecessarily increase the reference counter of the result value just to decrease it again at `dec_core t`. We can avoid this overhead by using the following alternative formulation
-```
-def my_map t :=
-switch (cidx t) {
-case 0:
-  return t;
-case 1:
-  if (ref_count t == 1) {
-    h1     := steal#0 t;
-    t1     := steal#1 t;
-    t_cell := t;
-  } else {
-    h1     := get#0 t;
-    t1     := get#1 t;
-    dec t;
-    t_cell := 0;
-  }
-  h2 := g h1;
-  t2 := my_map t2;
-  r  := mk_constructor_reusing #1 2 t_cell;
-  set#0 r h2;
-  set#1 r t2;
-  return r
-}
-```
-The instruction `steal#<idx> t` is similar to `get#<idx> t`, but it does not increase the reference counter of the resulting object.
-`mk_constructor_reusing #1 2 t_cell` creates a constructor object with tag `#1` and size 2 and reusing `t_cell` if different from 0. The instructions `set#<idx>` are used to initialize the resulting fields.
-The optimization above can be used whenever `t` is dead after the `case`, and an object of same size is created.
-Note that if `t` is a list of arrays and it is not shared, then `g h1` will also be able to perform destructive updates.
-Remark: suppose the `i`-th field in `case` branch is not used, then instead of using `steal#i t`, we use `dec#i t` to decrement the reference counter of the `i`-th field.
-
-TODO: create experiments to check whether the optimization above is relevant or not.
-
-# Tail recursion
-
-TODO
-
-# Unboxed products and sums
-
-TODO
-
-# Memory management
-
-Lean3 VM objects are not thread safe: they do not use atomic
-operations for updating the reference counter, and we use a small
-object memory allocator. The main motivation was performance.
-We evaluated these design decisions again, and did not observe any
-performance impact when we used atomic operations for updating
-the reference counter and removed the small object allocator.
-The experiments were conducted using OSX and Linux.
-We considered two benchmarks: core lib compilation, and a small Lean
-program attached in the end of this section.
-In both platforms and benchmarks no significant difference was observed.
-Then, we disable the `memory_pool` object, and again no difference
-in performance was observed.
-We believe the memory allocators in the C++ runtime have been improved.
-This is consistent with our observation that building Lean with `tcmalloc`
-does not improve the performance significantly anymore.
-However, it is not clear why using std::atomic does not impact performance
-anymore.
-
-```
-def foo (n : nat) : nat :=
-(((list.iota n).map (+10)).map (+30)).length
-
-#eval nat.repeat (λ i _, foo i) 4000 0
-```