Documentation

Lean.Compiler.LCNF.MonadScope

@[reducible, inline]
Equations
    Instances For
      Instances
        @[reducible, inline]
        abbrev Lean.Compiler.LCNF.ScopeT (m : TypeType) (α : Type) :
        Equations
          Instances For
            def Lean.Compiler.LCNF.inScope {m : TypeType} [MonadScope m] [Monad m] (fvarId : FVarId) :
            Equations
              Instances For
                @[inline]
                def Lean.Compiler.LCNF.withParams {m : TypeType} {α : Type} [MonadScope m] [Monad m] (ps : Array Param) (x : m α) :
                m α
                Equations
                  Instances For
                    @[inline]
                    def Lean.Compiler.LCNF.withFVar {m : TypeType} {α : Type} [MonadScope m] [Monad m] (fvarId : FVarId) (x : m α) :
                    m α
                    Equations
                      Instances For
                        @[inline]
                        def Lean.Compiler.LCNF.withNewScope {m : TypeType} {α : Type} [MonadScope m] [Monad m] (x : m α) :
                        m α
                        Equations
                          Instances For