set comprehension issue

Stream: new members

[Matt Earnshaw]

lean does not like my definition of concat – hopefully self explanatory what i am trying to do, any pointers? thanks :-)

inductive word
  | ε : word
  | nonempty : char → word → word

infixr ` ⊚ ` :100 := word.nonempty
notation `language` := set word

def concat (U V : language) : language := {u ⊚ v | u ∈ U ∧ v ∈ V}

[Reid Barton]

You can't put an expression on the left side of set builder notation, just a variable

[Reid Barton]

So you could write something like {w | ∃ u v, u ∈ U ∧ v ∈ V ∧ w = u ⊚ v}

[Yury G. Kudryashov]

Or {w | ∃ (u ∈ U) (v ∈ V), w = u ⊚ v}

[Matt Earnshaw]

ok, thanks!

[Matt Earnshaw]

edit: nevermind