Documentation

Init.Meta

Equations
Instances For
    Equations
    Instances For

      erw [rules] is a shorthand for rw (transparency := .default) [rules]. This does rewriting up to unfolding of regular definitions (by comparison to regular rw which only unfolds @[reducible] definitions).

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

              simp! is shorthand for simp with autoUnfold := true. This will unfold applications of functions defined by pattern matching, when one of the patterns applies. This can be used to partially evaluate many definitions.

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

                simp_arith has been deprecated. It was a shorthand for simp +arith +decide. Note that +decide is not needed for reducing arithmetic terms since simprocs have been added to Lean.

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

                  simp_arith! has been deprecated. It was a shorthand for simp! +arith +decide. Note that +decide is not needed for reducing arithmetic terms since simprocs have been added to Lean.

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

                    simp_all! is shorthand for simp_all with autoUnfold := true. This will unfold applications of functions defined by pattern matching, when one of the patterns applies. This can be used to partially evaluate many definitions.

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

                      simp_all_arith has been deprecated. It was a shorthand for simp_all +arith +decide. Note that +decide is not needed for reducing arithmetic terms since simprocs have been added to Lean.

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

                        simp_all_arith! has been deprecated. It was a shorthand for simp_all! +arith +decide. Note that +decide is not needed for reducing arithmetic terms since simprocs have been added to Lean.

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

                          dsimp! is shorthand for dsimp with autoUnfold := true. This will unfold applications of functions defined by pattern matching, when one of the patterns applies. This can be used to partially evaluate many definitions.

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