Zulip Chat Archive

Stream: general

Topic: mutual inductives docstring


Yaël Dillies (Sep 02 2021 at 14:05):

Dumb question... Where do I put the docstring on a mutual inductive definition? :thinking:
Eg, from set_theory.lists,

mutual inductive lists.equiv, lists'.subset
with lists.equiv : lists α  lists α  Prop
| refl (l) : lists.equiv l l
| antisymm {l₁ l₂ : lists' α tt} :
  lists'.subset l₁ l₂  lists'.subset l₂ l₁  lists.equiv _, l₁ _, l₂
with lists'.subset : lists' α tt  lists' α tt  Prop
| nil {l} : lists'.subset lists'.nil l
| cons {a a' l l'} : lists.equiv a a'  a'  lists'.to_list l' 
  lists'.subset l l'  lists'.subset (lists'.cons a l) l'
local infix ` ~ `:50 := lists.equiv

Alex J. Best (Sep 02 2021 at 14:17):

You could use docs#tactic.add_doc_string

import data.list.basic
-- /-- Foo and bar -/
mutual inductive {u v} foo, bar (α : Type u) (β : Type v)
with foo : nat  Type
| a : foo 0
| b {} (n : nat) : n < 3  foo 1
with bar : nat  Type
| c (n) : foo n  bar n
run_cmd tactic.add_doc_string `foo "foooo"
run_cmd tactic.add_doc_string `bar "barrr"

open tactic
#eval trace $ doc_string `foo
#eval trace $ doc_string `bar

Yaël Dillies (Sep 02 2021 at 14:18):

Smart smart smart!

Yaël Dillies (Sep 02 2021 at 14:25):

Don't know if this is expected behavior, but doing this puts the docstring on both lists.equiv and lists'.subset:

/-- A docstring -/
mutual inductive lists.equiv, lists'.subset
with lists.equiv : lists α  lists α  Prop
| refl (l) : lists.equiv l l
| antisymm {l₁ l₂ : lists' α tt} :
  lists'.subset l₁ l₂  lists'.subset l₂ l₁  lists.equiv _, l₁ _, l₂
with lists'.subset : lists' α tt  lists' α tt  Prop
| nil {l} : lists'.subset lists'.nil l
| cons {a a' l l'} : lists.equiv a a'  a'  lists'.to_list l' 
  lists'.subset l l'  lists'.subset (lists'.cons a l) l'
local infix ` ~ `:50 := lists.equiv

Rob Lewis (Sep 02 2021 at 14:41):

Alex J. Best said:

You could use docs#tactic.add_doc_string

import data.list.basic
-- /-- Foo and bar -/
mutual inductive {u v} foo, bar (α : Type u) (β : Type v)
with foo : nat  Type
| a : foo 0
| b {} (n : nat) : n < 3  foo 1
with bar : nat  Type
| c (n) : foo n  bar n
run_cmd tactic.add_doc_string `foo "foooo"
run_cmd tactic.add_doc_string `bar "barrr"

open tactic
#eval trace $ doc_string `foo
#eval trace $ doc_string `bar

Or better, command#add_decl_doc

Eric Wieser (Sep 02 2021 at 14:42):

Didn't Mario find a syntax for this in his weird syntax thread?

Yaël Dillies (Sep 02 2021 at 14:44):

Nope, what he did was to find a way to add docstrings to constructors of an inductive type. It didn't involve mutual inductives.

Yaël Dillies (Sep 02 2021 at 14:46):

By the way, these constructor docstrings don't seem to be picked up by docgen.


Last updated: Dec 20 2023 at 11:08 UTC