Documentation

Lean.MonadEnv

Equations
Instances For
    def Lean.withEnv {m : TypeType} {α : Type} [Monad m] [MonadFinally m] [Lean.MonadEnv m] (env : Lean.Environment) (x : m α) :
    m α
    Equations
    Instances For
      def Lean.isInductive {m : TypeType} [Monad m] [Lean.MonadEnv m] (declName : Lake.Name) :
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def Lean.isRecCore (env : Lean.Environment) (declName : Lake.Name) :
        Equations
        Instances For
          def Lean.isRec {m : TypeType} [Monad m] [Lean.MonadEnv m] (declName : Lake.Name) :
          Equations
          Instances For
            @[inline]
            def Lean.withoutModifyingEnv {m : TypeType} [Monad m] [Lean.MonadEnv m] [MonadFinally m] {α : Type} (x : m α) :
            m α
            Equations
            Instances For
              @[inline]
              def Lean.withoutModifyingEnv' {m : TypeType} [Monad m] [Lean.MonadEnv m] [MonadFinally m] {α : Type} (x : m α) :

              Similar to withoutModifyingEnv, but also returns the updated environment

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[inline]
                def Lean.matchConst {m : TypeType} {α : Type} [Monad m] [Lean.MonadEnv m] (e : Lean.Expr) (failK : Unitm α) (k : Lean.ConstantInfoList Lean.Levelm α) :
                m α
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[inline]
                  def Lean.matchConstInduct {m : TypeType} {α : Type} [Monad m] [Lean.MonadEnv m] (e : Lean.Expr) (failK : Unitm α) (k : Lean.InductiveValList Lean.Levelm α) :
                  m α
                  Equations
                  Instances For
                    @[inline]
                    def Lean.matchConstCtor {m : TypeType} {α : Type} [Monad m] [Lean.MonadEnv m] (e : Lean.Expr) (failK : Unitm α) (k : Lean.ConstructorValList Lean.Levelm α) :
                    m α
                    Equations
                    Instances For
                      @[inline]
                      def Lean.matchConstRec {m : TypeType} {α : Type} [Monad m] [Lean.MonadEnv m] (e : Lean.Expr) (failK : Unitm α) (k : Lean.RecursorValList Lean.Levelm α) :
                      m α
                      Equations
                      Instances For
                        def Lean.hasConst {m : TypeType} [Monad m] [Lean.MonadEnv m] (constName : Lake.Name) :
                        Equations
                        Instances For
                          def Lean.mkAuxName {m : TypeType} [Monad m] [Lean.MonadEnv m] (baseName : Lake.Name) (idx : Nat) :
                          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
                                • 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
                                      @[inline]
                                      def Lean.matchConstStruct {m : TypeType} {α : Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] (e : Lean.Expr) (failK : Unitm α) (k : Lean.InductiveValList Lean.LevelLean.ConstructorValm α) :
                                      m α
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        unsafe def Lean.evalConst {m : TypeType} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] [Lean.MonadOptions m] (α : Type) (constName : Lake.Name) :
                                        m α
                                        Equations
                                        Instances For
                                          unsafe def Lean.evalConstCheck {m : TypeType} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] [Lean.MonadOptions m] (α : Type) (typeName : Lake.Name) (constName : Lake.Name) :
                                          m α
                                          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
                                              def Lean.isEnumType {m : TypeType} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] (declName : Lake.Name) :
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For