Strange typechecking or parsing issue in lean4

Stream: lean4

[Arien Malec]

I've been translating my lean3 TPIL code to lean4, and have run into a weird issue.

I have the proof:

example {p: Prop} {q: Prop} {r: Prop} : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
  Iff.intro
    (fun (h: (p ∧ q) ∧ r) => And.intro h.left.left (And.intro h.left.right h.right))
    (fun (h: p ∧ (q ∧ r)) => And.intro (And.intro h.left h.right.left) h.right.right)

which typechecks just fine. If I write the word thoerem under it, I immediately get the error

function expected at
  { mp := fun h => { left := h.left.left, right := { left := h.left.right, right := h.right } },
    mpr := fun h => { left := { left := h.left, right := h.right.left }, right := h.right.right } }
term has type
  ?m.305 ↔ ?m.306

if, instead, I have

example : p → p := sorry

everything typechecks just fine.

If, under that example, I write theorem, I get the error at the sorry

function expected at
  sorryAx ?m.375
term has type
  ?m.375

[Kevin Buzzard]

This looks like a syntax error. You claim something typechecks just fine. What happens if you put #exit directly after it?

[Arien Malec]

I have it now -- I misspelled theorem as thoerem, which triggers the odd behavior.

#exit has everything typechecking fine btw. The word thoerem sends lean4 into an odd place.

[Arien Malec]

inserting the word thoerem anywhere seems to send the typechecker mad.

[Arien Malec]

That's a red herring -- any invalid word creates a strange type error -- is there an issue tracker or bug reporting system where I can post this?

[Kyle Miller]

What's happening is that thoerem is an identifier, so Lean parses Iff.intro blah blah thoerem as a function application.

I haven't thought about whether there are any problems doing so, but it would be nice to report unknown identifiers when there is another error like this.

[Kyle Miller]

With the sorry example, again it's sorry thoerem so it's trying to use sorry as a function, which Lean doesn't allow in a direct way like this.