Maude also allows mixfix like Agda.

There's an interesting example in the manual ( http://maude.cs.uiuc.edu/maude1/manual/maude-manual-html/mau... ) where juxtaposition is defined as an operation, specifically:

    op __ : Bits Bits -> Bits [assoc] .

The underscores are placeholders for arguments, just like in Agda, but there's no name defined! Since `0` and `1` are defined as constructors of `Bit` (which is a sub-type of `Bits`) this will parse values like `0101010` as `Bits`.

Agda mixfix supports things like:

    [ foo ]
    bar !
    ! baz

etc.

It also supports precedence parsing.

I don't Smalltalk can do all of these.

Smalltalk, unlike Agda, can probably omit the spacing around operators, though, while Agda can't :)

I probably should look more closely at Agda.

But the if_then_else_ example is basically smalltalk equivalant - although I suspect Agda will be able to do without the angle brackets that Smalltalk often needs in these cases.