Documentation

Mathlib.Data.Erased

A type for VM-erased data #

This file defines a type Erased α which is classically isomorphic to α, but erased in the VM. That is, at runtime every value of Erased α is represented as 0, just like types and proofs.

def Erased (α : Sort u) :
Sort (max 1 u)

Erased α is the same as α, except that the elements of Erased α are erased in the VM in the same way as types and proofs. This can be used to track data without storing it literally.

Equations
  • Erased α = ((s : αProp) ×' ∃ (a : α), (fun (b : α) => a = b) = s)
Instances For
    @[inline]
    def Erased.mk {α : Sort u_1} (a : α) :

    Erase a value.

    Equations
    Instances For
      noncomputable def Erased.out {α : Sort u_1} :
      Erased αα

      Extracts the erased value, noncomputably.

      Equations
      Instances For
        @[reducible, inline]
        abbrev Erased.OutType (a : Erased (Sort u)) :

        Extracts the erased value, if it is a type.

        Note: (mk a).OutType is not definitionally equal to a.

        Equations
        • a.OutType = a.out
        Instances For
          theorem Erased.out_proof {p : Prop} (a : Erased p) :
          p

          Extracts the erased value, if it is a proof.

          @[simp]
          theorem Erased.out_mk {α : Sort u_1} (a : α) :
          (Erased.mk a).out = a
          @[simp]
          theorem Erased.mk_out {α : Sort u_1} (a : Erased α) :
          Erased.mk a.out = a
          theorem Erased.out_inj {α : Sort u_1} (a : Erased α) (b : Erased α) (h : a.out = b.out) :
          a = b
          noncomputable def Erased.equiv (α : Sort u_1) :
          Erased α α

          Equivalence between Erased α and α.

          Equations
          • Erased.equiv α = { toFun := Erased.out, invFun := Erased.mk, left_inv := , right_inv := }
          Instances For
            instance Erased.instRepr (α : Type u) :
            Equations
            instance Erased.instToString (α : Type u) :
            Equations
            def Erased.choice {α : Sort u_1} (h : Nonempty α) :

            Computably produce an erased value from a proof of nonemptiness.

            Equations
            Instances For
              @[simp]
              theorem Erased.nonempty_iff {α : Sort u_1} :
              instance Erased.instInhabitedOfNonempty {α : Sort u_1} [h : Nonempty α] :
              Equations
              def Erased.bind {α : Sort u_1} {β : Sort u_2} (a : Erased α) (f : αErased β) :

              (>>=) operation on Erased.

              This is a separate definition because α and β can live in different universes (the universe is fixed in Monad).

              Equations
              • a.bind f = fun (b : β) => (f a.out).fst b,
              Instances For
                @[simp]
                theorem Erased.bind_eq_out {α : Sort u_1} {β : Sort u_2} (a : Erased α) (f : αErased β) :
                a.bind f = f a.out
                def Erased.join {α : Sort u_1} (a : Erased (Erased α)) :

                Collapses two levels of erasure.

                Equations
                • a.join = a.bind id
                Instances For
                  @[simp]
                  theorem Erased.join_eq_out {α : Sort u_1} (a : Erased (Erased α)) :
                  a.join = a.out
                  def Erased.map {α : Sort u_1} {β : Sort u_2} (f : αβ) (a : Erased α) :

                  (<$>) operation on Erased.

                  This is a separate definition because α and β can live in different universes (the universe is fixed in Functor).

                  Equations
                  Instances For
                    @[simp]
                    theorem Erased.map_out {α : Sort u_1} {β : Sort u_2} {f : αβ} (a : Erased α) :
                    (Erased.map f a).out = f a.out
                    Equations
                    @[simp]
                    theorem Erased.pure_def {α : Type u_1} :
                    pure = Erased.mk
                    @[simp]
                    theorem Erased.bind_def {α : Type u_1} {β : Type u_1} :
                    (fun (x : Erased α) (x_1 : αErased β) => x >>= x_1) = Erased.bind
                    @[simp]
                    theorem Erased.map_def {α : Type u_1} {β : Type u_1} :
                    (fun (x : αβ) (x_1 : Erased α) => x <$> x_1) = Erased.map