Documentation

Lean.Meta.CongrTheorems

  • fixed : CongrArgKind

    It is a parameter for the congruence theorem, the parameter occurs in the left and right hand sides.

  • fixedNoParam : CongrArgKind

    It is not a parameter for the congruence theorem, the theorem was specialized for this parameter. This only happens if the parameter is a subsingleton/proposition, and other parameters depend on it.

  • eq : CongrArgKind

    The lemma contains three parameters for this kind of argument a_i, b_i and eq_i : a_i = b_i. a_i and b_i represent the left and right hand sides, and eq_i is a proof for their equality.

  • cast : CongrArgKind

    The congr-simp theorems contains only one parameter for this kind of argument, and congr theorems contains two. They correspond to arguments that are subsingletons/propositions.

  • heq : CongrArgKind

    The lemma contains three parameters for this kind of argument a_i, b_i and eq_i : a_i ≍ b_i. a_i and b_i represent the left and right hand sides, and eq_i is a proof for their heterogeneous equality.

  • subsingletonInst : CongrArgKind

    For congr-simp theorems only. Indicates a decidable instance argument. The lemma contains two arguments [a_i : Decidable ...] [b_i : Decidable ...]

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

          Computes CongrArgKinds for a simp congruence theorem.

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

            Variant of getCongrSimpKinds for rewriting just argument 0. If it is possible to rewrite, the 0th CongrArgKind is .eq, and otherwise it is .fixed. This is used for the arg conv tactic.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def Lean.Meta.mkCongrSimpCore? (f : Expr) (info : FunInfo) (kinds : Array CongrArgKind) (subsingletonInstImplicitRhs : Bool := true) :

              Creates a congruence theorem that is useful for the simplifier and congr tactic.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def Lean.Meta.mkCongrSimp? (f : Expr) (subsingletonInstImplicitRhs : Bool := true) (maxArgs? : Option Nat := none) :

                Create a congruence theorem for f. The theorem is used in the simplifier.

                If subsingletonInstImplicitRhs = true, the rhs corresponding to [Decidable p] parameters is marked as instance implicit. It forces the simplifier to compute the new instance when applying the congruence theorem. For the congr tactic we set it to false.

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

                  Returns true if s is of the form hcongr_<idx>

                  Equations
                  Instances For
                    Equations
                    Instances For
                      def Lean.Meta.mkHCongrWithArityForConst? (declName : Name) (levels : List Level) (numArgs : Nat) :

                      Similar to mkHCongrWithArity, but uses reserved names to ensure we don't keep creating the same congruence theorem over and over again.

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

                        Similar to mkCongrSimp?, but uses reserved names to ensure we don't keep creating the same congruence theorem over and over again.

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