fix: support verus_spec in verusdoc

[Marsman1996]

Fix #2082

Now the verusdoc will display the doc for

#[verus_spec(ret =>
    with
        ghost_in1: Tracked<int>,
        ghost_in2: Tracked<int>,
        ->
        ghost_out: Ghost<(int,int)>,
    requires
        ghost_in1@ >= 0,
    ensures
        ghost_out@.0 == ghost_in1@,
        ret == 0,
)]
pub fn spec_with_example(&self) -> u32 {

as

pub exec fn spec_with_example(&self) -> ret : u32
with
  ghost_in1: Tracked <int>,
  ghost_in2: Tracked <int>,
  ->
  ghost_out: Ghost <(int,int)>,
requires
  ghost_in1@ >= 0,
ensures
  ghost_out@.0 == ghost_in1@,
  ret == 0,

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[rikosellic]

The generated doc of the example can be found here.