Documentation

Lean.Compiler.LCNF.MonadScope

@[inline, reducible]
Equations
Instances For
    Instances
      @[inline, reducible]
      abbrev Lean.Compiler.LCNF.ScopeT (m : TypeType) (α : Type) :
      Equations
      Instances For
        Equations
        • Lean.Compiler.LCNF.instMonadScopeScopeT = { getScope := read, withScope := fun {α : Type} => withReader }
        Equations
        • One or more equations did not get rendered due to their size.
        Equations
        Instances For
          @[inline]
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[inline]
            def Lean.Compiler.LCNF.withFVar {m : TypeType} {α : Type} [Lean.Compiler.LCNF.MonadScope m] [Monad m] (fvarId : Lean.FVarId) (x : m α) :
            m α
            Equations
            Instances For