Zulip Chat Archive Stream: lean4 Topic: Using let rec in expansion produces error Joseph O (May 20 2022 at 15:55): Any ideas? Last updated: Feb 28 2026 at 14:05 UTC