Lean syntax is weird

Stream: new members

[Ching-Tsun Chou]

The comment in the following code triggers the Lean error: "unexpected token 'open'; expected 'lemma'". Why? If I remove the open ... line, the error disappears but my proof breaks. What am I supposed to do here? I just want to add comments to my code.

/-- There is a gap between two successive occurrences of a predicate `p : ℕ → Prop`. -/
open scoped Classical in
theorem Nat.nth_succ_gap {p : ℕ → Prop} (hf : (setOf p).Infinite) (n : ℕ) :
    ∀ k < nth p (n + 1) - nth p n, k > 0 → ¬ p (k + nth p n) := by
  intro k h_k1 h_k0 h_p_k
  let m := count p (k + nth p n)
  have h_k_ex : nth p m = k + nth p n := by simp [m, nth_count h_p_k]
  have h_n_m : n < m := by apply (nth_lt_nth hf).mp ; omega
  have h_m_n : m < n + 1 := by apply (nth_lt_nth hf).mp ; omega
  omega

[Ching-Tsun Chou]

I found that exchanging the first two lines removes the error. But why should the location of a comment matter at all?

[Anthony Wang]

/-- -/ is a doc comment so it can only be used directly above a theorem, lemma, def etc.

[Ruben Van de Velde]

And notably, is not in any way a comment

[Ching-Tsun Chou]

How would you comment?

[Anthony Wang]

With /- -/ (one - instead of two)

[Ching-Tsun Chou]

But I want a doc comment.

[Anthony Wang]

You can swap the first two lines as you said above.

[Eric Wieser]

Doc comments are not "comments" in the usual sense of the word. Crucially, comments can go (almost) anywhere, doc comments can only go in fixed locations

[Julian Berman]

If you just want a sympathetic agreement, I also find this slightly ugly looking (and to my recollection @Yaël Dillies when I noticed this and mentioned it somewhere agreed). I wish the syntax were inverted in the way you hoped for, but the answer is simply that it isn't.

[Arthur Paulino]

Not really an apples-to-apples comparison, but Rust accepts both:

/// Moo.
#[inline]
fn moo() {}

#[inline]
/// Moo.
fn moo2() {}

[Anthony Wang]

For the Lean equivalent, seems like declaration modifiers have to come after the doc comment:

-- This works
/-- Moo. -/
@[inline]
def moo (a : Nat) := a

-- This doesn't
@[inline]
/-- Moo. -/
def moo2 (a : Nat) := a

So if you have both an open and a modifier the only order that works is

open scoped Classical in
/-- Moo. -/
@[inline]
def moo3 (a : Nat) := a

[Kevin Buzzard]

Agreed, I have noticed this before and thought it a little odd, but having no experience with any other programming languages I just accepted it as probably the way things were supposed to work.

[Ching-Tsun Chou]

By the way, I noticed that the rule for doc comment and a decoration like @[simp] is exactly the opposite: you must put the doc comment first.

[Aaron Liu]

open is a command on its own so it can't go in the middle of another command
in is a thing that attaches two commands together, so you need to put the entire declaration (including the doc comment if there is one) after the in

[Aaron Liu]

doc comments, and attributes like @[simp] and declaration modifiers like partial are part of the declaration syntax so they have to be directly attached to the def and they have to be in a certain order

[Aaron Liu]

so you can have /-- The foo. -/ @[simp] private protected noncomputable unsafe nonrec def foo but not some other order