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. Each function returns the unlifted expression e' together with a proof of e = e'.lift, built by congruence from the compatibility lemmas of Kernel.lift (comp_lift, parallelComp_lift, ...).

def unliftBinary (e κ' η' : Lean.Expr) (eLvl : Lean.Level) (mkOp mkPf : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr)

Unlifts a binary kernel operation e = op κ' η' by unlifting the inner kernels. mkOp builds the operation from the unlifted kernels κ η, and mkPf must return a proof of op κ.lift η.lift = (op κ η).lift.

Equations

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

def unliftComposition (e : Lean.Expr) (eLvl : Lean.Level) : Lean.MetaM (Lean.Expr × 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.

def unliftParallelComp (e : Lean.Expr) (eLvl : Lean.Level) : Lean.MetaM (Lean.Expr × 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.

def unliftProd (e : Lean.Expr) (eLvl : Lean.Level) : Lean.MetaM (Lean.Expr × 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.

def unliftCompProd (e : Lean.Expr) (eLvl : Lean.Level) : Lean.MetaM (Lean.Expr × 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.

def unliftCarrier (X' : Lean.Expr) : Lean.MetaM Carrier

The original carrier of a lifted carrier.

Equations

• unliftCarrier X' = do let __x ← getOriginalType X' match __x with | (type, lvl) => pure { type := type, lvl := lvl }

def unliftId (e : Lean.Expr) (eLvl : Lean.Level) : Lean.MetaM (Lean.Expr × Lean.Expr)

Unlifts the identity kernel by unlifting the carrier type.

Equations

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

def unliftDiscard (e : Lean.Expr) (eLvl : Lean.Level) : Lean.MetaM (Lean.Expr × Lean.Expr)

Unlifts the discard kernel by unlifting the carrier type.

Equations

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

def unliftCopy (e : Lean.Expr) (eLvl : Lean.Level) : Lean.MetaM (Lean.Expr × Lean.Expr)

Unlifts the copy kernel by unlifting the carrier type.

Equations

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

def unliftSwap (e : Lean.Expr) (eLvl : Lean.Level) : Lean.MetaM (Lean.Expr × Lean.Expr)

Unlifts the swap kernel by unlifting the carrier types.

Equations

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

def unliftKernel (e : Lean.Expr) : Lean.Level → Lean.MetaM (Lean.Expr × Lean.Expr)

Unlifts a lifted kernel by returning the inner kernel.

Equations

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