Lift and Unlift utilities

This file provides utility functions for lifting and unlifting equalities.

@[reducible, inline]

abbrev liftMetadata : Type

A type alias for lifting/unlifting functions.

Equations

• liftMetadata = (Lean.Expr → Lean.Level → List Lean.Expr → Lean.MetaM (Lean.Expr × List Lean.Expr))

@[reducible, inline]

abbrev finisherMetadata : Type

A type alias for finisher functions that construct the final proof of equality after lifting/ unlifting inner expressions.

Equations

• finisherMetadata = (Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Level → Lean.MetaM Lean.Expr)

def transformExpr (e : Lean.Expr) (maxLvl : Lean.Level) (proofs : List Lean.Expr) (impl_ref : IO.Ref (Array liftMetadata)) : Lean.MetaM (Lean.Expr × List Lean.Expr)

Transforms an expression using the registered lifting/unlifting functions given in impl_ref. Returns the first successful transformation along with the updated list of proofs.

Equations

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

def Lean.MVarId.nthRewrite (mvarId : MVarId) (n : Nat) (heq : Expr) : MetaM MVarId

Rewrites the type of mvarId at the n-th occurrence using heq.

Equations

• mvarId.nthRewrite n heq = do let __do_lift ← mvarId.getType let r ← mvarId.rewrite __do_lift heq false { occs := Lean.Meta.Occurrences.pos [n] } mvarId.replaceTargetEq r.eNew r.eqProof

def constructProof (eqProofType lhs rhs lhs_t rhs_t : Lean.Expr) (maxLvl : Lean.Level) (proofs : List Lean.Expr) (finisher_ref : IO.Ref (Array finisherMetadata)) : Lean.MetaM Lean.Expr

Constructs a proof of equality between the original and transformed expressions using the provided proofs and finisher functions.

Equations

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

def transformEquality (getLvl : Lean.Expr → Lean.MetaM Lean.Level) (lift_ref : IO.Ref (Array liftMetadata)) (finisher_ref : IO.Ref (Array finisherMetadata)) (eq : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr)

Lifts or unlifts an equality expression by transforming both sides using the registered lifting/ unlifting functions. Returns the transformed equality and a proof of equality between the original and transformed expressions.

Equations

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