'open' error

Stream: new members

[Holly Liu]

i have this code (by a member of lean zulip):

open free_group (of)

/- The 3-strand braid group. -/
def braids_rel3 : set (free_group (fin 2)) :=
{(of 0)⁻¹ * (of 1)⁻¹ * (of 0)⁻¹ * of 1 * of 0 * of 1}

i am getting red underlines under open and each of, the error being command does not accept doc string. how do i resolve this?

[Holly Liu]

these are my imports:

import data.zmod.basic
import group_theory.presented_group
import group_theory.free_group
import data.equiv.mul_add
import algebra.group.defs
import algebra.group_power
import tactic

[Bryan Gin-ge Chen]

Do you have a doc string before open? (i.e. a comment that starts with /-- and ends with -/)

[Bryan Gin-ge Chen]

If so, try changing the first /-- to /- instead.

[Holly Liu]

that fixed it, thanks

[Scott Morrison]

(It's a good idea to post code snippets as a #mwe --- i.e. an entire file (ideally minimised) that we could copy and paste into an editor window. e.g. in this example Bryan wouldn't have needed to deduce you had a misplaced doc-string.)

[Holly Liu]

alright i'll do that next time