Documentation

Lean.Meta.Order

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.

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
    Instances For
      def Lean.Meta.mkFixOfMonFun (packedType packedInst hmono : 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
        Instances For
          def Lean.Meta.toPartialOrder (packedInst : Expr) (type : Option Expr := none) :

          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
            Instances For
              def Lean.Meta.mkInstCCPOPProd (inst₁ inst₂ : Expr) :

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

              Equations
                Instances For

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

                  Equations
                    Instances For

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

                      Equations
                        Instances For