Zulip Chat Archive
Stream: triage
Topic: issue #18010: `(a :: l ++ [b]).last'` does not simplify t...
Random Issue Bot (Jul 11 2023 at 14:08):
Today I chose issue 18010 for discussion!
(a :: l ++ [b]).last' does not simplify to some b
Created by @Jineon Baek (@jcpaik) on 2022-12-24
Labels:
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Aug 13 2023 at 14:07):
Today I chose issue 18010 for discussion!
(a :: l ++ [b]).last' does not simplify to some b
Created by @Jineon Baek (@jcpaik) on 2022-12-24
Labels:
Is this issue still relevant? Any recent updates? Anyone making progress?
Eric Rodriguez (Aug 13 2023 at 14:39):
In Lean4 this simplifies to ⊢ List.last' (l ++ [b]) = some b, which is better but still not the best!
Eric Rodriguez (Aug 13 2023 at 14:49):
oh, supposedly last' is deprecated, but getLast? seems weird...
Last updated: Dec 20 2023 at 11:08 UTC