APL style notation for Lean

Stream: general

[suhr]

I would like to add some bits of APL notation in Lean. So I tried to do the following:

notation f "⌿" => List.foldl f

#reduce (Nat.add⌿) 0 [1,2,3]

But I would like to achieve this:

#reduce Nat.add⌿ 0 [1,2,3]
#reduce +⌿ 0 [1,2,3]

So I have the following questions:

• How to make ⌿ to bind more tightly, so parenthesis around Nat.add⌿ would be unnecessary?
• How define a specific syntax for the case when there's an operator at the left of ⌿?

[Kyle Miller]

notation:max f:max "⌿" => List.foldl f

#check Nat.add⌿ 0 [1,2,3]

[suhr]

Thanks. Is it possible to specialize it for +⌿ 0 [1,2,3] as well?

[Edward van de Meent]

no, i don't think so. you'd at the very least need to specify (·+·)

[Edward van de Meent]

also note that there exists postfix, i.e. the following works:

postfix :max "⌿" => List.foldl

#check (·+·)⌿

[Kyle Miller]

Yeah, postfix is a good choice for this (idiomatically I think it's postfix:max, no space). It's worth knowing that postfix is a macro for notation, so its benefit is that you don't have to write f:max.