Documentation

EqLift.Tactic.Kernel.KernelLift

Implementation of the lift_eq tactic for kernels. #

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

source
def liftComposition (e : Lean.Expr) (maxLvl : Lean.Level) (proofs : List Lean.Expr) :
Lean.MetaM (Lean.Expr × List Lean.Expr)

Lifts a composition of kernels by lifting the inner kernels.

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

    Lifts a parallel composition of kernels by lifting the inner kernels.

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

      Lifts a product of kernels by lifting the inner kernels.

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

        Lifts a composition-product of kernels by lifting the inner kernels.

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

          Lifts a composition of kernels by lifting the carrier type.

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

            Lifts a discard kernel by lifting the carrier type.

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

              Lifts a copy kernel by lifting the carrier type.

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

                Lifts a swap kernel by lifting the carrier types.

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

                  Lifts a kernel using Kernel.lift.

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

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

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