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.

def Lean.Meta.mkInstPiOfInstsForall (xs : Array Expr) (inst : Expr) : MetaM Expr

An n-ary version of mkInstPiOfInstForall. Takes an array of arguments instead.

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.

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.

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

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

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

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

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.