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 : 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 : 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
        Instances For
          Equations
            Instances For
              partial def Lean.Meta.mkHCongrWithArity.withNewEqs.loop {α : Type} (xs ys : Array Expr) (k : Array ExprArray CongrArgKindMetaM α) (i : Nat) (eqs : Array Expr) (kinds : Array CongrArgKind) :
              Equations
                Instances For

                  Compute CongrArgKinds for a simp congruence theorem.

                  Equations
                    Instances For

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

                      Equations
                        Instances For
                          def Lean.Meta.mkCongrSimpCore? (f : Expr) (info : FunInfo) (kinds : Array CongrArgKind) (subsingletonInstImplicitRhs : Bool := true) :

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

                          Equations
                            Instances For
                              def Lean.Meta.mkCongrSimpCore?.mk? (subsingletonInstImplicitRhs : Bool := true) (f : Expr) (info : FunInfo) (kinds : Array CongrArgKind) :

                              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
                                Instances For
                                  partial def Lean.Meta.mkCongrSimpCore?.mk?.go (subsingletonInstImplicitRhs : Bool := true) (f : Expr) (info : FunInfo) (kinds : Array CongrArgKind) (lhss : Array Expr) (i : Nat) (rhss : Array Expr) (eqs : Array (Option Expr)) (hyps : Array Expr) :
                                  Equations
                                    Instances For
                                      def Lean.Meta.mkCongrSimp? (f : Expr) (subsingletonInstImplicitRhs : Bool := true) :

                                      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
                                        Instances For
                                          Equations
                                            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
                                                        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
                                                            Instances For