4 ms·
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.htm
by 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`.