This module has meta-functions for constructions expressions related to Lean.Order. In particular some of these functions can handle the CCPO and CompleteLattice structures conveniently uniformly, picking the right one based on the type of the arguments.

def Lean.Meta.mkInstPiOfInstForall (x inst : Expr) : MetaM Expr

Given inst : CCPO (t[x]) for some FVar x, constructs an instance of the type CCPO (∀ x, t[x]). Can handle CompleteLattice as well.

Equations

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

def Lean.Meta.mkFixOfMonFun (packedType packedInst hmono : Expr) : MetaM Expr

Given a function f : α → α, an instance inst : CCPO α and a monotonicity proof hmono : monotone f, constructs a least fixpoint of f with respect to the instance inst. The packedType is assumed to contain the type α. Can handle CompleteLattice as well.

Equations

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

def Lean.Meta.toPartialOrder (packedInst : Expr) (type : Option Expr := none) : MetaM Expr

Given packedInst : CCPO α , returns an underlying instance of the type PartialOrder α. Can handle CompleteLattice as well. Takes an optional argument with the type α. If the optional argument is none, it is treated implicitly.

Equations

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

def Lean.Meta.mkInstCCPOPProd (inst₁ inst₂ : Expr) : MetaM Expr

Given CCPO instances inst₁ : CCPO α₁ and inst₂ : CCPO α₂, constructs an instance of the type CCPO (α₁ × α₂).

Equations

• Lean.Meta.mkInstCCPOPProd inst₁ inst₂ = Lean.Meta.mkAppOptM `Lean.Order.instCCPOPProd #[none, none, some inst₁, some inst₂]

def Lean.Meta.mkInstCompleteLatticePProd (inst₁ inst₂ : Expr) : MetaM Expr

Given CCPO instances inst₁ : CompleteLattice α₁ and inst₂ : CompleteLattice α₂, constructs an instance of the type CompleteLattice (α₁ × α₂).

Equations

• Lean.Meta.mkInstCompleteLatticePProd inst₁ inst₂ = Lean.Meta.mkAppOptM `Lean.Order.instCompleteLatticePProd #[none, none, some inst₁, some inst₂]

def Lean.Meta.mkPackedPPRodInstance (insts : Array Expr) : MetaM Expr

Given an array of CCPO instances insts = #[CCPO α₁, ..., CCPO αₙ], constructs an instance of the type CCPO (α₁ × ... × αₙ). Can handle CompleteLattice as well.

Equations

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