Init.Prelude

/--
The identity function. `id` takes an implicit argument `α : Sort u`
(a type in any universe), and an argument `a : α`, and returns `a`.

Although this may look like a useless function, one application of the identity
function is to explicitly put a type on an expression. If `e` has type `T`,
and `T'` is definitionally equal to `T`, then `@id T' e` typechecks, and Lean
knows that this expression has type `T'` rather than `T`. This can make a
difference for typeclass inference, since `T` and `T'` may have different
typeclass instances on them. `show T' from e` is sugar for an `@id T' e`
expression.
-/
@[inline] def id {α : Sort u} (a : α) : α := a

/--
Function composition, usually written with the infix operator `∘`. A new function is created from
two existing functions, where one function's output is used as input to the other.

Examples:
 * `Function.comp List.reverse (List.drop 2) [3, 2, 4, 1] = [1, 4]`
 * `(List.reverse ∘ List.drop 2) [3, 2, 4, 1] = [1, 4]`
-/
@[inline] def Function.comp {α : Sort u} {β : Sort v} {δ : Sort w} (f : β → δ) (g : α → β) : α → δ :=
  fun x => f (g x)

/--
The constant function that ignores its argument.

If `a : α`, then `Function.const β a : β → α` is the “constant function with value `a`”. For all
arguments `b : β`, `Function.const β a b = a`.

Examples:
 * `Function.const Bool 10 true = 10`
 * `Function.const Bool 10 false = 10`
 * `Function.const String 10 "any string" = 10`
-/
@[inline] def Function.const {α : Sort u} (β : Sort v) (a : α) : β → α :=
  fun _ => a

/--
The encoding of `let_fun x := v; b` is `letFun v (fun x => b)`.
This is equal to `(fun x => b) v`, so the value of `x` is not accessible to `b`.
This is in contrast to `let x := v; b`, where the value of `x` is accessible to `b`.

There is special support for `letFun`.
Both WHNF and `simp` are aware of `letFun` and can reduce it when zeta reduction is enabled,
despite the fact it is marked `irreducible`.
For metaprogramming, the function `Lean.Expr.letFun?` can be used to recognize a `let_fun` expression
to extract its parts as if it were a `let` expression.
-/
@[irreducible] def letFun {α : Sort u} {β : α → Sort v} (v : α) (f : (x : α) → β x) : β v := f v

/--
`inferInstance` synthesizes a value of any target type by typeclass
inference. This function has the same type signature as the identity
function, but the square brackets on the `[i : α]` argument means that it will
attempt to construct this argument by typeclass inference. (This will fail if
`α` is not a `class`.) Example:
```
#check (inferInstance : Inhabited Nat) -- Inhabited Nat

def foo : Inhabited (Nat × Nat) :=
  inferInstance

example : foo.default = (default, default) :=
  rfl
```
-/
abbrev inferInstance {α : Sort u} [i : α] : α := i

/-- `inferInstanceAs α` synthesizes a value of any target type by typeclass
inference. This is just like `inferInstance` except that `α` is given
explicitly instead of being inferred from the target type. It is especially
useful when the target type is some `α'` which is definitionally equal to `α`,
but the instance we are looking for is only registered for `α` (because
typeclass search does not unfold most definitions, but definitional equality
does.) Example:
```
#check inferInstanceAs (Inhabited Nat) -- Inhabited Nat
```
-/
abbrev inferInstanceAs (α : Sort u) [i : α] : α := i

/--
The canonical universe-polymorphic type with just one element.

It should be used in contexts that require a type to be universe polymorphic, thus disallowing
`Unit`.
-/
inductive PUnit : Sort u where
  /-- The only element of the universe-polymorphic unit type. -/
  | unit : PUnit

/--
The canonical type with one element. This element is written `()`.

`Unit` has a number of uses:
 * It can be used to model control flow that returns from a function call without providing other
   information.
 * Monadic actions that return `Unit` have side effects without computing values.
 * In polymorphic types, it can be used to indicate that no data is to be stored in a particular
   field.
-/
abbrev Unit : Type := PUnit

/--
The only element of the unit type.

It can be written as an empty tuple: `()`.
-/
@[match_pattern] abbrev Unit.unit : Unit := PUnit.unit

/-- Marker for information that has been erased by the code generator. -/
unsafe axiom lcErased : Type

/-- Marker for type dependency that has been erased by the code generator. -/
unsafe axiom lcAny : Type

/--
Auxiliary unsafe constant used by the Compiler when erasing proofs from code.

It may look strange to have an axiom that says "every proposition is true",
since this is obviously unsound, but the `unsafe` marker ensures that the
kernel will not let this through into regular proofs. The lower levels of the
code generator don't need proofs in terms, so this is used to stub the proofs
out.
-/
unsafe axiom lcProof {α : Prop} : α

/--
Auxiliary unsafe constant used by the Compiler when erasing casts.
-/
unsafe axiom lcCast {α : Sort u} {β : Sort v} (a : α) : β

/--
Auxiliary unsafe constant used by the Compiler to mark unreachable code.

Like `lcProof`, this is an `unsafe axiom`, which means that even though it is
not sound, the kernel will not let us use it for regular proofs.

Executing this expression to actually synthesize a value of type `α` causes
**immediate undefined behavior**, and the compiler does take advantage of this
to optimize the code assuming that it is not called. If it is not optimized out,
it is likely to appear as a print message saying "unreachable code", but this
behavior is not guaranteed or stable in any way.
-/
unsafe axiom lcUnreachable {α : Sort u} : α

/--
`True` is a proposition and has only an introduction rule, `True.intro : True`.
In other words, `True` is simply true, and has a canonical proof, `True.intro`
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)
-/
inductive True : Prop where
  /-- `True` is true, and `True.intro` (or more commonly, `trivial`)
  is the proof. -/
  | intro : True

/--
`False` is the empty proposition. Thus, it has no introduction rules.
It represents a contradiction. `False` elimination rule, `False.rec`,
expresses the fact that anything follows from a contradiction.
This rule is sometimes called ex falso (short for ex falso sequitur quodlibet),
or the principle of explosion.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)
-/
inductive False : Prop

/--
The empty type. It has no constructors.

Use `Empty.elim` in contexts where a value of type `Empty` is in scope.
-/
inductive Empty : Type

/--
The universe-polymorphic empty type, with no constructors.

`PEmpty` can be used in any universe, but this flexibility can lead to worse error messages and more
challenges with universe level unification. Prefer the type `Empty` or the proposition `False` when
possible.
-/
inductive PEmpty : Sort u where

/--
`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)
-/
def Not (a : Prop) : Prop := a → False

/--
`False.elim : False → C` says that from `False`, any desired proposition
`C` holds. Also known as ex falso quodlibet (EFQ) or the principle of explosion.

The target type is actually `C : Sort u` which means it works for both
propositions and types. When executed, this acts like an "unreachable"
instruction: it is **undefined behavior** to run, but it will probably print
"unreachable code". (You would need to construct a proof of false to run it
anyway, which you can only do using `sorry` or unsound axioms.)
-/
@[macro_inline] def False.elim {C : Sort u} (h : False) : C :=
  h.rec

/--
Anything follows from two contradictory hypotheses. Example:
```
example (hp : p) (hnp : ¬p) : q := absurd hp hnp
```
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)
-/
@[macro_inline] def absurd {a : Prop} {b : Sort v} (h₁ : a) (h₂ : Not a) : b :=
  (h₂ h₁).rec

/--
The equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
-/
inductive Eq : α → α → Prop where
  /-- `Eq.refl a : a = a` is reflexivity, the unique constructor of the
  equality type. See also `rfl`, which is usually used instead. -/
  | refl (a : α) : Eq a a

/-- Non-dependent recursor for the equality type. -/
@[simp] abbrev Eq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} (m : motive a) {b : α} (h : Eq a b) : motive b :=
  h.rec m

/--
`rfl : a = a` is the unique constructor of the equality type. This is the
same as `Eq.refl` except that it takes `a` implicitly instead of explicitly.

This is a more powerful theorem than it may appear at first, because although
the statement of the theorem is `a = a`, Lean will allow anything that is
definitionally equal to that type. So, for instance, `2 + 2 = 4` is proven in
Lean by `rfl`, because both sides are the same up to definitional equality.
-/
@[match_pattern] def rfl {α : Sort u} {a : α} : Eq a a := Eq.refl a

/-- `id x = x`, as a `@[simp]` lemma. -/
@[simp] theorem id_eq (a : α) : Eq (id a) a := rfl

/--
The substitution principle for equality. If `a = b ` and `P a` holds,
then `P b` also holds. We conventionally use the name `motive` for `P` here,
so that you can specify it explicitly using e.g.
`Eq.subst (motive := fun x => x < 5)` if it is not otherwise inferred correctly.

This theorem is the underlying mechanism behind the `rw` tactic, which is
essentially a fancy algorithm for finding good `motive` arguments to usefully
apply this theorem to replace occurrences of `a` with `b` in the goal or
hypotheses.

For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
-/
theorem Eq.subst {α : Sort u} {motive : α → Prop} {a b : α} (h₁ : Eq a b) (h₂ : motive a) : motive b :=
  Eq.ndrec h₂ h₁

/--
Equality is symmetric: if `a = b` then `b = a`.

Because this is in the `Eq` namespace, if you have a variable `h : a = b`,
`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.

For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
-/
@[symm] theorem Eq.symm {α : Sort u} {a b : α} (h : Eq a b) : Eq b a :=
  h ▸ rfl

/--
Equality is transitive: if `a = b` and `b = c` then `a = c`.

Because this is in the `Eq` namespace, if you have variables or expressions
`h₁ : a = b` and `h₂ : b = c`, you can use `h₁.trans h₂ : a = c` as shorthand
for `Eq.trans h₁ h₂`.

For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
-/
theorem Eq.trans {α : Sort u} {a b c : α} (h₁ : Eq a b) (h₂ : Eq b c) : Eq a c :=
  h₂ ▸ h₁

/--
Cast across a type equality. If `h : α = β` is an equality of types, and
`a : α`, then `a : β` will usually not typecheck directly, but this function
will allow you to work around this and embed `a` in type `β` as `cast h a : β`.

It is best to avoid this function if you can, because it is more complicated
to reason about terms containing casts, but if the types don't match up
definitionally sometimes there isn't anything better you can do.

For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
-/
@[macro_inline] def cast {α β : Sort u} (h : Eq α β) (a : α) : β :=
  h.rec a

/--
Congruence in the function argument: if `a₁ = a₂` then `f a₁ = f a₂` for
any (nondependent) function `f`. This is more powerful than it might look at first, because
you can also use a lambda expression for `f` to prove that
`<something containing a₁> = <something containing a₂>`. This function is used
internally by tactics like `congr` and `simp` to apply equalities inside
subterms.

For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
-/
theorem congrArg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : Eq a₁ a₂) : Eq (f a₁) (f a₂) :=
  h ▸ rfl

/--
Congruence in both function and argument. If `f₁ = f₂` and `a₁ = a₂` then
`f₁ a₁ = f₂ a₂`. This only works for nondependent functions; the theorem
statement is more complex in the dependent case.

For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
-/
theorem congr {α : Sort u} {β : Sort v} {f₁ f₂ : α → β} {a₁ a₂ : α} (h₁ : Eq f₁ f₂) (h₂ : Eq a₁ a₂) : Eq (f₁ a₁) (f₂ a₂) :=
  h₁ ▸ h₂ ▸ rfl

/-- Congruence in the function part of an application: If `f = g` then `f a = g a`. -/
theorem congrFun {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : Eq f g) (a : α) : Eq (f a) (g a) :=
  h ▸ rfl

/--
Unsafe auxiliary constant used by the compiler to erase `Quot.lift`.
-/
unsafe axiom Quot.lcInv {α : Sort u} {r : α → α → Prop} (q : Quot r) : α

