Zulip Chat Archive

Stream: new members

Topic: Disjunctions in "Theorem Proving in Lean 4"


Andreas Hofmeister (Nov 20 2021 at 18:09):

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

Last updated: Dec 20 2023 at 11:08 UTC