Zulip Chat Archive
Stream: lean4
Topic: expected '{' or strict indendation
Wojciech Nawrocki (Nov 27 2022 at 04:03):
The following code broke sometime before nightly-2022-11-24. Is this the expected behaviour?
example : true := go
where go :
true := by
/- expected '{' or strict indentation -/
trivial
Last updated: Dec 20 2023 at 11:08 UTC