/--
Heterogeneous equality. `HEq a b` asserts that `a` and `b` have the same
type, and casting `a` across the equality yields `b`, and vice versa.

You should avoid using this type if you can. Heterogeneous equality does not
have all the same properties as `Eq`, because the assumption that the types of
`a` and `b` are equal is often too weak to prove theorems of interest. One
important non-theorem is the analogue of `congr`: If `HEq f g` and `HEq x y`
and `f x` and `g y` are well typed it does not follow that `HEq (f x) (g y)`.
(This does follow if you have `f = g` instead.) However if `a` and `b` have
the same type then `a = b` and `HEq a b` are equivalent.
-/
inductive HEq : {α : Sort u} → α → {β : Sort u} → β → Prop where
  /-- Reflexivity of heterogeneous equality. -/
  | refl (a : α) : HEq a a

/-- A version of `HEq.refl` with an implicit argument. -/
@[match_pattern] protected def HEq.rfl {α : Sort u} {a : α} : HEq a a :=
  HEq.refl a

/--
The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.
-/
structure Prod (α : Type u) (β : Type v) where
  /--
  Constructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.
  -/
  mk ::
  /-- The first element of a pair. -/
  fst : α
  /-- The second element of a pair. -/
  snd : β

/--
A product type in which the types may be propositions, usually written `α ×' β`.

This type is primarily used internally and as an implementation detail of proof automation. It is
rarely useful in hand-written code.
-/
structure PProd (α : Sort u) (β : Sort v) where
  /-- The first element of a pair. -/
  fst : α
  /-- The second element of a pair. -/
  snd : β

/--
A product type in which both `α` and `β` are in the same universe.

It is called `MProd` is because it is the *universe-monomorphic* product type.
-/
structure MProd (α β : Type u) where
  /-- The first element of a pair. -/
  fst : α
  /-- The second element of a pair. -/
  snd : β

/--
`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.
-/
@[pp_using_anonymous_constructor]
structure And (a b : Prop) : Prop where
  /-- `And.intro : a → b → a ∧ b` is the constructor for the And operation. -/
  intro ::
  /-- Extract the left conjunct from a conjunction. `h : a ∧ b` then
  `h.left`, also notated as `h.1`, is a proof of `a`. -/
  left : a
  /-- Extract the right conjunct from a conjunction. `h : a ∧ b` then
  `h.right`, also notated as `h.2`, is a proof of `b`. -/
  right : b

/--
`Or a b`, or `a ∨ b`, is the disjunction of propositions. There are two
constructors for `Or`, called `Or.inl : a → a ∨ b` and `Or.inr : b → a ∨ b`,
and you can use `match` or `cases` to destruct an `Or` assumption into the
two cases.
-/
inductive Or (a b : Prop) : Prop where
  /-- `Or.inl` is "left injection" into an `Or`. If `h : a` then `Or.inl h : a ∨ b`. -/
  | inl (h : a) : Or a b
  /-- `Or.inr` is "right injection" into an `Or`. If `h : b` then `Or.inr h : a ∨ b`. -/
  | inr (h : b) : Or a b

/-- Alias for `Or.inl`. -/
theorem Or.intro_left (b : Prop) (h : a) : Or a b :=
  Or.inl h

/-- Alias for `Or.inr`. -/
theorem Or.intro_right (a : Prop) (h : b) : Or a b :=
  Or.inr h

/--
Proof by cases on an `Or`. If `a ∨ b`, and both `a` and `b` imply
proposition `c`, then `c` is true.
-/
theorem Or.elim {c : Prop} (h : Or a b) (left : a → c) (right : b → c) : c :=
  match h with
  | Or.inl h => left h
  | Or.inr h => right h

theorem Or.resolve_left  (h: Or a b) (na : Not a) : b := h.elim (absurd · na) id

theorem Or.resolve_right (h: Or a b) (nb : Not b) : a := h.elim id (absurd · nb)

theorem Or.neg_resolve_left  (h : Or (Not a) b) (ha : a) : b := h.elim (absurd ha) id

theorem Or.neg_resolve_right (h : Or a (Not b)) (nb : b) : a := h.elim id (absurd nb)

/--
The Boolean values, `true` and `false`.

Logically speaking, this is equivalent to `Prop` (the type of propositions). The distinction is
important for programming: both propositions and their proofs are erased in the code generator,
while `Bool` corresponds to the Boolean type in most programming languages and carries precisely one
bit of run-time information.
-/
inductive Bool : Type where
  /-- The Boolean value `false`, not to be confused with the proposition `False`. -/
  | false : Bool
  /-- The Boolean value `true`, not to be confused with the proposition `True`. -/
  | true : Bool

/--
All the elements of a type that satisfy a predicate.

`Subtype p`, usually written `{ x : α // p x }` or `{ x // p x }`, contains all elements `x : α` for
which `p x` is true. Its constructor is a pair of the value and the proof that it satisfies the
predicate. In run-time code, `{ x : α // p x }` is represented identically to `α`.

There is a coercion from `{ x : α // p x }` to `α`, so elements of a subtype may be used where the
underlying type is expected.

Examples:
 * `{ n : Nat // n % 2 = 0 }` is the type of even numbers.
 * `{ xs : Array String // xs.size = 5 }` is the type of arrays with five `String`s.
 * Given `xs : List α`, `List { x : α // x ∈ xs }` is the type of lists in which all elements are
   contained in `xs`.
-/
@[pp_using_anonymous_constructor]
structure Subtype {α : Sort u} (p : α → Prop) where
  /--
  The value in the underlying type that satisfies the predicate.
  -/
  val : α
  /--
  The proof that `val` satisfies the predicate `p`.
  -/
  property : p val

/--
Gadget for optional parameter support.

A binder like `(x : α := default)` in a declaration is syntax sugar for
`x : optParam α default`, and triggers the elaborator to attempt to use
`default` to supply the argument if it is not supplied.
-/
@[reducible] def optParam (α : Sort u) (default : α) : Sort u := α

/--
Gadget for marking output parameters in type classes.

For example, the `Membership` class is defined as:
```
class Membership (α : outParam (Type u)) (γ : Type v)
```
This means that whenever a typeclass goal of the form `Membership ?α ?γ` comes
up, Lean will wait to solve it until `?γ` is known, but then it will run
typeclass inference, and take the first solution it finds, for any value of `?α`,
which thereby determines what `?α` should be.

This expresses that in a term like `a ∈ s`, `s` might be a `Set α` or
`List α` or some other type with a membership operation, and in each case
the "member" type `α` is determined by looking at the container type.
-/
@[reducible] def outParam (α : Sort u) : Sort u := α

/--
Gadget for marking semi output parameters in type classes.

Semi-output parameters influence the order in which arguments to type class
instances are processed.  Lean determines an order where all non-(semi-)output
parameters to the instance argument have to be figured out before attempting to
synthesize an argument (that is, they do not contain assignable metavariables
created during TC synthesis). This rules out instances such as `[Mul β] : Add
α` (because `β` could be anything). Marking a parameter as semi-output is a
promise that instances of the type class will always fill in a value for that
parameter.

For example, the `Coe` class is defined as:
```
class Coe (α : semiOutParam (Sort u)) (β : Sort v)
```
This means that all `Coe` instances should provide a concrete value for `α`
(i.e., not an assignable metavariable). An instance like `Coe Nat Int` or `Coe
α (Option α)` is fine, but `Coe α Nat` is not since it does not provide a value
for `α`.
-/
@[reducible] def semiOutParam (α : Sort u) : Sort u := α

/-- Auxiliary declaration used to implement named patterns like `x@h:p`. -/
@[reducible] def namedPattern {α : Sort u} (x a : α) (h : Eq x a) : α := a

/--
Auxiliary axiom used to implement the `sorry` term and tactic.

The `sorry` term/tactic expands to `sorryAx _ (synthetic := false)`.
It is intended for stubbing-out incomplete parts of a value or proof while still having a syntactically correct skeleton.
Lean will give a warning whenever a declaration uses `sorry`, so you aren't likely to miss it,
but you can check if a declaration depends on `sorry` either directly or indirectly by looking for `sorryAx` in the output
of the `#print axioms my_thm` command.

The `synthetic` flag is false when a `sorry` is written explicitly by the user, but it is
set to `true` when a tactic fails to prove a goal, or if there is a type error
in the expression. A synthetic `sorry` acts like a regular one, except that it
suppresses follow-up errors in order to prevent an error from causing a cascade
of other errors because the desired term was not constructed.
-/
@[extern "lean_sorry", never_extract]
axiom sorryAx (α : Sort u) (synthetic : Bool) : α

theorem ne_false_of_eq_true : {b : Bool} → Eq b true → Not (Eq b false)
  | true, _  => fun h => Bool.noConfusion h
  | false, h => Bool.noConfusion h

theorem ne_true_of_eq_false : {b : Bool} → Eq b false → Not (Eq b true)
  | true, h  => Bool.noConfusion h
  | false, _ => fun h => Bool.noConfusion h

/--
`Inhabited α` is a typeclass that says that `α` has a designated element,
called `(default : α)`. This is sometimes referred to as a "pointed type".

This class is used by functions that need to return a value of the type
when called "out of domain". For example, `Array.get! arr i : α` returns
a value of type `α` when `arr : Array α`, but if `i` is not in range of
the array, it reports a panic message, but this does not halt the program,
so it must still return a value of type `α` (and in fact this is required
for logical consistency), so in this case it returns `default`.
-/
class Inhabited (α : Sort u) where
  /-- `default` is a function that produces a "default" element of any
  `Inhabited` type. This element does not have any particular specified
  properties, but it is often an all-zeroes value. -/
  default : α

/--
`Nonempty α` is a typeclass that says that `α` is not an empty type,
that is, there exists an element in the type. It differs from `Inhabited α`
in that `Nonempty α` is a `Prop`, which means that it does not actually carry
an element of `α`, only a proof that *there exists* such an element.
Given `Nonempty α`, you can construct an element of `α` *nonconstructively*
using `Classical.choice`.
-/
class inductive Nonempty (α : Sort u) : Prop where
  /-- If `val : α`, then `α` is nonempty. -/
  | intro (val : α) : Nonempty α

/--
**The axiom of choice**. `Nonempty α` is a proof that `α` has an element,
but the element itself is erased. The axiom `choice` supplies a particular
element of `α` given only this proof.

The textbook axiom of choice normally makes a family of choices all at once,
but that is implied from this formulation, because if `α : ι → Type` is a
family of types and `h : ∀ i, Nonempty (α i)` is a proof that they are all
nonempty, then `fun i => Classical.choice (h i) : ∀ i, α i` is a family of
chosen elements. This is actually a bit stronger than the ZFC choice axiom;
this is sometimes called "[global choice](https://en.wikipedia.org/wiki/Axiom_of_global_choice)".

In Lean, we use the axiom of choice to derive the law of excluded middle
(see `Classical.em`), so it will often show up in axiom listings where you
may not expect. You can use `#print axioms my_thm` to find out if a given
theorem depends on this or other axioms.

This axiom can be used to construct "data", but obviously there is no algorithm
to compute it, so Lean will require you to mark any definition that would
involve executing `Classical.choice` or other axioms as `noncomputable`, and
will not produce any executable code for such definitions.
-/
axiom Classical.choice {α : Sort u} : Nonempty α → α

/--
The elimination principle for `Nonempty α`. If `Nonempty α`, and we can
prove `p` given any element `x : α`, then `p` holds. Note that it is essential
that `p` is a `Prop` here; the version with `p` being a `Sort u` is equivalent
to `Classical.choice`.
-/
protected theorem Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂ : α → p) : p :=
  match h₁ with
  | intro a => h₂ a

instance {α : Sort u} [Inhabited α] : Nonempty α :=
  ⟨default⟩

/--
A variation on `Classical.choice` that uses typeclass inference to
infer the proof of `Nonempty α`.
-/
noncomputable def Classical.ofNonempty {α : Sort u} [Nonempty α] : α :=
  Classical.choice inferInstance

