Zulip Chat Archive
Stream: general
Topic: Let's add user-friendly doc-strings to core.
Scott Morrison (Jun 03 2020 at 07:09):
That's definitionally the doc-string for eq.rec: "Somebody messed up bad, probably you. If you're the sick sort of person who enjoys this kind of thing, Cubical Agda might be a better place for you."
Scott Morrison (Jun 03 2020 at 07:10):
[/jk] Who doesn't love an afternoon with eq.rec?
Johan Commelin (Jun 03 2020 at 07:11):
Kevin Buzzard said:
I think that the analogous docstring for
heqshould just say "please turn back, you made a mistake" ;-)
This! :+100:
Johan Commelin (Jun 03 2020 at 07:12):
Scott Morrison said:
That's definitionally the doc-string for
eq.rec: "Somebody messed up bad, probably you. If you're the sick sort of person who enjoys this kind of thing, Cubical Agda might be a better place for you."
/me is glad that his mic is muted
Johan Commelin (Jun 03 2020 at 07:20):
@Scott Morrison @Bryan Gin-ge Chen If we don't want to pollute the docstrings with advise on using mathlib and import tactic etc... we could add the docstrings in logic.basic instead of in core.
Johan Commelin (Jun 03 2020 at 07:20):
Or we could add a link to some documentation
Johan Commelin (Jun 03 2020 at 07:20):
I'm fine with adding things in core, btw
Johan Commelin (Jun 03 2020 at 07:22):
We could even add a docstring on → mentioning intros and specialize
Johan Commelin (Jun 03 2020 at 07:22):
Should the docstring on nat mention induction?
Scott Morrison (Jun 03 2020 at 07:23):
Can we replace doc-strings from mathlib?
Johan Commelin (Jun 03 2020 at 07:24):
Scott Morrison said:
Can we replace doc-strings from mathlib?
I don't know if we can replace, but we can certainly add them.
Johan Commelin (Jun 03 2020 at 07:53):
I have no idea how all these docstrings work... I can't "jump to definition" on →. Can we add a docstring to it?
Johan Commelin (Jun 03 2020 at 07:53):
How about \lambda?
Gabriel Ebner (Jun 03 2020 at 07:57):
→, λ, ∀, Type are not constants. Hence no docstrings and no go-to-definition.
Johan Commelin (Jun 03 2020 at 07:57):
Aha... too bad
Mario Carneiro (Jun 03 2020 at 08:18):
We could add them to the C++ :stuck_out_tongue:
Johan Commelin (Jun 03 2020 at 08:27):
I have no idea what the vscode extension needs to show docstrings etc... But I think it might be worth adding these docstrings to C++. Otherwise we'll get questions: why does \exists have helpful info, but \forall doesn't?
Last updated: Dec 20 2023 at 11:08 UTC