Documentation

Lean.Compiler.LCNF.MonadScope

source
@[inline, reducible]
abbrev Lean.Compiler.LCNF.Scope :
Type
Instances For
    source
    class Lean.Compiler.LCNF.MonadScope (m : Type → Type) :
    Type 1
    Instances
      source
      @[inline, reducible]
      abbrev Lean.Compiler.LCNF.ScopeT (m : Type → Type) (α : Type) :
      Type
      Instances For
        source
        instance Lean.Compiler.LCNF.instMonadScopeScopeT {m : Type → Type} [Monad m] :
        Lean.Compiler.LCNF.MonadScope (Lean.Compiler.LCNF.ScopeT m)
        source
        instance Lean.Compiler.LCNF.instMonadScope (m : Type → Type) (n : Type → Type) [MonadLift m n] [MonadFunctor m n] [Lean.Compiler.LCNF.MonadScope m] :
        Lean.Compiler.LCNF.MonadScope n
        source
        def Lean.Compiler.LCNF.inScope {m : Type → Type} [Lean.Compiler.LCNF.MonadScope m] [Monad m] (fvarId : Lean.FVarId) :
        m Bool
        Instances For
          source
          @[inline]
          def Lean.Compiler.LCNF.withParams {m : Type → Type} {α : Type} [Lean.Compiler.LCNF.MonadScope m] [Monad m] (ps : Array Lean.Compiler.LCNF.Param) (x : m α) :
          m α
          Instances For
            source
            @[inline]
            def Lean.Compiler.LCNF.withFVar {m : Type → Type} {α : Type} [Lean.Compiler.LCNF.MonadScope m] [Monad m] (fvarId : Lean.FVarId) (x : m α) :
            m α
            Instances For
              source
              @[inline]
              def Lean.Compiler.LCNF.withNewScope {m : Type → Type} {α : Type} [Lean.Compiler.LCNF.MonadScope m] [Monad m] (x : m α) :
              m α
              Instances For