instance {α : Sort u} {β : Sort v} [Nonempty β] : Nonempty (α → β) :=
  Nonempty.intro fun _ => Classical.ofNonempty

instance Pi.instNonempty {α : Sort u} {β : α → Sort v} [(a : α) → Nonempty (β a)] :
    Nonempty ((a : α) → β a) :=
  Nonempty.intro fun _ => Classical.ofNonempty

instance : Inhabited (Sort u) where
  default := PUnit

instance (α : Sort u) {β : Sort v} [Inhabited β] : Inhabited (α → β) where
  default := fun _ => default

instance Pi.instInhabited {α : Sort u} {β : α → Sort v} [(a : α) → Inhabited (β a)] :
    Inhabited ((a : α) → β a) where
  default := fun _ => default

Inhabited for Bool

/--
Lifts a proposition or type to a higher universe level.

`PLift α` wraps a proof or value of type `α`. The resulting type is in the next largest universe
after that of `α`. In particular, propositions become data.

The related type `ULift` can be used to lift a non-proposition type by any number of levels.

Examples:
 * `(False : Prop)`
 * `(PLift False : Type)`
 * `([.up (by trivial), .up (by simp), .up (by decide)] : List (PLift True))`
 * `(Nat : Type 0)`
 * `(PLift Nat : Type 1)`
-/
structure PLift (α : Sort u) : Type u where
  /-- Wraps a proof or value to increase its type's universe level by 1. -/
  up ::
  /-- Extracts a wrapped proof or value from a universe-lifted proposition or type. -/
  down : α

/-- Bijection between `α` and `PLift α` -/
theorem PLift.up_down {α : Sort u} (b : PLift α) : Eq (up (down b)) b := rfl

/-- Bijection between `α` and `PLift α` -/
theorem PLift.down_up {α : Sort u} (a : α) : Eq (down (up a)) a := rfl

/--
`NonemptyType.{u}` is the type of nonempty types in universe `u`.
It is mainly used in constant declarations where we wish to introduce a type
and simultaneously assert that it is nonempty, but otherwise make the type
opaque.
-/
def NonemptyType := Subtype fun α : Type u => Nonempty α

/-- The underlying type of a `NonemptyType`. -/
abbrev NonemptyType.type (type : NonemptyTypeNonemptyType.{u}) : Type u :=
  type.val

/-- `NonemptyType` is inhabited, because `PUnit` is a nonempty type. -/
instance : Inhabited NonemptyTypeNonemptyType.{u} where
  default := ⟨PUnit, ⟨⟨⟩⟩⟩

/--
Lifts a type to a higher universe level.

`ULift α` wraps a value of type `α`. Instead of occupying the same universe as `α`, which would be
the minimal level, it takes a further level parameter and occupies their minimum. The resulting type
may occupy any universe that's at least as large as that of `α`.

The resulting universe of the lifting operator is the first parameter, and may be written explicitly
while allowing `α`'s level to be inferred.

The related type `PLift` can be used to lift a proposition or type by one level.

Examples:
 * `(Nat : Type 0)`
 * `(ULift Nat : Type 0)`
 * `(ULift Nat : Type 1)`
 * `(ULift Nat : Type 5)`
 * `(ULift.{7} (PUnit : Type 3) : Type 7)`
-/
-- The universe variable `r` is written first so that `ULift.{r} α` can be used
-- when `s` can be inferred from the type of `α`.
structure ULift.{r, s} (α : Type s) : Type (max s r) where
  /-- Wraps a value to increase its type's universe level. -/
  up ::
  /-- Extracts a wrapped value from a universe-lifted type. -/
  down : α

/-- Bijection between `α` and `ULift.{v} α` -/
theorem ULift.up_down {α : Type u} (b : ULift.{v} α) : Eq (up (down b)) b := rfl

/-- Bijection between `α` and `ULift.{v} α` -/
theorem ULift.down_up {α : Type u} (a : α) : Eq (down (up.{v} a)) a := rfl

/--
Either a proof that `p` is true or a proof that `p` is false. This is equivalent to a `Bool` paired
with a proof that the `Bool` is `true` if and only if `p` is true.

`Decidable` instances are primarily used via `if`-expressions and the tactic `decide`. In
conditional expressions, the `Decidable` instance for the proposition is used to select a branch. At
run time, this case distinction code is identical to that which would be generated for a
`Bool`-based conditional. In proofs, the tactic `decide` synthesizes an instance of `Decidable p`,
attempts to reduce it to `isTrue h`, and then succeeds with the proof `h` if it can.

Because `Decidable` carries data, when writing `@[simp]` lemmas which include a `Decidable` instance
on the LHS, it is best to use `{_ : Decidable p}` rather than `[Decidable p]` so that non-canonical
instances can be found via unification rather than instance synthesis.
-/
class inductive Decidable (p : Prop) where
  /-- Proves that `p` is decidable by supplying a proof of `¬p` -/
  | isFalse (h : Not p) : Decidable p
  /-- Proves that `p` is decidable by supplying a proof of `p` -/
  | isTrue (h : p) : Decidable p

/--
Converts a decidable proposition into a `Bool`.

If `p : Prop` is decidable, then `decide p : Bool` is the Boolean value
that is `true` if `p` is true and `false` if `p` is false.
-/
@[inline_if_reduce, nospecialize] def Decidable.decide (p : Prop) [h : Decidable p] : Bool :=
  h.casesOn (fun _ => false) (fun _ => true)

/--
A decidable predicate.

A predicate is decidable if the corresponding proposition is `Decidable` for each possible argument.
-/
abbrev DecidablePred {α : Sort u} (r : α → Prop) :=
  (a : α) → Decidable (r a)

/--
A decidable relation.

A relation is decidable if the corresponding proposition is `Decidable` for all possible arguments.
-/
abbrev DecidableRel {α : Sort u} {β : Sort v} (r : α → β → Prop) :=
  (a : α) → (b : β) → Decidable (r a b)

/--
Propositional equality is `Decidable` for all elements of a type.

In other words, an instance of `DecidableEq α` is a means of deciding the proposition `a = b` is
for all `a b : α`.
-/
abbrev DecidableEq (α : Sort u) :=
  (a b : α) → Decidable (Eq a b)

/--
Checks whether two terms of a type are equal using the type's `DecidableEq` instance.
-/
def decEq {α : Sort u} [inst : DecidableEq α] (a b : α) : Decidable (Eq a b) :=
  inst a b

theorem decide_eq_true : [inst : Decidable p] → p → Eq (decide p) true
  | isTrue  _, _   => rfl
  | isFalse h₁, h₂ => absurd h₂ h₁

theorem decide_eq_false : [Decidable p] → Not p → Eq (decide p) false
  | isTrue  h₁, h₂ => absurd h₁ h₂
  | isFalse _, _   => rfl

theorem of_decide_eq_true [inst : Decidable p] : Eq (decide p) true → p := fun h =>
  match (generalizing := false) inst with
  | isTrue  h₁ => h₁
  | isFalse h₁ => absurd h (ne_true_of_eq_false (decide_eq_false h₁))

theorem of_decide_eq_false [inst : Decidable p] : Eq (decide p) false → Not p := fun h =>
  match (generalizing := false) inst with
  | isTrue  h₁ => absurd h (ne_false_of_eq_true (decide_eq_true h₁))
  | isFalse h₁ => h₁

theorem of_decide_eq_self_eq_true [inst : DecidableEq α] (a : α) : Eq (decide (Eq a a)) true :=
  match (generalizing := false) inst a a with
  | isTrue  _  => rfl
  | isFalse h₁ => absurd rfl h₁

/--
Decides whether two Booleans are equal.

This function should normally be called via the `DecidableEq Bool` instance that it exists to
support.
-/
@[inline] def Bool.decEq (a b : Bool) : Decidable (Eq a b) :=
   match a, b with
   | false, false => isTrue rfl
   | false, true  => isFalse (fun h => Bool.noConfusion h)
   | true, false  => isFalse (fun h => Bool.noConfusion h)
   | true, true   => isTrue rfl

@[inline] instance : DecidableEq Bool :=
   Bool.decEq

/--
`BEq α` is a typeclass for supplying a boolean-valued equality relation on
`α`, notated as `a == b`. Unlike `DecidableEq α` (which uses `a = b`), this
is `Bool` valued instead of `Prop` valued, and it also does not have any
axioms like being reflexive or agreeing with `=`. It is mainly intended for
programming applications. See `LawfulBEq` for a version that requires that
`==` and `=` coincide.

Typically we prefer to put the "more variable" term on the left,
and the "more constant" term on the right.
-/
class BEq (α : Type u) where
  /-- Boolean equality, notated as `a == b`. -/
  beq : α → α → Bool

instance [DecidableEq α] : BEq α where
  beq a b := decide (Eq a b)

/--
"Dependent" if-then-else, normally written via the notation `if h : c then t(h) else e(h)`,
is sugar for `dite c (fun h => t(h)) (fun h => e(h))`, and it is the same as
`if c then t else e` except that `t` is allowed to depend on a proof `h : c`,
and `e` can depend on `h : ¬c`. (Both branches use the same name for the hypothesis,
even though it has different types in the two cases.)

We use this to be able to communicate the if-then-else condition to the branches.
For example, `Array.get arr i h` expects a proof `h : i < arr.size` in order to
avoid a bounds check, so you can write `if h : i < arr.size then arr.get i h else ...`
to avoid the bounds check inside the if branch. (Of course in this case we have only
lifted the check into an explicit `if`, but we could also use this proof multiple times
or derive `i < arr.size` from some other proposition that we are checking in the `if`.)
-/
@[macro_inline] def dite {α : Sort u} (c : Prop) [h : Decidable c] (t : c → α) (e : Not c → α) : α :=
  h.casesOn e t

