How to specify implicit arguments for infix operators?

user_5986907 0
Viewed 107

Suppose I have an operator

infixl 9 @@

(@@) : Tensor [S n] t -> Tensor (S n :: tail) t -> Tensor tail t

(where Tensor takes a Vect and a type, but that's not important here). If I want to specify tail, I know that I can add to a @@ b by turning @@ into a function (@@) like

(@@) {tail=[]} a b

but that somewhat defeats the point of it being infix. What's idiomatic?

infix-operator idris implicit
2 Answers

You could try using a postfix projection operator:

(.f) : Tensor [S n] t -> Tensor (S n :: tail) t -> Tensor tail t

a.f {tail=[]} b
user_63692760

You can use

let (@@) = (@@) {tail=[]} in a @@ b

which is a little long but keeps the syntax

user_59869070
Related