CODEWITHSUNDEEP
prooflean
Yifan Dai
Yifan Dai

Reputation: 9

Lean 4 Invalid Field Notation

Minimum not-working example:

#check Or.intro_left

gives

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

on my machine.

Some experimentation seems to show that the error occurs whenever accessing elements (not sure if that's the correct term) using ..

Upvotes: 0

Views: 519

Answers (1)

Christopher Hughes
Christopher Hughes

Reputation: 1129

#check Or.inl works. I think it's just because there's no declaration called Or.intro_left in Lean4.

Upvotes: 1

Related Questions