Zulip Chat Archive

Stream: lean4

Topic: array and list notation

Dean Young (Mar 05 2023 at 03:37):

How does one make their own list or array notation in lean 4?

Adam Topaz (Mar 05 2023 at 04:10):

The notation for lists is implemented starting here:
https://github.com/leanprover/lean4/blob/3b50410ec0a8b83344d0f61df554a1024bdaf298/src/Init/Notation.lean#L474

Dean Young (Mar 05 2023 at 06:17):

wasn't there something to do with foldr?

Reid Barton (Mar 05 2023 at 06:20):

Like https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Fin/VecNotation.lean#L68?

Reid Barton (Mar 05 2023 at 06:21):

That's a mathlib4 command notation3

Dean Young (Mar 05 2023 at 06:27):

thanks that was it!

Last updated: Dec 20 2023 at 11:08 UTC