Documentation

Lean.Server.Completion

@[export lean_completion_add_to_black_list]
Instances For
    @[inline, reducible]
    Instances For
      def Lean.Server.Completion.matchNamespace (ns : Lake.Name) (nsFragment : Lake.Name) (danglingDot : Bool) :
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For