leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: general

Topic: docstring in ctrl+space


Kenny Lau (Apr 21 2018 at 22:34):

The docstring is quite well-formatted when I hover over it, but not when I press Ctrl+space:
2018-04-22.png

Gabriel Ebner (Apr 22 2018 at 06:48):

fixed in 0.11.1

Kenny Lau (Apr 22 2018 at 06:49):

thanks


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll