Using emoji as a synonym for a function

Stream: new members

[Malcolm Langfield]

Hello, I'd like to name a function with an emoji (i.e. the magnifying glass for Finmap.lookup), or something like this. The parser is not happy about this, and I've tried various other strategies, like writing notation for a prefix operator, or writing an elaborator. I've had no luck.

I was able to get the notation approach to work for unary functions, but anything that wants more than 1 argument requires parentheses to get the precedence to work out, which is a bit disappointing.

#check ((🔎 var) s)

Anyone know how to do this? :sweat_smile:

[Yaël Dillies]

Have you tried enclosing everything in french quotes? «», typed \f<<>>.

[Malcolm Langfield]

Sorry, what do you mean by everything? Can you give a full example?

[Yaël Dillies]

Well, can you give an example of what you tried?

[Malcolm Langfield]

Sure, sure, apologies!

import Mathlib.Data.Finmap
notation:65 "🔎 " var s => Finmap.lookup var s

Here's the most naive version.

[Yaël Dillies]

This works

import Mathlib.Data.Finmap

variable {α : Type*} {β : α → Type*} [DecidableEq α] (a : α) (s : Finmap β)

abbrev «🔎» := Finmap.lookup a s

#check «🔎» a s

[Malcolm Langfield]

Oh my gosh! Thank you so much!

[Malcolm Langfield]

:heart: :heart: :heart:

[Eric Rodriguez]

Having to use the French quotes after declaring the abbrev is a crummy workaround :/

[Kyle Miller]

I'd expect this to work:

import Mathlib.Data.Finmap
notation "🔎" => Finmap.lookup

[Yongyi Chen]

I was experimenting with that! It looks like `notation:##`` doesn't work except when ## is the maximum (1024). So it looks like no ## is a synonym for max, is that right? And what are best practices regarding doing that? (Obviously in this case, max is the only option.)

[Yaël Dillies]

Indeed, this works

import Mathlib.Data.Finmap

variable {α : Type*} {β : α → Type*} [DecidableEq α] (a : α) (s : Finmap β)

notation "🔎" => Finmap.lookup

#check 🔎 a s