## Stream: lean4

### Topic: Custom identifiers?

#### Mac (Apr 13 2021 at 22:03):

When trying to define Haskell-like operator identifiers I encountered the following error:

syntax "(~)" : ident
-- unknown category 'ident'


Is there some reason why ident is not a proper syntax category? I would like to able to do something akin the following:

syntax "(~)" : ident
infix:50 " ~ " => $(Lean.mkIdent (~)) def trans (A : Sort _) ((~) : A -> A -> Prop) (a b c : A) := a ~ b -> b ~ c -> a ~ c  #### Sebastian Ullrich (Apr 14 2021 at 07:06): An intriguing idea. What I don't quite like about it is that you need an unhygienic macro for it, and you need to do it for each operator separately. I'd rather like to have a general mechanism a la (infix "~" : A -> A -> Prop)  #### Mario Carneiro (Apr 14 2021 at 08:03): Oh no we're turning into agda #### Sebastian Ullrich (Apr 14 2021 at 08:53): Actually it's not clear to me whether Agda allows local mixfix notations (@Jakob von Raumer ?) A type name, function name, or constructor name can comprise one or more name parts if we separate them with underscore characters _, and the resulting name can be used as an operator. #### Jakob von Raumer (Apr 14 2021 at 08:54): What do you mean by "local"? #### Sebastian Ullrich (Apr 14 2021 at 08:55): For a let- or lambda-bound function as above #### Jannis Limperg (Apr 14 2021 at 08:58): Yeah, no problem. data ⊤ : Set where tt : ⊤ stuff : ⊤ stuff = let _//_ : ⊤ → ⊤ → ⊤ x // y = tt in (tt ~ tt + tt) // tt where _~_+_ : ⊤ → ⊤ → ⊤ → ⊤ x ~ y + z = tt  Works with lambda binders as well. #### Jakob von Raumer (Apr 14 2021 at 08:58): foo : (X : Set)(x : X) → Set foo X x = let _~_ = λ (x y : X) → X in x ~ x  #### Sebastian Ullrich (Apr 14 2021 at 08:59): Nice. I would have been surprised if it didn't work, but the docs quoted above seemed relatively specific. #### Jakob von Raumer (Apr 14 2021 at 08:59): Agda has the same rules for every sort of identifier, be it constructor, definition, ... #### Sebastian Ullrich (Apr 14 2021 at 09:00): I guess it's still a "function name" #### Jakob von Raumer (Apr 14 2021 at 09:02): I mean, the Lean community seems pretty dismissive about mixfix as theorem names, which I get, but mixfix variable seem to have some good use cases too #### Mario Carneiro (Apr 14 2021 at 09:03): I just don't think that notations should be the actual canonical names of things #### Mario Carneiro (Apr 14 2021 at 09:04): I think local notations (like literally local to an expression) are a fine way to address this use case #### Jakob von Raumer (Apr 14 2021 at 09:05): But isn't the reasoning behind that the same as the reasoning why a "thing" shouldn't be just named with a single letter and we do that all the time locally? #### Mario Carneiro (Apr 14 2021 at 09:06): For that, I think a macro expansion to name the identifier something inaccessible and let you supply the mixfix notation would be ideal #### Mario Carneiro (Apr 14 2021 at 09:07): but the grammar of identifiers shouldn't need to change to support this #### Mac (Apr 14 2021 at 23:43): Sebastian Ullrich said: An intriguing idea. What I don't quite like about it is that you need an unhygienic macro for it, and you need to do it for each operator separately. I'd rather like to have a general mechanism a la (infix "~" : A -> A -> Prop)  I fully support this idea! However, this does could restrict the kinds of notation you can locally bind. For example, this would likely not allow for local binding of lambda-like macros (akin to forall/exists/sigma, etc.). #### Mac (Apr 14 2021 at 23:53): Mario Carneiro said: I just don't think that notations should be the actual canonical names of things Mario Carneiro said: For that, I think a macro expansion to name the identifier something inaccessible and let you supply the mixfix notation would be ideal You can already do both of these. For the unlikely to access approach: infix:50 " ~ " =>$(Lean.mkIdent «~»)
def trans (A : Sort _) («~» : A -> A -> Prop) (a b c : A) := a ~ b -> b ~ c -> a ~ c


For the standard naming approach:

#### Sebastian Ullrich (Apr 15 2021 at 07:20):

Mac said:

I fully support this idea! However, this does could restrict the kinds of notation you can locally bind. For example, this would likely not allow for local binding of lambda-like macros (akin to forall/exists/sigma, etc.).

Yes, it will need cooperation from each macro's parser at least. But if we can do it for built-in syntax, it will also be possible for any user-defined one.

Last updated: May 07 2021 at 12:15 UTC