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
      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
                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
                  • One or more equations did not get rendered due to their size.
                  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
                    • One or more equations did not get rendered due to their size.
                    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
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        def Lean.hasConst {m : TypeType} [Monad m] [Lean.MonadEnv m] (constName : Lake.Name) :
                        Equations
                        • Lean.hasConst constName = do let __do_liftLean.getEnv pure (__do_lift.contains constName)
                        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
                              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 α
                                          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 α
                                            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