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: May 02 2025 at 03:31 UTC