Documentation

Lean.Meta.Tactic.Grind.Propagate

source
def Lean.Meta.Grind.propagateAndUp :
Propagator

Propagates equalities for a conjunction a ∧ b based on the truth values of its components a and b. This function checks the truth value of a and b, and propagates the following equalities:

  • If a = True, propagates (a ∧ b) = b.
  • If b = True, propagates (a ∧ b) = a.
  • If a = False, propagates (a ∧ b) = False.
  • If b = False, propagates (a ∧ b) = False.
Instances For
    source
    def Lean.Meta.Grind.propagateAndDown :
    Propagator

    Propagates truth values downwards for a conjunction a ∧ b when the expression itself is known to be True.

    Instances For
      source
      def Lean.Meta.Grind.propagateOrUp :
      Propagator

      Propagates equalities for a disjunction a ∨ b based on the truth values of its components a and b. This function checks the truth value of a and b, and propagates the following equalities:

      • If a = False, propagates (a ∨ b) = b.
      • If b = False, propagates (a ∨ b) = a.
      • If a = True, propagates (a ∨ b) = True.
      • If b = True, propagates (a ∨ b) = True.
      Instances For
        source
        def Lean.Meta.Grind.propagateOrDown :
        Propagator

        Propagates truth values downwards for a disjunction a ∨ b when the expression itself is known to be False.

        Instances For
          source
          def Lean.Meta.Grind.propagateNotUp :
          Propagator

          Propagates equalities for a negation Not a based on the truth value of a. This function checks the truth value of a and propagates the following equalities:

          Instances For
            source
            def Lean.Meta.Grind.propagateNotDown :
            Propagator

            Propagates truth values downwards for a negation expression Not a based on the truth value of Not a. This function performs the following:

            Instances For
              source
              def Lean.Meta.Grind.propagateBoolDiseq (eq a b : Expr) :
              GoalM Unit
              Instances For
                source
                def Lean.Meta.Grind.propagateEqUp :
                Propagator

                Propagates Eq upwards

                Instances For
                  source
                  def Lean.Meta.Grind.propagateEqDown :
                  Propagator

                  Propagates Eq downwards

                  Instances For
                    source
                    def Lean.Meta.Grind.propagateBEqUp :
                    Propagator
                    Instances For
                      source
                      def Lean.Meta.Grind.propagateBEqDown :
                      Propagator
                      Instances For
                        source
                        def Lean.Meta.Grind.propagateEqMatchDown :
                        Propagator

                        Propagates EqMatch downwards

                        Instances For
                          source
                          def Lean.Meta.Grind.propagateHEqDown :
                          Propagator

                          Propagates HEq downwards

                          Instances For
                            source
                            def Lean.Meta.Grind.propagateHEqUp :
                            Propagator

                            Propagates HEq upwards

                            Instances For
                              source
                              def Lean.Meta.Grind.propagateIte :
                              Propagator

                              Propagates ite upwards

                              Instances For
                                source
                                def Lean.Meta.Grind.propagateDIte :
                                Propagator

                                Propagates dite upwards

                                Instances For
                                  source
                                  def Lean.Meta.Grind.propagateDecideDown :
                                  Propagator
                                  Instances For
                                    source
                                    def Lean.Meta.Grind.propagateDecideUp :
                                    Propagator
                                    Instances For
                                      source
                                      def Lean.Meta.Grind.propagateBoolAndUp :
                                      Propagator

                                      Bool version of propagateAndUp

                                      Instances For
                                        source
                                        def Lean.Meta.Grind.propagateBoolAndDown :
                                        Propagator

                                        Bool version of propagateAndDown

                                        Instances For
                                          source
                                          def Lean.Meta.Grind.propagateBoolOrUp :
                                          Propagator

                                          Bool version of propagateOrUp

                                          Instances For
                                            source
                                            def Lean.Meta.Grind.propagateBoolOrDown :
                                            Propagator

                                            Bool version of propagateOrDown

                                            Instances For
                                              source
                                              def Lean.Meta.Grind.propagateBoolNotUp :
                                              Propagator

                                              Bool version of propagateNotUp

                                              Instances For
                                                source
                                                def Lean.Meta.Grind.propagateBoolNotDown :
                                                Propagator

                                                Bool version of propagateNotDown

                                                Instances For