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 2023 at 11:08 UTC