Zulip Chat Archive

Stream: new members

Topic: Using emoji as a synonym for a function


Malcolm Langfield (Nov 22 2023 at 14:31):

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 (Nov 22 2023 at 14:32):

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

Malcolm Langfield (Nov 22 2023 at 14:35):

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

Yaël Dillies (Nov 22 2023 at 14:41):

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

Malcolm Langfield (Nov 22 2023 at 14:43):

Sure, sure, apologies!

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

Here's the most naive version.

Yaël Dillies (Nov 22 2023 at 14:53):

This works

import Mathlib.Data.Finmap

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

abbrev «🔎» := Finmap.lookup a s

#check «🔎» a s

Malcolm Langfield (Nov 22 2023 at 14:54):

Oh my gosh! Thank you so much!

Malcolm Langfield (Nov 22 2023 at 14:54):

:heart: :heart: :heart:

Eric Rodriguez (Nov 22 2023 at 14:54):

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

Kyle Miller (Nov 22 2023 at 14:54):

I'd expect this to work:

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

Yongyi Chen (Nov 22 2023 at 14:57):

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 (Nov 22 2023 at 14:57):

Indeed, this works

import Mathlib.Data.Finmap

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

notation "🔎" => Finmap.lookup

#check 🔎 a s

Last updated: Dec 20 2023 at 11:08 UTC