Documentation

Lean.Meta.Tactic.Simp.Simproc

Builtin simproc declaration extension state.

It contains:

  • The discrimination tree keys for each simproc (including symbolic evaluation procedures) name.
  • The actual procedure associated with a name.
Instances For

    This global reference is populated using the command builtin_simproc_pattern%.

    This reference is then used to process the attributes builtin_simproc and builtin_sevalproc. Both attributes need the keys and the actual procedure registered using the command builtin_simproc_pattern%.

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

            Given a declaration name declName, store the discrimination tree keys and the actual procedure.

            This method is invoked by the command builtin_simproc_pattern% elaborator.

            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
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  Builtin symbolic evaluation procedures.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[implemented_by Lean.Meta.Simp.getSimprocFromDeclImpl]
                    Equations
                    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

                          Implements attributes builtin_simproc and builtin_sevalproc.

                          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
                                  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
                                          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

                                                  Try to retrieve the simproc set using the simp or simproc attribute names. Recall that when we declare a simp set using register_simp_attr, an associated simproc set is automatically created. We use the function simpAttrNameToSimprocAttrName to find the simproc associated with the simp attribute.

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