<html><head><style>body{font-family:Helvetica,Arial;font-size:13px}</style></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div id="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;">The backtick notation can of course be defined:</div><div id="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;"><br></div><div id="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;"><br></div><div id="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;">postulate max : ℕ → ℕ → ℕ</div><div id="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;"><br></div><div id="bloop_customfont" style="margin: 0px;">_`_`_ : ∀{a b c : Set} → a → (a → b → c) → b → c</div><div id="bloop_customfont" style="margin: 0px;">a ` f ` b = f a b</div><div id="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;"><br></div><div id="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;">test = 43 ` max ` 10</div><div id="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;"><br></div><div id="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;"><br></div> ~L<br> <div class="bloop_sign" id="bloop_sign_1514129926331613184"></div> <br><p class="airmail_on">On 25 December 2017 at 2:26:08 am, Miëtek Bak (<a href="mailto:mietek@bak.io">mietek@bak.io</a>) wrote:</p> <blockquote type="cite" class="clean_bq"><span><div><div></div><div>Agda supports section notation. For example:<br><br> data Nat : Set where<br> zero : Nat<br> suc : Nat → Nat<br> {-# BUILTIN NATURAL Nat #-} -- For the literals<br><br> _+_ : Nat → Nat → Nat<br> zero + m = m<br> suc n + m = suc (n + m)<br><br> plus = _+_<br><br> postinc = _+ 1<br><br> preinc = 1 +_<br><br>In general, Agda supports mixfix operator notation. For example:<br><br> data Bool : Set where<br> true : Bool<br> false : Bool<br><br> if_then_else_ : {A : Set} → Bool → A → A → A<br> if true then x else y = x<br> if false then x else y = y<br><br> _<|_|>_ = if_then_else_<br><br>Agda’s new documentation website has a page on mixfix operators:<br>http://agda.readthedocs.io/en/latest/language/mixfix-operators.html<br><br>As far as I know, there is no equivalent to the backtick notation. Instead, we default to declaring infix operators, and then we use the full name with the underscores whenever the prefix form is required.<br><br>Using the prefix form is required to bind implicit arguments. For example:<br><br> _<|_|>'_ : {A : Set} → Bool → A → A → A<br> _<|_|>'_ {A} b x y = if_then_else_ {A} b x y<br><br>-- <br>Mietek<br><br><br>> On 24 Dec 2017, at 13:46, Peter Hancock <hancock@fastmail.fm> wrote:<br>> <br>> I have never properly learnt to use Agda's fancy notational features,<br>> except in a basic ad-hoc way, that accomplishes most of what I want. I'm<br>> not referring to unicode symbols and whatnot, but the business of making<br>> symbols by scattering '_' characters in some line-noise.<br>> <br>> I'd like some hints and tips about how to get the most out of this feature.<br>> RTFM with a pointer would be fine.<br>> <br>> Away from the keyboard, I often use some haskell-like apparatus for dealing with infix<br>> symbols. Namely:<br>> <br>> * "section notation", as in (*), (*a), (a*), where * is binary infix.<br>> Anything that avoids having to write a lambda-expression or think <br>> of a bound-variable name is great.<br>> * "backtick" notation, as in (a `foo` b), where foo is a name. Something<br>> that turns a short name into an infix symbol is great.<br>> * I very much like the notation (a <| b |> c) for "if b, then a else c"<br>> that allows three-place relations to masquerade as infix relations. <br>> <br>> How much of this can be supported or emulated with Agda's symbol-wizardry? <br>> <br>> Hank<br>> <br>> <br>> <br>> _______________________________________________<br>> Agda mailing list<br>> Agda@lists.chalmers.se<br>> https://lists.chalmers.se/mailman/listinfo/agda<br><br>_______________________________________________<br>Agda mailing list<br>Agda@lists.chalmers.se<br>https://lists.chalmers.se/mailman/listinfo/agda<br></div></div></span></blockquote></body></html>