Disjunctions in "Theorem Proving in Lean 4"

Stream: new members

[Andreas Hofmeister]

I have just installed Lean for the first time (version 4.0.0-m2, commit 26dda3f63d88) and I am reading "Theorem Proving in Lean 4". I have gotten as far as the "Disjunction" section in the third chapter "Propositions and Proofs". The examples before that section worked as described in the text, but the examples in that section do not. The example

variable (p q : Prop)
example (hp : p) : p ∨ q := Or.intro_left q hp

produces the error

Mypackage.lean:2:28: error: invalid field notation, type is not of the form (C ...) where C is a constant
  Or
has type
  Prop → Prop → Prop