Zulip Chat Archive
Stream: new members
Topic: vector index not inferred
Alok Singh (Mar 05 2025 at 04:21):
#eval #v[1, 2][0] fails but #eval #[1, 2][0] works.
Sebastian Ullrich (Mar 05 2025 at 08:08):
It works fine in all versions on https://live.lean-lang.org
Last updated: May 02 2025 at 03:31 UTC