Note about Mathlib/Init/

The files in Mathlib/Init are leftovers from the port from Mathlib3. (They contain content moved from lean3 itself that Mathlib needed but was not moved to lean4.)

We intend to move all the content of these files out into the main Mathlib directory structure. Contributions assisting with this are appreciated.

#align statements without corresponding declarations (i.e. because the declaration is in Batteries or Lean) can be left here. These will be deleted soon so will not significantly delay deleting otherwise empty Init files.

Realignments from lean 3 init

These are collected in one place only for ease of maintenance of a bunch of files that would otherwise be nothing but #aligns. Please use the respective files in Mathlib.Init if there are actual theorems in the files.

init.algebra.classes

init.cc_lemmas

init.classical

init.coe

init.control.alternative

init.control.applicative

init.control.except

init.control.functor

init.control.lift

init.control.monad

init.data.array.default

init.data.char.basic

init.data.char.classes

init.data.char.default

init.data.default

init.data.fin.basic

init.data.int.comp_lemmas

init.data.int.default

init.data.list.basic

init.data.nat.basic

init.data.nat.div

init.data.nat.lemmas

init.data.option.instances

init.data.ordering.basic

init.data.prod

init.data.punit

init.data.quot

init.data.random

init.data.repr

init.data.setoid

init.data.sigma.basic

init.data.string.basic

init.data.subtype.basic

init.data.sum.basic

init.data.sum.default

init.data.to_string

init.data.unsigned.basic

init.data.unsigned.default

init.default

init.function

init.funext

init.meta.exceptional

init.meta.feature_search

init.meta.float

init.meta.format

init.meta.json

init.meta.level

init.meta.name

init.meta.options

init.meta.rb_map

init.meta.task

init.meta.widget.basic

init.meta.widget.default

init.meta.widget.html_cmd

init.meta.widget.interactive_expr

init.meta.widget.replace_save_info

init.meta.widget.tactic_component

init.prelude

init.propext

init.util

init.version

init.wf