Documentation

Lean.Meta.CongrTheorems

  • fixed: Lean.Meta.CongrArgKind

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

  • fixedNoParam: Lean.Meta.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: Lean.Meta.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: Lean.Meta.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: Lean.Meta.CongrArgKind

    The lemma contains three parameters for this kind of argument a_i, b_i and eq_i : HEq 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: Lean.Meta.CongrArgKind

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

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

        Compute CongrArgKinds for a simp congruence theorem.

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

          Create 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

            Create a congruence theorem that is useful for the simplifier. In this kind of theorem, if the i-th argument is a cast argument, then the theorem contains an input a_i representing the i-th argument in the left-hand-side, and it appears with a cast (e.g., Eq.drec ... a_i ...) in the right-hand-side. The idea is that the right-hand-side of this theorem "tells" the simplifier how the resulting term looks like.

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

              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