3 ms·

It's almost exactly smalltalk (circa 1980 or so) notation.

• Peaker 12y ago
  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 :)
  • beagle3 12y ago
    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.
• chriswarbo 12y ago
  Maude also allows mixfix like Agda. There's an interesting example in the manual ( http://maude.cs.uiuc.edu/maude1/manual/maude-manual-html/maude-manual_31.html 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`.