Documentation

Lean.ReducibilityAttrs

Reducibility status for a definition.

Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[export lean_get_reducibility_status]
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Return the reducibility attribute for the given declaration.

        Equations
        Instances For

          Set the reducibility attribute for the given declaration.

          Equations
          Instances For

            Set the given declaration as [reducible]

            Equations
            Instances For
              def Lean.isReducible {m : TypeType} [Monad m] [Lean.MonadEnv m] (declName : Lake.Name) :

              Return true if the given declaration has been marked as [reducible].

              Equations
              Instances For
                def Lean.isIrreducible {m : TypeType} [Monad m] [Lean.MonadEnv m] (declName : Lake.Name) :

                Return true if the given declaration has been marked as [irreducible]

                Equations
                Instances For

                  Set the given declaration as [irreducible]

                  Equations
                  Instances For