Zulip Chat Archive
Stream: mathlib4
Topic: Squash, Trunc
Eric Rodriguez (Dec 20 2023 at 00:26):
Why do we have the both of these? docs#Squash, docs#Trunc
Eric Wieser (Dec 20 2023 at 00:53):
The latter was ported from lean3's docs3#trunc
Eric Wieser (Dec 20 2023 at 00:54):
I guess lean 4 core independently decided it wanted this and invented a different name
Eric Rodriguez (Dec 20 2023 at 01:08):
I guess it's worth deduplicating, right?
Kevin Buzzard (Dec 20 2023 at 01:16):
My impression from talking to agda users is that trunc is a standard name? :-/
Scott Morrison (Dec 20 2023 at 02:30):
Squash is not used in Lean outside of a single test. It might be reasonable to simply remove it from Lean.
Scott Morrison (Dec 20 2023 at 02:30):
This feels like something that belongs in Std.
Last updated: Dec 20 2023 at 11:08 UTC