mutual inductives docstring

Stream: general

[Yaël Dillies]

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]

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]

Smart smart smart!

[Yaël Dillies]

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]

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]

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

[Yaël Dillies]

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]

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