Documentation

Lean.ReducibilityAttrs

source
inductive Lean.ReducibilityStatus :
Type

Reducibility status for a definition.

Instances For
    source
    instance Lean.instInhabitedReducibilityStatus :
    Inhabited Lean.ReducibilityStatus
    source
    instance Lean.instReprReducibilityStatus :
    Repr Lean.ReducibilityStatus
    source
    opaque Lean.reducibilityAttrs :
    Lean.EnumAttributes Lean.ReducibilityStatus

    Environment extension for storing the reducibility attribute for definitions.

    source
    def Lean.getReducibilityStatus {m : Type → Type} [Monad m] [Lean.MonadEnv m] (declName : Lake.Name) :
    m Lean.ReducibilityStatus

    Return the reducibility attribute for the given declaration.

    Instances For
      source
      def Lean.setReducibilityStatus {m : Type → Type} [Monad m] [Lean.MonadEnv m] (declName : Lake.Name) (s : Lean.ReducibilityStatus) :
      m Unit

      Set the reducibility attribute for the given declaration.

      Instances For
        source
        def Lean.setReducibleAttribute {m : Type → Type} [Monad m] [Lean.MonadEnv m] (declName : Lake.Name) :
        m Unit

        Set the given declaration as [reducible]

        Instances For
          source
          def Lean.isReducible {m : Type → Type} [Monad m] [Lean.MonadEnv m] (declName : Lake.Name) :
          m Bool

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

          Instances For
            source
            def Lean.isIrreducible {m : Type → Type} [Monad m] [Lean.MonadEnv m] (declName : Lake.Name) :
            m Bool

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

            Instances For