Documentation

EqLift.Tactic.Kernel.KernelUnlift

Implementation of the unlift_eq tactic for kernels. #

This file contains functions that propagate the unlifting of lifted kernel expressions through several operators and primitives, and constructs the necessary proofs for the unlift_eq tactic.

source
def unliftComposition (e : Lean.Expr) (eLvl : Lean.Level) (proofs : List Lean.Expr) :
Lean.MetaM (Lean.Expr × List Lean.Expr)

Unlifts a composition of kernels by unlifting the inner kernels.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def unliftParallelComp (e : Lean.Expr) (eLvl : Lean.Level) (proofs : List Lean.Expr) :
    Lean.MetaM (Lean.Expr × List Lean.Expr)

    Unlifts a parallel composition of kernels by unlifting the inner kernels.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def unliftProd (e : Lean.Expr) (eLvl : Lean.Level) (proofs : List Lean.Expr) :
      Lean.MetaM (Lean.Expr × List Lean.Expr)

      Unlifts a product of kernels by unlifting the inner kernels.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def unliftCompProd (e : Lean.Expr) (eLvl : Lean.Level) (proofs : List Lean.Expr) :
        Lean.MetaM (Lean.Expr × List Lean.Expr)

        Unlifts a composition-product of kernels by unlifting the inner kernels.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def unliftId (e : Lean.Expr) (eLvl : Lean.Level) (proofs : List Lean.Expr) :
          Lean.MetaM (Lean.Expr × List Lean.Expr)

          Unlifts the identity kernel by unlifting the carrier type.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def unliftDiscard (e : Lean.Expr) (eLvl : Lean.Level) (proofs : List Lean.Expr) :
            Lean.MetaM (Lean.Expr × List Lean.Expr)

            Unlifts the discard kernel by unlifting the carrier type.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def unliftCopy (e : Lean.Expr) (eLvl : Lean.Level) (proofs : List Lean.Expr) :
              Lean.MetaM (Lean.Expr × List Lean.Expr)

              Unlifts the copy kernel by unlifting the carrier type.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def unliftSwap (e : Lean.Expr) (eLvl : Lean.Level) (proofs : List Lean.Expr) :
                Lean.MetaM (Lean.Expr × List Lean.Expr)

                Unlifts the swap kernel by unlifting the carrier types.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def unliftKernel (e : Lean.Expr) :
                  Lean.Level → (proofs : List Lean.Expr) → Lean.MetaM (Lean.Expr × List Lean.Expr)

                  Unlifts a lifted kernel by returning the inner kernel.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def finisherKernelUnlift :
                    Lean.Expr → Lean.Expr → (lhs rhs : Lean.Expr) → (maxLvl : Lean.Level) → Lean.MetaM Lean.Expr

                    Constructs the finisher proof that concludes the unlifting after rewriting the equalities.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For