Zulip Chat Archive
Stream: lean4
Topic: custom indexing
Adam Nemecek (Mar 24 2023 at 22:43):
is it possible to implement indexing for a type?
Henrik Böving (Mar 24 2023 at 23:02):
If you are referring to the array index operator yes you can use docs4#GetElem
Adam Nemecek (Mar 25 2023 at 02:38):
(deleted)
Adam Nemecek (Mar 25 2023 at 03:16):
(deleted)
Last updated: Dec 20 2023 at 11:08 UTC