/--
`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to
return `t` or `e` depending on whether `c` is true or false. The explicit argument
`c : Prop` does not have any actual computational content, but there is an additional
`[Decidable c]` argument synthesized by typeclass inference which actually
determines how to evaluate `c` to true or false. Write `if h : c then t else e`
instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact
that `c` is true/false.
-/
/-
Because Lean uses a strict (call-by-value) evaluation strategy, the signature of this
function is problematic in that it would require `t` and `e` to be evaluated before
calling the `ite` function, which would cause both sides of the `if` to be evaluated.
Even if the result is discarded, this would be a big performance problem,
and is undesirable for users in any case. To resolve this, `ite` is marked as
`@[macro_inline]`, which means that it is unfolded during code generation, and
the definition of the function uses `fun _ => t` and `fun _ => e` so this recovers
the expected "lazy" behavior of `if`: the `t` and `e` arguments delay evaluation
until `c` is known.
-/
@[macro_inline] def ite {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) : α :=
  h.casesOn (fun _ => e) (fun _ => t)

@[macro_inline] instance {p q} [dp : Decidable p] [dq : Decidable q] : Decidable (And p q) :=
  match dp with
  | isTrue  hp =>
    match dq with
    | isTrue hq  => isTrue ⟨hp, hq⟩
    | isFalse hq => isFalse (fun h => hq (And.right h))
  | isFalse hp =>
    isFalse (fun h => hp (And.left h))

@[macro_inline] instance [dp : Decidable p] [dq : Decidable q] : Decidable (Or p q) :=
  match dp with
  | isTrue  hp => isTrue (Or.inl hp)
  | isFalse hp =>
    match dq with
    | isTrue hq  => isTrue (Or.inr hq)
    | isFalse hq =>
      isFalse fun h => match h with
        | Or.inl h => hp h
        | Or.inr h => hq h

instance [dp : Decidable p] : Decidable (Not p) :=
  match dp with
  | isTrue hp  => isFalse (absurd hp)
  | isFalse hp => isTrue hp

/--
The conditional function.

`cond c x y` is the same as `if c then x else y`, but optimized for a Boolean condition rather than
a decidable proposition. It can also be written using the notation `bif c then x else y`.

Just like `ite`, `cond` is declared `@[macro_inline]`, which causes applications of `cond` to be
unfolded. As a result, `x` and `y` are not evaluated at runtime until one of them is selected, and
only the selected branch is evaluated.
-/
@[macro_inline] def cond {α : Sort u} (c : Bool) (x y : α) : α :=
  match c with
  | true  => x
  | false => y

/--
The dependent conditional function, in which each branch is provided with a local assumption about
the condition's value. This allows the value to be used in proofs as well as for control flow.

`dcond c (fun h => x) (fun h => y)` is the same as `if h : c then x else y`, but optimized for a
Boolean condition rather than a decidable proposition. Unlike the non-dependent version `cond`,
there is no special notation for `dcond`.

Just like `ite`, `dite`, and `cond`, `dcond` is declared `@[macro_inline]`, which causes
applications of `dcond` to be unfolded. As a result, `x` and `y` are not evaluated at runtime until
one of them is selected, and only the selected branch is evaluated. `dcond` is intended for
metaprogramming use, rather than for use in verified programs, so behavioral lemmas are not
provided.
-/
@[macro_inline]
protected def Bool.dcond {α : Sort u} (c : Bool) (x : Eq c true → α) (y : Eq c false → α) : α :=
  match c with
  | true  => x rfl
  | false => y rfl

/--
Boolean “or”, also known as disjunction. `or x y` can be written `x || y`.

The corresponding propositional connective is `Or : Prop → Prop → Prop`, written with the `∨`
operator.

The Boolean `or` is a `@[macro_inline]` function in order to give it short-circuiting evaluation:
if `x` is `true` then `y` is not evaluated at runtime.
-/
@[macro_inline] def Bool.or (x y : Bool) : Bool :=
  match x with
  | true  => true
  | false => y

/--
Boolean “and”, also known as conjunction. `and x y` can be written `x && y`.

The corresponding propositional connective is `And : Prop → Prop → Prop`, written with the `∧`
operator.

The Boolean `and` is a `@[macro_inline]` function in order to give it short-circuiting evaluation:
if `x` is `false` then `y` is not evaluated at runtime.
-/
@[macro_inline] def Bool.and (x y : Bool) : Bool :=
  match x with
  | false => false
  | true  => y

/--
Boolean negation, also known as Boolean complement. `not x` can be written `!x`.

This is a function that maps the value `true` to `false` and the value `false` to `true`. The
propositional connective is `Not : Prop → Prop`.
-/
@[inline] def Bool.not : Bool → Bool
  | true  => false
  | false => true

/--
The natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
-/
inductive Nat where
  /--
  Zero, the smallest natural number.

  Using `Nat.zero` explicitly should usually be avoided in favor of the literal `0`, which is the
  [simp normal form](lean-manual://section/simp-normal-forms).
  -/
  | zero : Nat
  /--
  The successor of a natural number `n`.

  Using `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal
  form](lean-manual://section/simp-normal-forms).
  -/
  | succ (n : Nat) : Nat

instance : Inhabited Nat where
  default := Nat.zero

/--
The class `OfNat α n` powers the numeric literal parser. If you write
`37 : α`, Lean will attempt to synthesize `OfNat α 37`, and will generate
the term `(OfNat.ofNat 37 : α)`.

There is a bit of infinite regress here since the desugaring apparently
still contains a literal `37` in it. The type of expressions contains a
primitive constructor for "raw natural number literals", which you can directly
access using the macro `nat_lit 37`. Raw number literals are always of type `Nat`.
So it would be more correct to say that Lean looks for an instance of
`OfNat α (nat_lit 37)`, and it generates the term `(OfNat.ofNat (nat_lit 37) : α)`.
-/
class OfNat (α : Type u) (_ : Nat) where
  /-- The `OfNat.ofNat` function is automatically inserted by the parser when
  the user writes a numeric literal like `1 : α`. Implementations of this
  typeclass can therefore customize the behavior of `n : α` based on `n` and
  `α`. -/
  ofNat : α

@[default_instance 100] /- low prio -/
instance instOfNatNat (n : Nat) : OfNat Nat n where
  ofNat := n

/-- `LE α` is the typeclass which supports the notation `x ≤ y` where `x y : α`.-/
class LE (α : Type u) where
  /-- The less-equal relation: `x ≤ y` -/
  le : α → α → Prop

/-- `LT α` is the typeclass which supports the notation `x < y` where `x y : α`.-/
class LT (α : Type u) where
  /-- The less-than relation: `x < y` -/
  lt : α → α → Prop

/-- `a ≥ b` is an abbreviation for `b ≤ a`. -/
@[reducible] def GE.ge {α : Type u} [LE α] (a b : α) : Prop := LE.le b a

/-- `a > b` is an abbreviation for `b < a`. -/
@[reducible] def GT.gt {α : Type u} [LT α] (a b : α) : Prop := LT.lt b a

/-- Abbreviation for `DecidableRel (· < · : α → α → Prop)`. -/
abbrev DecidableLT (α : Type u) [LT α] := DecidableRel (LT.lt : α → α → Prop)

/-- Abbreviation for `DecidableRel (· ≤ · : α → α → Prop)`. -/
abbrev DecidableLE (α : Type u) [LE α] := DecidableRel (LE.le : α → α → Prop)

/--
An overloaded operation to find the greater of two values of type `α`.
-/
class Max (α : Type u) where
  /-- Returns the greater of its two arguments. -/
  max : α → α → α

/--
Constructs a `Max` instance from a decidable `≤` operation.
-/
-- Marked inline so that `min x y + max x y` can be optimized to a single branch.
@[inline]
def maxOfLe [LE α] [DecidableRel (@LE.le α _)] : Max α where
  max x y := ite (LE.le x y) y x

/--
An overloaded operation to find the lesser of two values of type `α`.
-/
class Min (α : Type u) where
  /-- Returns the lesser of its two arguments. -/
  min : α → α → α

/--
Constructs a `Min` instance from a decidable `≤` operation.
-/
-- Marked inline so that `min x y + max x y` can be optimized to a single branch.
@[inline]
def minOfLe [LE α] [DecidableRel (@LE.le α _)] : Min α where
  min x y := ite (LE.le x y) x y

/--
Transitive chaining of proofs, used e.g. by `calc`.

It takes two relations `r` and `s` as "input", and produces an "output"
relation `t`, with the property that `r a b` and `s b c` implies `t a c`.
The `calc` tactic uses this so that when it sees a chain with `a ≤ b` and `b < c`
it knows that this should be a proof of `a < c` because there is an instance
`Trans (·≤·) (·<·) (·<·)`.
-/
class Trans (r : α → β → Sort u) (s : β → γ → Sort v) (t : outParam (α → γ → Sort w)) where
  /-- Compose two proofs by transitivity, generalized over the relations involved. -/
  trans : r a b → s b c → t a c

instance (r : α → γ → Sort u) : Trans Eq r r where
  trans heq h' := heq ▸ h'

instance (r : α → β → Sort u) : Trans r Eq r where
  trans h' heq := heq ▸ h'

/--
The notation typeclass for heterogeneous addition.
This enables the notation `a + b : γ` where `a : α`, `b : β`.
-/
class HAdd (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  /-- `a + b` computes the sum of `a` and `b`.
  The meaning of this notation is type-dependent. -/
  hAdd : α → β → γ

/--
The notation typeclass for heterogeneous subtraction.
This enables the notation `a - b : γ` where `a : α`, `b : β`.
-/
class HSub (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  /-- `a - b` computes the difference of `a` and `b`.
  The meaning of this notation is type-dependent.
  * For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. -/
  hSub : α → β → γ

/--
The notation typeclass for heterogeneous multiplication.
This enables the notation `a * b : γ` where `a : α`, `b : β`.
-/
class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  /-- `a * b` computes the product of `a` and `b`.
  The meaning of this notation is type-dependent. -/
  hMul : α → β → γ

/--
The notation typeclass for heterogeneous division.
This enables the notation `a / b : γ` where `a : α`, `b : β`.
-/
class HDiv (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  /-- `a / b` computes the result of dividing `a` by `b`.
  The meaning of this notation is type-dependent.
  * For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
  * For `Nat`, `a / b` rounds downwards.
  * For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
    It is implemented as `Int.ediv`, the unique function satisfying
    `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
    Other rounding conventions are available using the functions
    `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
  * For `Float`, `a / 0` follows the IEEE 754 semantics for division,
    usually resulting in `inf` or `nan`. -/
  hDiv : α → β → γ

/--
The notation typeclass for heterogeneous modulo / remainder.
This enables the notation `a % b : γ` where `a : α`, `b : β`.
-/
class HMod (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  /-- `a % b` computes the remainder upon dividing `a` by `b`.
  The meaning of this notation is type-dependent.
  * For `Nat` and `Int` it satisfies `a % b + b * (a / b) = a`,
    and `a % 0` is defined to be `a`. -/
  hMod : α → β → γ

/--
The notation typeclass for heterogeneous exponentiation.
This enables the notation `a ^ b : γ` where `a : α`, `b : β`.
-/
class HPow (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  /-- `a ^ b` computes `a` to the power of `b`.
  The meaning of this notation is type-dependent. -/
  hPow : α → β → γ

/--
The notation typeclass for heterogeneous append.
This enables the notation `a ++ b : γ` where `a : α`, `b : β`.
-/
class HAppend (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  /-- `a ++ b` is the result of concatenation of `a` and `b`, usually read "append".
  The meaning of this notation is type-dependent. -/
  hAppend : α → β → γ

/--
The typeclass behind the notation `a <|> b : γ` where `a : α`, `b : β`.
Because `b` is "lazy" in this notation, it is passed as `Unit → β` to the
implementation so it can decide when to evaluate it.
-/
class HOrElse (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  /-- `a <|> b` executes `a` and returns the result, unless it fails in which
  case it executes and returns `b`. Because `b` is not always executed, it
  is passed as a thunk so it can be forced only when needed.
  The meaning of this notation is type-dependent. -/
  hOrElse : α → (Unit → β) → γ

/--
The typeclass behind the notation `a >> b : γ` where `a : α`, `b : β`.
Because `b` is "lazy" in this notation, it is passed as `Unit → β` to the
implementation so it can decide when to evaluate it.
-/
class HAndThen (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  /-- `a >> b` executes `a`, ignores the result, and then executes `b`.
  If `a` fails then `b` is not executed. Because `b` is not always executed, it
  is passed as a thunk so it can be forced only when needed.
  The meaning of this notation is type-dependent. -/
  hAndThen : α → (Unit → β) → γ

/-- The typeclass behind the notation `a &&& b : γ` where `a : α`, `b : β`. -/
class HAnd (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  /-- `a &&& b` computes the bitwise AND of `a` and `b`.
  The meaning of this notation is type-dependent. -/
  hAnd : α → β → γ

/-- The typeclass behind the notation `a ^^^ b : γ` where `a : α`, `b : β`. -/
class HXor (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  /-- `a ^^^ b` computes the bitwise XOR of `a` and `b`.
  The meaning of this notation is type-dependent. -/
  hXor : α → β → γ

/-- The typeclass behind the notation `a ||| b : γ` where `a : α`, `b : β`. -/
class HOr (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  /-- `a ||| b` computes the bitwise OR of `a` and `b`.
  The meaning of this notation is type-dependent. -/
  hOr : α → β → γ

/-- The typeclass behind the notation `a <<< b : γ` where `a : α`, `b : β`. -/
class HShiftLeft (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  /-- `a <<< b` computes `a` shifted to the left by `b` places.
  The meaning of this notation is type-dependent.
  * On `Nat`, this is equivalent to `a * 2 ^ b`.
  * On `UInt8` and other fixed width unsigned types, this is the same but
    truncated to the bit width. -/
  hShiftLeft : α → β → γ

/-- The typeclass behind the notation `a >>> b : γ` where `a : α`, `b : β`. -/
class HShiftRight (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  /-- `a >>> b` computes `a` shifted to the right by `b` places.
  The meaning of this notation is type-dependent.
  * On `Nat` and fixed width unsigned types like `UInt8`,
    this is equivalent to `a / 2 ^ b`. -/
  hShiftRight : α → β → γ

/-- A type with a zero element. -/
class Zero (α : Type u) where
  /-- The zero element of the type. -/
  zero : α

/-- The homogeneous version of `HAdd`: `a + b : α` where `a b : α`. -/
class Add (α : Type u) where
  /-- `a + b` computes the sum of `a` and `b`. See `HAdd`. -/
  add : α → α → α

/-- The homogeneous version of `HSub`: `a - b : α` where `a b : α`. -/
class Sub (α : Type u) where
  /-- `a - b` computes the difference of `a` and `b`. See `HSub`. -/
  sub : α → α → α

/-- The homogeneous version of `HMul`: `a * b : α` where `a b : α`. -/
class Mul (α : Type u) where
  /-- `a * b` computes the product of `a` and `b`. See `HMul`. -/
  mul : α → α → α

/--
The notation typeclass for negation.
This enables the notation `-a : α` where `a : α`.
-/
class Neg (α : Type u) where
  /-- `-a` computes the negative or opposite of `a`.
  The meaning of this notation is type-dependent. -/
  neg : α → α

/-- The homogeneous version of `HDiv`: `a / b : α` where `a b : α`. -/
class Div (α : Type u) where
  /-- `a / b` computes the result of dividing `a` by `b`. See `HDiv`. -/
  div : α → α → α

/-- The homogeneous version of `HMod`: `a % b : α` where `a b : α`. -/
class Mod (α : Type u) where
  /-- `a % b` computes the remainder upon dividing `a` by `b`. See `HMod`. -/
  mod : α → α → α

/-- Notation typeclass for the `∣` operation (typed as `\|`), which represents divisibility. -/
class Dvd (α : Type _) where
  /-- Divisibility. `a ∣ b` (typed as `\|`) means that there is some `c` such that `b = a * c`. -/
  dvd : α → α → Prop

/--
The homogeneous version of `HPow`: `a ^ b : α` where `a : α`, `b : β`.
(The right argument is not the same as the left since we often want this even
in the homogeneous case.)

Types can choose to subscribe to particular defaulting behavior by providing
an instance to either `NatPow` or `HomogeneousPow`:
- `NatPow` is for types whose exponents is preferentially a `Nat`.
- `HomogeneousPow` is for types whose base and exponent are preferentially the same.
-/
class Pow (α : Type u) (β : Type v) where
  /-- `a ^ b` computes `a` to the power of `b`. See `HPow`. -/
  pow : α → β → α

/-- The homogeneous version of `Pow` where the exponent is a `Nat`.
The purpose of this class is that it provides a default `Pow` instance,
which can be used to specialize the exponent to `Nat` during elaboration.

For example, if `x ^ 2` should preferentially elaborate with `2 : Nat` then `x`'s type should
provide an instance for this class. -/
class NatPow (α : Type u) where
  /-- `a ^ n` computes `a` to the power of `n` where `n : Nat`. See `Pow`. -/
  protected pow : α → Nat → α

/-- The completely homogeneous version of `Pow` where the exponent has the same type as the base.
The purpose of this class is that it provides a default `Pow` instance,
which can be used to specialize the exponent to have the same type as the base's type during elaboration.
This is to say, a type should provide an instance for this class in case `x ^ y` should be elaborated
with both `x` and `y` having the same type.

For example, the `Float` type provides an instance of this class, which causes expressions
such as `(2.2 ^ 2.2 : Float)` to elaborate. -/
class HomogeneousPow (α : Type u) where
  /-- `a ^ b` computes `a` to the power of `b` where `a` and `b` both have the same type. -/
  protected pow : α → α → α

/-- The homogeneous version of `HAppend`: `a ++ b : α` where `a b : α`. -/
class Append (α : Type u) where
  /-- `a ++ b` is the result of concatenation of `a` and `b`. See `HAppend`. -/
  append : α → α → α

/--
The homogeneous version of `HOrElse`: `a <|> b : α` where `a b : α`.
Because `b` is "lazy" in this notation, it is passed as `Unit → α` to the
implementation so it can decide when to evaluate it.
-/
class OrElse (α : Type u) where
  /-- The implementation of `a <|> b : α`. See `HOrElse`. -/
  orElse  : α → (Unit → α) → α

/--
The homogeneous version of `HAndThen`: `a >> b : α` where `a b : α`.
Because `b` is "lazy" in this notation, it is passed as `Unit → α` to the
implementation so it can decide when to evaluate it.
-/
class AndThen (α : Type u) where
  /-- The implementation of `a >> b : α`. See `HAndThen`. -/
  andThen : α → (Unit → α) → α

/--
The homogeneous version of `HAnd`: `a &&& b : α` where `a b : α`.
(It is called `AndOp` because `And` is taken for the propositional connective.)
-/
class AndOp (α : Type u) where
  /-- The implementation of `a &&& b : α`. See `HAnd`. -/
  and : α → α → α

/-- The homogeneous version of `HXor`: `a ^^^ b : α` where `a b : α`. -/
class Xor (α : Type u) where
  /-- The implementation of `a ^^^ b : α`. See `HXor`. -/
  xor : α → α → α

/--
The homogeneous version of `HOr`: `a ||| b : α` where `a b : α`.
(It is called `OrOp` because `Or` is taken for the propositional connective.)
-/
class OrOp (α : Type u) where
  /-- The implementation of `a ||| b : α`. See `HOr`. -/
  or : α → α → α

/-- The typeclass behind the notation `~~~a : α` where `a : α`. -/
class Complement (α : Type u) where
  /-- The implementation of `~~~a : α`. -/
  complement : α → α

/-- The homogeneous version of `HShiftLeft`: `a <<< b : α` where `a b : α`. -/
class ShiftLeft (α : Type u) where
  /-- The implementation of `a <<< b : α`. See `HShiftLeft`. -/
  shiftLeft : α → α → α

/-- The homogeneous version of `HShiftRight`: `a >>> b : α` where `a b : α`. -/
class ShiftRight (α : Type u) where
  /-- The implementation of `a >>> b : α`. See `HShiftRight`. -/
  shiftRight : α → α → α

@[default_instance]
instance instHAdd [Add α] : HAdd α α α where
  hAdd a b := Add.add a b

@[default_instance]
instance instHSub [Sub α] : HSub α α α where
  hSub a b := Sub.sub a b

@[default_instance]
instance instHMul [Mul α] : HMul α α α where
  hMul a b := Mul.mul a b

@[default_instance]
instance instHDiv [Div α] : HDiv α α α where
  hDiv a b := Div.div a b

@[default_instance]
instance instHMod [Mod α] : HMod α α α where
  hMod a b := Mod.mod a b

@[default_instance]
instance instHPow [Pow α β] : HPow α β α where
  hPow a b := Pow.pow a b

@[default_instance]
instance instPowNat [NatPow α] : Pow α Nat where
  pow a n := NatPow.pow a n

@[default_instance]
instance [HomogeneousPow α] : Pow α α where
  pow a b := HomogeneousPow.pow a b

@[default_instance]
instance [Append α] : HAppend α α α where
  hAppend a b := Append.append a b

@[default_instance]
instance [OrElse α] : HOrElse α α α where
  hOrElse a b := OrElse.orElse a b

@[default_instance]
instance [AndThen α] : HAndThen α α α where
  hAndThen a b := AndThen.andThen a b

@[default_instance]
instance [AndOp α] : HAnd α α α where
  hAnd a b := AndOp.and a b

@[default_instance]
instance [Xor α] : HXor α α α where
  hXor a b := Xor.xor a b

@[default_instance]
instance [OrOp α] : HOr α α α where
  hOr a b := OrOp.or a b

@[default_instance]
instance [ShiftLeft α] : HShiftLeft α α α where
  hShiftLeft a b := ShiftLeft.shiftLeft a b

@[default_instance]
instance [ShiftRight α] : HShiftRight α α α where
  hShiftRight a b := ShiftRight.shiftRight a b

/--
The typeclass behind the notation `a ∈ s : Prop` where `a : α`, `s : γ`.
Because `α` is an `outParam`, the "container type" `γ` determines the type
of the elements of the container.
-/
class Membership (α : outParam (Type u)) (γ : Type v) where
  /-- The membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. -/
  mem : γ → α → Prop

/--
Addition of natural numbers, typically used via the `+` operator.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the
arbitrary-precision arithmetic library. The definition provided here is the logical model.
-/
@[extern "lean_nat_add"]
protected def Nat.add : (@& Nat) → (@& Nat) → Nat
  | a, Nat.zero   => a
  | a, Nat.succ b => Nat.succ (Nat.add a b)

instance instAddNat : Add Nat where
  add := Nat.add

/--
Multiplication of natural numbers, usually accessed via the `*` operator.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the
arbitrary-precision arithmetic library. The definition provided here is the logical model.
-/
@[extern "lean_nat_mul"]
protected def Nat.mul : (@& Nat) → (@& Nat) → Nat
  | _, 0          => 0
  | a, Nat.succ b => Nat.add (Nat.mul a b) a

instance instMulNat : Mul Nat where
  mul := Nat.mul

/--
The power operation on natural numbers, usually accessed via the `^` operator.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the
arbitrary-precision arithmetic library. The definition provided here is the logical model.
-/
@[extern "lean_nat_pow"]
protected def Nat.pow (m : @& Nat) : (@& Nat) → Nat
  | 0      => 1
  | succ n => Nat.mul (Nat.pow m n) m

instance instNatPowNat : NatPow Nat := ⟨Nat.pow⟩

/--
Boolean equality of natural numbers, usually accessed via the `==` operator.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the
arbitrary-precision arithmetic library. The definition provided here is the logical model.
-/
@[extern "lean_nat_dec_eq"]
def Nat.beq : (@& Nat) → (@& Nat) → Bool
  | zero,   zero   => true
  | zero,   succ _ => false
  | succ _, zero   => false
  | succ n, succ m => beq n m

theorem Nat.ne_of_beq_eq_false : {n m : Nat} → Eq (beq n m) false → Not (Eq n m)
  | zero,   zero,   h₁, _  => Bool.noConfusion h₁
  | zero,   succ _, _,  h₂ => Nat.noConfusion h₂
  | succ _, zero,   _,  h₂ => Nat.noConfusion h₂
  | succ n, succ m, h₁, h₂ =>
    have : Eq (beq n m) false := h₁
    Nat.noConfusion h₂ (fun h₂ => absurd h₂ (ne_of_beq_eq_false this))

/--
A decision procedure for equality of natural numbers, usually accessed via the `DecidableEq Nat`
instance.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the
arbitrary-precision arithmetic library. The definition provided here is the logical model.

Examples:
 * `Nat.decEq 5 5 = isTrue rfl`
 * `(if 3 = 4 then "yes" else "no") = "no"`
 * `show 12 = 12 by decide`
-/
@[reducible, extern "lean_nat_dec_eq"]
protected def Nat.decEq (n m : @& Nat) : Decidable (Eq n m) :=
  match h:beq n m with
  | true  => isTrue (eq_of_beq_eq_true h)
  | false => isFalse (ne_of_beq_eq_false h)

@[inline] instance : DecidableEq Nat := Nat.decEq

/--
The Boolean less-than-or-equal-to comparison on natural numbers.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the
arbitrary-precision arithmetic library. The definition provided here is the logical model.

Examples:
 * `Nat.ble 2 5 = true`
 * `Nat.ble 5 2 = false`
 * `Nat.ble 5 5 = true`
-/
@[extern "lean_nat_dec_le"]
def Nat.ble : @& Nat → @& Nat → Bool
  | zero,   zero   => true
  | zero,   succ _ => true
  | succ _, zero   => false
  | succ n, succ m => ble n m

/--
Non-strict, or weak, inequality of natural numbers, usually accessed via the `≤` operator.
-/
protected inductive Nat.le (n : Nat) : Nat → Prop
  /-- Non-strict inequality is reflexive: `n ≤ n` -/
  | refl     : Nat.le n n
  /-- If `n ≤ m`, then `n ≤ m + 1`. -/
  | step {m} : Nat.le n m → Nat.le n (succ m)

instance instLENat : LE Nat where
  le := Nat.le

/--
Strict inequality of natural numbers, usually accessed via the `<` operator.

It is defined as `n < m = n + 1 ≤ m`.
-/
protected def Nat.lt (n m : Nat) : Prop :=
  Nat.le (succ n) m

instance instLTNat : LT Nat where
  lt := Nat.lt

theorem Nat.not_succ_le_zero : ∀ (n : Nat), LE.le (succ n) 0 → False
  | 0      => nofun
  | succ _ => nofun

theorem Nat.not_lt_zero (n : Nat) : Not (LT.lt n 0) :=
  not_succ_le_zero n

theorem Nat.zero_le : (n : Nat) → LE.le 0 n
  | zero   => Nat.le.refl
  | succ n => Nat.le.step (zero_le n)

theorem Nat.succ_le_succ : LE.le n m → LE.le (succ n) (succ m)
  | Nat.le.refl   => Nat.le.refl
  | Nat.le.step h => Nat.le.step (succ_le_succ h)

theorem Nat.zero_lt_succ (n : Nat) : LT.lt 0 (succ n) :=
  succ_le_succ (zero_le n)

theorem Nat.le_step (h : LE.le n m) : LE.le n (succ m) :=
  Nat.le.step h

protected theorem Nat.le_trans {n m k : Nat} : LE.le n m → LE.le m k → LE.le n k
  | h,  Nat.le.refl    => h
  | h₁, Nat.le.step h₂ => Nat.le.step (Nat.le_trans h₁ h₂)

protected theorem Nat.lt_trans {n m k : Nat} (h₁ : LT.lt n m) : LT.lt m k → LT.lt n k :=
  Nat.le_trans (le_step h₁)

theorem Nat.le_succ (n : Nat) : LE.le n (succ n) :=
  Nat.le.step Nat.le.refl

theorem Nat.le_succ_of_le {n m : Nat} (h : LE.le n m) : LE.le n (succ m) :=
  Nat.le_trans h (le_succ m)

protected theorem Nat.le_refl (n : Nat) : LE.le n n :=
  Nat.le.refl

theorem Nat.succ_pos (n : Nat) : LT.lt 0 (succ n) :=
  zero_lt_succ n

/--
The predecessor of a natural number is one less than it. The precedessor of `0` is defined to be
`0`.

This definition is overridden in the compiler with an efficient implementation. This definition is
the logical model.
-/
@[extern "lean_nat_pred"]
def Nat.pred : (@& Nat) → Nat
  | 0      => 0
  | succ a => a

theorem Nat.pred_le_pred : {n m : Nat} → LE.le n m → LE.le (pred n) (pred m)
  | _,           _, Nat.le.refl   => Nat.le.refl
  | 0,      succ _, Nat.le.step h => h
  | succ _, succ _, Nat.le.step h => Nat.le_trans (le_succ _) h

theorem Nat.le_of_succ_le_succ {n m : Nat} : LE.le (succ n) (succ m) → LE.le n m :=
  pred_le_pred

theorem Nat.le_of_lt_succ {m n : Nat} : LT.lt m (succ n) → LE.le m n :=
  le_of_succ_le_succ

protected theorem Nat.lt_or_ge (n m : Nat) : Or (LT.lt n m) (GE.ge n m) :=
  match m with
  | zero   => Or.inr (zero_le n)
  | succ m =>
    match Nat.lt_or_ge n m with
    | Or.inl h => Or.inl (le_succ_of_le h)
    | Or.inr h =>
      match Nat.eq_or_lt_of_le h with
      | Or.inl h1 => Or.inl (h1 ▸ Nat.le_refl _)
      | Or.inr h1 => Or.inr h1

theorem Nat.not_succ_le_self : (n : Nat) → Not (LE.le (succ n) n)
  | 0      => not_succ_le_zero _
  | succ n => fun h => absurd (le_of_succ_le_succ h) (not_succ_le_self n)

protected theorem Nat.lt_irrefl (n : Nat) : Not (LT.lt n n) :=
  Nat.not_succ_le_self n

protected theorem Nat.lt_of_le_of_lt {n m k : Nat} (h₁ : LE.le n m) (h₂ : LT.lt m k) : LT.lt n k :=
  Nat.le_trans (Nat.succ_le_succ h₁) h₂

protected theorem Nat.le_antisymm {n m : Nat} (h₁ : LE.le n m) (h₂ : LE.le m n) : Eq n m :=
  match h₁ with
  | Nat.le.refl   => rfl
  | Nat.le.step h => absurd (Nat.lt_of_le_of_lt h h₂) (Nat.lt_irrefl n)

protected theorem Nat.lt_of_le_of_ne {n m : Nat} (h₁ : LE.le n m) (h₂ : Not (Eq n m)) : LT.lt n m :=
  match Nat.lt_or_ge n m with
  | Or.inl h₃ => h₃
  | Or.inr h₃ => absurd (Nat.le_antisymm h₁ h₃) h₂

theorem Nat.le_of_ble_eq_true (h : Eq (Nat.ble n m) true) : LE.le n m :=
  match n, m with
  | 0,      _      => Nat.zero_le _
  | succ _, succ _ => Nat.succ_le_succ (le_of_ble_eq_true h)

theorem Nat.ble_self_eq_true : (n : Nat) → Eq (Nat.ble n n) true
  | 0      => rfl
  | succ n => ble_self_eq_true n

theorem Nat.ble_succ_eq_true : {n m : Nat} → Eq (Nat.ble n m) true → Eq (Nat.ble n (succ m)) true
  | 0,      _,      _ => rfl
  | succ n, succ _, h => ble_succ_eq_true (n := n) h

theorem Nat.ble_eq_true_of_le (h : LE.le n m) : Eq (Nat.ble n m) true :=
  match h with
  | Nat.le.refl   => Nat.ble_self_eq_true n
  | Nat.le.step h => Nat.ble_succ_eq_true (ble_eq_true_of_le h)

theorem Nat.not_le_of_not_ble_eq_true (h : Not (Eq (Nat.ble n m) true)) : Not (LE.le n m) :=
  fun h' => absurd (Nat.ble_eq_true_of_le h') h

/--
A decision procedure for non-strict inequality of natural numbers, usually accessed via the
`DecidableLE Nat` instance.

Examples:
 * `(if 3 ≤ 4 then "yes" else "no") = "yes"`
 * `(if 6 ≤ 4 then "yes" else "no") = "no"`
 * `show 12 ≤ 12 by decide`
 * `show 5 ≤ 12 by decide`
-/
@[extern "lean_nat_dec_le"]
instance Nat.decLe (n m : @& Nat) : Decidable (LE.le n m) :=
  dite (Eq (Nat.ble n m) true) (fun h => isTrue (Nat.le_of_ble_eq_true h)) (fun h => isFalse (Nat.not_le_of_not_ble_eq_true h))

/--
A decision procedure for strict inequality of natural numbers, usually accessed via the
`DecidableLT Nat` instance.

Examples:
 * `(if 3 < 4 then "yes" else "no") = "yes"`
 * `(if 4 < 4 then "yes" else "no") = "no"`
 * `(if 6 < 4 then "yes" else "no") = "no"`
 * `show 5 < 12 by decide`
-/
@[extern "lean_nat_dec_lt"]
instance Nat.decLt (n m : @& Nat) : Decidable (LT.lt n m) :=
  decLe (succ n) m

instance : Min Nat := minOfLe

/--
Subtraction of natural numbers, truncated at `0`. Usually used via the `-` operator.

If a result would be less than zero, then the result is zero.

This definition is overridden in both the kernel and the compiler to efficiently evaluate using the
arbitrary-precision arithmetic library. The definition provided here is the logical model.

Examples:
* `5 - 3 = 2`
* `8 - 2 = 6`
* `8 - 8 = 0`
* `8 - 20 = 0`
-/
@[extern "lean_nat_sub"]
protected def Nat.sub : (@& Nat) → (@& Nat) → Nat
  | a, 0      => a
  | a, succ b => pred (Nat.sub a b)

instance instSubNat : Sub Nat where
  sub := Nat.sub

/--
Gets the word size of the curent platform. The word size may be 64 or 32 bits.

This function is opaque because there is no guarantee at compile time that the target will have the
same word size as the host. It also helps avoid having type checking be architecture-dependent.

Lean only works on 64 and 32 bit systems. This fact is visible in the return type.
-/
@[extern "lean_system_platform_nbits"] opaque System.Platform.getNumBits : Unit → Subtype fun (n : Nat) => Or (Eq n 32) (Eq n 64) :=
  fun _ => ⟨64, Or.inr rfl⟩

/--
The word size of the current platform, which may be 64 or 32 bits.
-/
def System.Platform.numBits : Nat :=
  (getNumBits ()).val

/--
The word size of the current platform may be 64 or 32 bits.
-/
theorem System.Platform.numBits_eq : Or (Eq numBits 32) (Eq numBits 64) :=
  (getNumBits ()).property

/--
Natural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
-/
@[pp_using_anonymous_constructor]
structure Fin (n : Nat) where
  /-- Creates a `Fin n` from `i : Nat` and a proof that `i < n`. -/
  mk ::
  /--
  The number that is strictly less than `n`.

  `Fin.val` is a coercion, so any `Fin n` can be used in a position where a `Nat` is expected.
  -/
  val  : Nat
  /--
  The number `val` is strictly less than the bound `n`.
  -/
  isLt : LT.lt val n

theorem Fin.val_eq_of_eq {n} {i j : Fin n} (h : Eq i j) : Eq i.val j.val :=
  h ▸ rfl

instance (n : Nat) : DecidableEq (Fin n) :=
  fun i j =>
    match decEq i.val j.val with
    | isTrue h  => isTrue (Fin.eq_of_val_eq h)
    | isFalse h => isFalse (fun h' => absurd (Fin.val_eq_of_eq h') h)

instance {n} : LT (Fin n) where
  lt a b := LT.lt a.val b.val

instance {n} : LE (Fin n) where
  le a b := LE.le a.val b.val

instance Fin.decLt {n} (a b : Fin n) : Decidable (LT.lt a b) := Nat.decLt ..

instance Fin.decLe {n} (a b : Fin n) : Decidable (LE.le a b) := Nat.decLe ..

/--
A bitvector of the specified width.

This is represented as the underlying `Nat` number in both the runtime
and the kernel, inheriting all the special support for `Nat`.
-/
structure BitVec (w : Nat) where
  /-- Construct a `BitVec w` from a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  ofFin ::
  /-- Interpret a bitvector as a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  toFin : Fin (hPow 2 w)

/--
Bitvectors have decidable equality.

This should be used via the instance `DecidableEq (BitVec n)`.
-/
-- We manually derive the `DecidableEq` instances for `BitVec` because
-- we want to have builtin support for bit-vector literals, and we
-- need a name for this function to implement `canUnfoldAtMatcher` at `WHNF.lean`.
def BitVec.decEq (x y : BitVec n) : Decidable (Eq x y) :=
  match x, y with
  | ⟨n⟩, ⟨m⟩ =>
    dite (Eq n m)
      (fun h => isTrue (h ▸ rfl))
      (fun h => isFalse (fun h' => BitVec.noConfusion h' (fun h' => absurd h' h)))

instance : DecidableEq (BitVec n) := BitVec.decEq

/-- The `BitVec` with value `i`, given a proof that `i < 2^n`. -/
@[match_pattern]
protected def BitVec.ofNatLT {n : Nat} (i : Nat) (p : LT.lt i (hPow 2 n)) : BitVec n where
  toFin := ⟨i, p⟩

/--
Return the underlying `Nat` that represents a bitvector.

This is O(1) because `BitVec` is a (zero-cost) wrapper around a `Nat`.
-/
protected def BitVec.toNat (x : BitVec n) : Nat := x.toFin.val

instance : LT (BitVec n) where lt := (LT.lt ·.toNat ·.toNat)

instance (x y : BitVec n) : Decidable (LT.lt x y) :=
  inferInstanceAs (Decidable (LT.lt x.toNat y.toNat))

instance : LE (BitVec n) where le := (LE.le ·.toNat ·.toNat)

instance (x y : BitVec n) : Decidable (LE.le x y) :=
  inferInstanceAs (Decidable (LE.le x.toNat y.toNat))

/-- The number of distinct values representable by `UInt8`, that is, `2^8 = 256`. -/
abbrev UInt8.size : Nat := 256

/--
Unsigned 8-bit integers.

This type has special support in the compiler so it can be represented by an unboxed 8-bit value
rather than wrapping a `BitVec 8`.
-/
structure UInt8 where
  /--
  Creates a `UInt8` from a `BitVec 8`. This function is overridden with a native implementation.
  -/
  ofBitVec ::
  /--
  Unpacks a `UInt8` into a `BitVec 8`. This function is overridden with a native implementation.
  -/
  toBitVec : BitVec 8

/--
Converts a natural number to an 8-bit unsigned integer. Requires a proof that the number is small
enough to be representable without overflow; it must be smaller than `2^8`.

This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint8_of_nat"]
def UInt8.ofNatLT (n : @& Nat) (h : LT.lt n UInt8.size) : UInt8 where
  toBitVec := BitVec.ofNatLT n h

/--
Decides whether two 8-bit unsigned integers are equal. Usually accessed via the `DecidableEq UInt8`
instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `UInt8.decEq 123 123 = .isTrue rfl`
 * `(if (6 : UInt8) = 7 then "yes" else "no") = "no"`
 * `show (7 : UInt8) = 7 by decide`
-/
@[extern "lean_uint8_dec_eq"]
def UInt8.decEq (a b : UInt8) : Decidable (Eq a b) :=
  match a, b with
  | ⟨n⟩, ⟨m⟩ =>
    dite (Eq n m)
      (fun h => isTrue (h ▸ rfl))
      (fun h => isFalse (fun h' => UInt8.noConfusion h' (fun h' => absurd h' h)))

instance : DecidableEq UInt8 := UInt8.decEq

instance : Inhabited UInt8 where
  default := UInt8.ofNatLT 0 (of_decide_eq_true rfl)

/-- The number of distinct values representable by `UInt16`, that is, `2^16 = 65536`. -/
abbrev UInt16.size : Nat := 65536

/--
Unsigned 16-bit integers.

This type has special support in the compiler so it can be represented by an unboxed 16-bit value
rather than wrapping a `BitVec 16`.
-/
structure UInt16 where
  /--
  Creates a `UInt16` from a `BitVec 16`. This function is overridden with a native implementation.
  -/
  ofBitVec ::
  /--
  Unpacks a `UInt16` into a `BitVec 16`. This function is overridden with a native implementation.
  -/
  toBitVec : BitVec 16

/--
Converts a natural number to a 16-bit unsigned integer. Requires a proof that the number is small
enough to be representable without overflow; it must be smaller than `2^16`.

This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint16_of_nat"]
def UInt16.ofNatLT (n : @& Nat) (h : LT.lt n UInt16.size) : UInt16 where
  toBitVec := BitVec.ofNatLT n h

/--
Decides whether two 16-bit unsigned integers are equal. Usually accessed via the
`DecidableEq UInt16` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `UInt16.decEq 123 123 = .isTrue rfl`
 * `(if (6 : UInt16) = 7 then "yes" else "no") = "no"`
 * `show (7 : UInt16) = 7 by decide`
-/
@[extern "lean_uint16_dec_eq"]
def UInt16.decEq (a b : UInt16) : Decidable (Eq a b) :=
  match a, b with
  | ⟨n⟩, ⟨m⟩ =>
    dite (Eq n m)
      (fun h => isTrue (h ▸ rfl))
      (fun h => isFalse (fun h' => UInt16.noConfusion h' (fun h' => absurd h' h)))

instance : DecidableEq UInt16 := UInt16.decEq

instance : Inhabited UInt16 where
  default := UInt16.ofNatLT 0 (of_decide_eq_true rfl)

/-- The number of distinct values representable by `UInt32`, that is, `2^32 = 4294967296`. -/
abbrev UInt32.size : Nat := 4294967296

/--
Unsigned 32-bit integers.

This type has special support in the compiler so it can be represented by an unboxed 32-bit value
rather than wrapping a `BitVec 32`.
-/
structure UInt32 where
  /--
  Creates a `UInt32` from a `BitVec 32`. This function is overridden with a native implementation.
  -/
  ofBitVec ::
  /--
  Unpacks a `UInt32` into a `BitVec 32`. This function is overridden with a native implementation.
  -/
  toBitVec : BitVec 32

/--
Converts a natural number to a 32-bit unsigned integer. Requires a proof that the number is small
enough to be representable without overflow; it must be smaller than `2^32`.

This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint32_of_nat"]
def UInt32.ofNatLT (n : @& Nat) (h : LT.lt n UInt32.size) : UInt32 where
  toBitVec := BitVec.ofNatLT n h

/--
Converts a 32-bit unsigned integer to an arbitrary-precision natural number.

This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint32_to_nat"]
def UInt32.toNat (n : UInt32) : Nat := n.toBitVec.toNat

/--
Decides whether two 32-bit unsigned integers are equal. Usually accessed via the
`DecidableEq UInt32` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `UInt32.decEq 123 123 = .isTrue rfl`
 * `(if (6 : UInt32) = 7 then "yes" else "no") = "no"`
 * `show (7 : UInt32) = 7 by decide`
-/
@[extern "lean_uint32_dec_eq"]
def UInt32.decEq (a b : UInt32) : Decidable (Eq a b) :=
  match a, b with
  | ⟨n⟩, ⟨m⟩ =>
    dite (Eq n m) (fun h => isTrue (h ▸ rfl)) (fun h => isFalse (fun h' => UInt32.noConfusion h' (fun h' => absurd h' h)))

instance : DecidableEq UInt32 := UInt32.decEq

instance : Inhabited UInt32 where
  default := UInt32.ofNatLT 0 (of_decide_eq_true rfl)

instance : LT UInt32 where
  lt a b := LT.lt a.toBitVec b.toBitVec

instance : LE UInt32 where
  le a b := LE.le a.toBitVec b.toBitVec

/--
Decides whether one 8-bit unsigned integer is strictly less than another. Usually accessed via the
`DecidableLT UInt32` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `(if (6 : UInt32) < 7 then "yes" else "no") = "yes"`
 * `(if (5 : UInt32) < 5 then "yes" else "no") = "no"`
 * `show ¬((7 : UInt32) < 7) by decide`
-/
@[extern "lean_uint32_dec_lt"]
def UInt32.decLt (a b : UInt32) : Decidable (LT.lt a b) :=
  inferInstanceAs (Decidable (LT.lt a.toBitVec b.toBitVec))

/--
Decides whether one 32-bit signed integer is less than or equal to another. Usually accessed via the
`DecidableLE UInt32` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `(if (15 : UInt32) ≤ 15 then "yes" else "no") = "yes"`
 * `(if (15 : UInt32) ≤ 5 then "yes" else "no") = "no"`
 * `(if (5 : UInt32) ≤ 15 then "yes" else "no") = "yes"`
 * `show (7 : UInt32) ≤ 7 by decide`
-/
@[extern "lean_uint32_dec_le"]
def UInt32.decLe (a b : UInt32) : Decidable (LE.le a b) :=
  inferInstanceAs (Decidable (LE.le a.toBitVec b.toBitVec))

instance (a b : UInt32) : Decidable (LT.lt a b) := UInt32.decLt a b

instance (a b : UInt32) : Decidable (LE.le a b) := UInt32.decLe a b

instance : Max UInt32 := maxOfLe

instance : Min UInt32 := minOfLe

/-- The number of distinct values representable by `UInt64`, that is, `2^64 = 18446744073709551616`. -/
abbrev UInt64.size : Nat := 18446744073709551616

/--
Unsigned 64-bit integers.

This type has special support in the compiler so it can be represented by an unboxed 64-bit value
rather than wrapping a `BitVec 64`.
-/
structure UInt64 where
  /--
  Creates a `UInt64` from a `BitVec 64`. This function is overridden with a native implementation.
  -/
  ofBitVec ::
  /--
  Unpacks a `UInt64` into a `BitVec 64`. This function is overridden with a native implementation.
  -/
  toBitVec : BitVec 64

/--
Converts a natural number to a 64-bit unsigned integer. Requires a proof that the number is small
enough to be representable without overflow; it must be smaller than `2^64`.

This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_uint64_of_nat"]
def UInt64.ofNatLT (n : @& Nat) (h : LT.lt n UInt64.size) : UInt64 where
  toBitVec := BitVec.ofNatLT n h

/--
Decides whether two 64-bit unsigned integers are equal. Usually accessed via the
`DecidableEq UInt64` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `UInt64.decEq 123 123 = .isTrue rfl`
 * `(if (6 : UInt64) = 7 then "yes" else "no") = "no"`
 * `show (7 : UInt64) = 7 by decide`
-/
@[extern "lean_uint64_dec_eq"]
def UInt64.decEq (a b : UInt64) : Decidable (Eq a b) :=
  match a, b with
  | ⟨n⟩, ⟨m⟩ =>
    dite (Eq n m)
      (fun h => isTrue (h ▸ rfl))
      (fun h => isFalse (fun h' => UInt64.noConfusion h' (fun h' => absurd h' h)))

instance : DecidableEq UInt64 := UInt64.decEq

instance : Inhabited UInt64 where
  default := UInt64.ofNatLT 0 (of_decide_eq_true rfl)

/-- The number of distinct values representable by `USize`, that is, `2^System.Platform.numBits`. -/
abbrev USize.size : Nat := (hPow 2 System.Platform.numBits)

theorem USize.size_eq : Or (Eq USize.size 4294967296) (Eq USize.size 18446744073709551616) :=
  show Or (Eq (hPow 2 System.Platform.numBits) 4294967296) (Eq (hPow 2 System.Platform.numBits) 18446744073709551616) from
  match System.Platform.numBits, System.Platform.numBits_eq with
  | _, Or.inl rfl => Or.inl (of_decide_eq_true rfl)
  | _, Or.inr rfl => Or.inr (of_decide_eq_true rfl)

theorem USize.size_pos : LT.lt 0 USize.size :=
  match USize.size, USize.size_eq with
  | _, Or.inl rfl => of_decide_eq_true rfl
  | _, Or.inr rfl => of_decide_eq_true rfl

/--
Unsigned integers that are the size of a word on the platform's architecture.

On a 32-bit architecture, `USize` is equivalent to `UInt32`. On a 64-bit machine, it is equivalent
to `UInt64`.
-/
structure USize where
  /--
  Creates a `USize` from a `BitVec System.Platform.numBits`. This function is overridden with a
  native implementation.
  -/
  ofBitVec ::
  /--
  Unpacks a `USize` into a `BitVec System.Platform.numBits`. This function is overridden with a native
  implementation.
  -/
  toBitVec : BitVec System.Platform.numBits

/--
Converts a natural number to a `USize`. Requires a proof that the number is small enough to be
representable without overflow.

This function is overridden at runtime with an efficient implementation.
-/
@[extern "lean_usize_of_nat"]
def USize.ofNatLT (n : @& Nat) (h : LT.lt n USize.size) : USize where
  toBitVec := BitVec.ofNatLT n h

/--
Decides whether two word-sized unsigned integers are equal. Usually accessed via the
`DecidableEq USize` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `USize.decEq 123 123 = .isTrue rfl`
 * `(if (6 : USize) = 7 then "yes" else "no") = "no"`
 * `show (7 : USize) = 7 by decide`
-/
@[extern "lean_usize_dec_eq"]
def USize.decEq (a b : USize) : Decidable (Eq a b) :=
  match a, b with
  | ⟨n⟩, ⟨m⟩ =>
    dite (Eq n m)
      (fun h => isTrue (h ▸ rfl))
      (fun h => isFalse (fun h' => USize.noConfusion h' (fun h' => absurd h' h)))

instance : DecidableEq USize := USize.decEq

instance : Inhabited USize where
  default := USize.ofNatLT 0 USize.size_pos

/--
A `Nat` denotes a valid Unicode code point if it is less than `0x110000` and it is also not a
surrogate code point (the range `0xd800` to `0xdfff` inclusive).
-/
abbrev Nat.isValidChar (n : Nat) : Prop :=
  Or (LT.lt n 0xd800) (And (LT.lt 0xdfff n) (LT.lt n 0x110000))

/--
A `UInt32` denotes a valid Unicode code point if it is less than `0x110000` and it is also not a
surrogate code point (the range `0xd800` to `0xdfff` inclusive).
-/
abbrev UInt32.isValidChar (n : UInt32) : Prop :=
  n.toNat.isValidChar

/--
Characters are Unicode [scalar values](http://www.unicode.org/glossary/#unicode_scalar_value).
-/
structure Char where
  /-- The underlying Unicode scalar value as a `UInt32`. -/
  val   : UInt32
  /-- The value must be a legal scalar value. -/
  valid : val.isValidChar

/--
Pack a `Nat` encoding a valid codepoint into a `Char`.
This function is overridden with a native implementation.
-/
@[extern "lean_uint32_of_nat"]
def Char.ofNatAux (n : @& Nat) (h : n.isValidChar) : Char :=
  { val := ⟨BitVec.ofNatLT n (isValidChar_UInt32 h)⟩, valid := h }

/--
Converts a `Nat` into a `Char`. If the `Nat` does not encode a valid Unicode scalar value, `'\0'` is
returned instead.
-/
@[noinline, match_pattern]
def Char.ofNat (n : Nat) : Char :=
  dite (n.isValidChar)
    (fun h => Char.ofNatAux n h)
    (fun _ => { val := ⟨BitVec.ofNatLT 0 (of_decide_eq_true rfl)⟩, valid := Or.inl (of_decide_eq_true rfl) })

theorem Char.val_eq_of_eq : ∀ {c d : Char}, Eq c d → Eq c.val d.val
  | _, _, rfl => rfl

theorem Char.ne_of_val_ne {c d : Char} (h : Not (Eq c.val d.val)) : Not (Eq c d) :=
  fun h' => absurd (val_eq_of_eq h') h

theorem Char.val_ne_of_ne {c d : Char} (h : Not (Eq c d)) : Not (Eq c.val d.val) :=
  fun h' => absurd (eq_of_val_eq h') h

instance : DecidableEq Char :=
  fun c d =>
    match decEq c.val d.val with
    | isTrue h  => isTrue (Char.eq_of_val_eq h)
    | isFalse h => isFalse (Char.ne_of_val_ne h)

/-- Returns the number of bytes required to encode this `Char` in UTF-8. -/
def Char.utf8Size (c : Char) : Nat :=
  let v := c.val
  ite (LE.le v (UInt32.ofNatLT 0x7F (of_decide_eq_true rfl))) 1
    (ite (LE.le v (UInt32.ofNatLT 0x7FF (of_decide_eq_true rfl))) 2
      (ite (LE.le v (UInt32.ofNatLT 0xFFFF (of_decide_eq_true rfl))) 3 4))

/--
Optional values, which are either `some` around a value from the underlying type or `none`.

`Option` can represent nullable types or computations that might fail. In the codomain of a function
type, it can also represent partiality.
-/
inductive Option (α : Type u) where
  /-- No value. -/
  | none : Option α
  /-- Some value of type `α`. -/
  | some (val : α) : Option α

instance {α} : Inhabited (Option α) where
  default := none

/--
Gets an optional value, returning a given default on `none`.

This function is `@[macro_inline]`, so `dflt` will not be evaluated unless `opt` turns out to be
`none`.

Examples:
 * `(some "hello").getD "goodbye" = "hello"`
 * `none.getD "goodbye" = "hello"`
-/
@[macro_inline] def Option.getD (opt : Option α) (dflt : α) : α :=
  match opt with
  | some x => x
  | none => dflt

/--
Apply a function to an optional value, if present.

From the perspective of `Option` as a container with at most one value, this is analogous to
`List.map`. It can also be accessed via the `Functor Option` instance.

Examples:
 * `(none : Option Nat).map (· + 1) = none`
 * `(some 3).map (· + 1) = some 4`
-/
@[inline] protected def Option.map (f : α → β) : Option α → Option β
  | some x => some (f x)
  | none   => none

/--
Linked lists: ordered lists, in which each element has a reference to the next element.

Most operations on linked lists take time proportional to the length of the list, because each
element must be traversed to find the next element.

`List α` is isomorphic to `Array α`, but they are useful for different things:
* `List α` is easier for reasoning, and `Array α` is modeled as a wrapper around `List α`.
* `List α` works well as a persistent data structure, when many copies of the tail are shared. When
  the value is not shared, `Array α` will have better performance because it can do destructive
  updates.
-/
inductive List (α : Type u) where
  /-- The empty list, usually written `[]`. -/
  | nil : List α
  /--
  The list whose first element is `head`, where `tail` is the rest of the list.
  Usually written `head :: tail`.
  -/
  | cons (head : α) (tail : List α) : List α

instance {α} : Inhabited (List α) where
  default := List.nil

/-- Implements decidable equality for `List α`, assuming `α` has decidable equality. -/
protected def List.hasDecEq {α : Type u} [DecidableEq α] : (a b : List α) → Decidable (Eq a b)
  | nil,       nil       => isTrue rfl
  | cons _ _, nil        => isFalse (fun h => List.noConfusion h)
  | nil,       cons _ _  => isFalse (fun h => List.noConfusion h)
  | cons a as, cons b bs =>
    match decEq a b with
    | isTrue hab  =>
      match List.hasDecEq as bs with
      | isTrue habs  => isTrue (hab ▸ habs ▸ rfl)
      | isFalse nabs => isFalse (fun h => List.noConfusion h (fun _ habs => absurd habs nabs))
    | isFalse nab => isFalse (fun h => List.noConfusion h (fun hab _ => absurd hab nab))

instance {α : Type u} [DecidableEq α] : DecidableEq (List α) := List.hasDecEq

/--
The length of a list.

This function is overridden in the compiler to `lengthTR`, which uses constant stack space.

Examples:
 * `([] : List String).length = 0`
 * `["green", "brown"].length = 2`
-/
def List.length : List α → Nat
  | nil       => 0
  | cons _ as => HAdd.hAdd (length as) 1

/-- Auxiliary function for `List.lengthTR`. -/
def List.lengthTRAux : List α → Nat → Nat
  | nil,       n => n
  | cons _ as, n => lengthTRAux as (Nat.succ n)

/--
The length of a list.

This is a tail-recursive version of `List.length`, used to implement `List.length` without running
out of stack space.

Examples:
 * `([] : List String).lengthTR = 0`
 * `["green", "brown"].lengthTR = 2`
-/
def List.lengthTR (as : List α) : Nat :=
  lengthTRAux as 0

/--
Returns the element at the provided index, counting from `0`.

In other words, for `i : Fin as.length`, `as.get i` returns the `i`'th element of the list `as`.
Because the index is a `Fin` bounded by the list's length, the index will never be out of bounds.

Examples:
 * `["spring", "summer", "fall", "winter"].get (2 : Fin 4) = "fall"`
 * `["spring", "summer", "fall", "winter"].get (0 : Fin 4) = "spring"`
-/
def List.get {α : Type u} : (as : List α) → Fin as.length → α
  | cons a _,  ⟨0, _⟩ => a
  | cons _ as, ⟨Nat.succ i, h⟩ => get as ⟨i, Nat.le_of_succ_le_succ h⟩

/--
Replaces the value at (zero-based) index `n` in `l` with `a`. If the index is out of bounds, then
the list is returned unmodified.

Examples:
* `["water", "coffee", "soda", "juice"].set 1 "tea" = ["water", "tea", "soda", "juice"]`
* `["water", "coffee", "soda", "juice"].set 4 "tea" = ["water", "coffee", "soda", "juice"]`
-/
def List.set : (l : List α) → (n : Nat) → (a : α) → List α
  | cons _ as, 0,          b => cons b as
  | cons a as, Nat.succ n, b => cons a (set as n b)
  | nil,       _,          _ => nil

/--
Folds a function over a list from the left, accumulating a value starting with `init`. The
accumulated value is combined with the each element of the list in order, using `f`.

Examples:
 * `[a, b, c].foldl f z  = f (f (f z a) b) c`
 * `[1, 2, 3].foldl (· ++ toString ·) "" = "123"`
 * `[1, 2, 3].foldl (s!"({·} {·})") "" = "((( 1) 2) 3)"`
-/
@[specialize]
def List.foldl {α : Type u} {β : Type v} (f : α → β → α) : (init : α) → List β → α
  | a, nil      => a
  | a, cons b l => foldl f (f a b) l

/--
Adds an element to the *end* of a list.

The added element is the last element of the resulting list.

Examples:
 * `List.concat ["red", "yellow"] "green" = ["red", "yellow", "green"]`
 * `List.concat [1, 2, 3] 4 = [1, 2, 3, 4]`
 * `List.concat [] () = [()]`
-/
def List.concat {α : Type u} : List α → α → List α
  | nil,       b => cons b nil
  | cons a as, b => cons a (concat as b)

/--
A string is a sequence of Unicode code points.

At runtime, strings are represented by [dynamic arrays](https://en.wikipedia.org/wiki/Dynamic_array)
of bytes using the UTF-8 encoding. Both the size in bytes (`String.utf8ByteSize`) and in characters
(`String.length`) are cached and take constant time. Many operations on strings perform in-place
modifications when the reference to the string is unique.
-/
structure String where
  /-- Pack a `List Char` into a `String`. This function is overridden by the
  compiler and is O(n) in the length of the list. -/
  mk ::
  /-- Unpack `String` into a `List Char`. This function is overridden by the
  compiler and is O(n) in the length of the list. -/
  data : List Char

/--
Decides whether two strings are equal. Normally used via the `DecidableEq String` instance and the
`=` operator.

At runtime, this function is overridden with an efficient native implementation.
-/
@[extern "lean_string_dec_eq"]
def String.decEq (s₁ s₂ : @& String) : Decidable (Eq s₁ s₂) :=
  match s₁, s₂ with
  | ⟨s₁⟩, ⟨s₂⟩ =>
    dite (Eq s₁ s₂) (fun h => isTrue (congrArg _ h)) (fun h => isFalse (fun h' => String.noConfusion h' (fun h' => absurd h' h)))

instance : DecidableEq String := String.decEq

/--
A byte position in a `String`, according to its UTF-8 encoding.

Character positions (counting the Unicode code points rather than bytes) are represented by plain
`Nat`s. Indexing a `String` by a `String.Pos` takes constant time, while character positions need to
be translated internally to byte positions, which takes linear time.

A byte position `p` is *valid* for a string `s` if `0 ≤ p ≤ s.endPos` and `p` lies on a UTF-8
character boundary.
-/
structure String.Pos where
  /-- Get the underlying byte index of a `String.Pos` -/
  byteIdx : Nat := 0