error on verso.doc

Stream: general

[Asei Inoue]

when doc.verso is set to true, the following unexpected error occurs.

set_option doc.verso true

/-- This code block in doc comment raise an error
```lean
#guard factorial 0 = 1
```
-/
def factorial (n : Nat) : Nat :=
  match n with
  | 0 => 1
  | n + 1 => (n + 1) * factorial n

-- This does not raise an error
#guard factorial 0 = 1

[Asei Inoue]

@David Thrane Christiansen I think you are working on this.

[Asei Inoue]

background

I think verso syntax in doc comment enables "test code in doc comment" style.
So I tried it in simple code.

[Asei Inoue]

oh, recursive function seems to be not allowed in doc comment...
The following code works. (fail as expectedly)

/--

```lean
#guard factorial 0 = 1
#guard factorial 5 = 120
```
-/
def factorial (n : Nat) : Nat :=
  match n with
  | 0 => 1
  | n + 1 => (n + 1)

[Robin Arnez]

Try

/--
This code block in doc comment doesn't raise an error
```lean
#guard factorial 0 = 1
```
-/
def factorial (n : Nat) : Nat :=
  match n with
  | 0 => 1
  | n + 1 => (n + 1) * factorial n

docs_to_verso factorial

For self-referential verso docs.

[Asei Inoue]

doc_to_verso is needed?
I think we want to use self reference in verso doc, so more convenient way is better…

[Asei Inoue]

try ... for self-referential verso docs

Your code does not work... :(

set_option doc.verso true

/--
This code block in doc comment doesn't raise an error
```lean
#guard factorial 0 = 1
```
-/
def factorial (n : Nat) : Nat :=
  match n with
  | 0 => 1
  | n + 1 => (n + 1) * factorial n

/- error: Documentation for `factorial` is already in Verso format  -/
docs_to_verso factorial