Zulip Chat Archive
Stream: mathlib4
Topic: custom let that registers for reduction in simp
Matthew Ballard (Feb 27 2024 at 00:26):
Given the changes to simp
in core, we do want something like letR
(WIP) that registers it for use in simp
?
Yaël Dillies (Feb 27 2024 at 08:18):
(I fell off my chair answering this proposal, maybe a sign it would be a disrupting change) Would it be practically different from letI
?
Last updated: May 02 2025 at 03:31 UTC