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: Dec 20 2025 at 21:32 UTC