Documentation

Lean.Meta.PProdN

This module provides functions to pack and unpack values using nested PProd or And, as used in the .below construction, in the .brecOn construction for mutual recursion and and the mutual_induct construction.

It uses And (equivalent to PProd.{0} when possible).

The nesting is t₁ ×' (t₂ ×' t₃), not t₁ ×' (t₂ ×' (t₃ ×' PUnit)). This is more readable, slightly shorter, and means that the packing is the identity if n=1, which we rely on in some places. It comes at the expense that hat projection needs to know n.

Packing an empty list uses True or PUnit depending on the given lvl.

Also see Lean.Meta.ArgsPacker for a similar module for PSigma and PSum, used by well-founded recursion.

Given types t₁ and t₂, produces t₁ ×' t₂ (or t₁ ∧ t₂ if the universes allow)

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

    Given values of typs t₁ and t₂, produces value of type t₁ ×' t₂ (or t₁ ∧ t₂ if the universes allow)

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

      PProd.fst or And.left (using .proj)

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

        PProd.snd or And.right (using .proj)

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

          Given types tᵢ, produces t₁ ×' t₂ ×' t₃

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

            Given values xᵢ of type tᵢ, produces value of type t₁ ×' t₂ ×' t₃

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

              Given a value of type t₁ ×' … ×' tᵢ ×' … ×' tₙ, return a value of type tᵢ

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

                Packs multiple type-forming lambda expressions taking the same parameters using PProd.

                The parameter type is the common type of the these expressions

                For example

                packLambdas (Nat → Sort u) #[(fun (n : Nat) => Nat), (fun (n : Nat) => Fin n -> Fin n )]
                

                will return

                fun (n : Nat) => (Nat ×' (Fin n → Fin n))
                

                It is the identity if es.size = 1.

                It returns a dummy motive (xs : ) → PUnit or (xs : … ) → True if no expressions are given. (this is the reason we need the expected type in the type parameter).

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

                  The value analogue to PProdN.packLambdas.

                  It is the identity if es.size = 1.

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