Zulip Chat Archive
Stream: new members
Topic: Symbol minus
Martin Dvořák (Feb 27 2022 at 15:12):
Does the symbol − (minus) already have a meaning in lean/mathlib?
Kevin Buzzard (Feb 27 2022 at 15:18):
You're talking about \minus?
import all
#print notation − -- unexpected token
That's a good start! Searching mathlib in VS Code gives 15 results but they are all in docstrings (and probably should be fixed)
Martin Dvořák (Feb 27 2022 at 15:22):
Thanks a lot! I have just learnt two new commands from your two-line-long code!
Kevin Buzzard (Feb 27 2022 at 15:25):
Kevin Buzzard (Feb 27 2022 at 15:26):
You can make the all file I'm importing by running ./scripts/mk_all.sh.
Martin Dvořák (Feb 27 2022 at 15:39):
OK, great! I will use minus for the complement of a language.
Notification Bot (Feb 27 2022 at 15:43):
Martin Dvořák has marked this topic as resolved.
Eric Wieser (Feb 27 2022 at 15:47):
Have you considered just using docs#has_compl?
Martin Dvořák (Feb 27 2022 at 15:49):
It seems that has_compl is not defined on computability.language unless I am mistaken.
Martin Dvořák (Feb 27 2022 at 15:50):
Martin Dvořák (Feb 27 2022 at 15:52):
Or, would you suggest adding it there? Alongside with has_subset and has_inter probably.
Eric Wieser (Feb 27 2022 at 15:52):
My point is that if the semantics are similar (I don't know if they are) then it would be reasonable to reuse existing notation
Martin Dvořák (Feb 27 2022 at 15:53):
Should I add it to mathlib, or just to my project?
Eric Wieser (Feb 27 2022 at 15:54):
It looks like it does already have a has_compl instance
Martin Dvořák (Feb 27 2022 at 15:54):
In which file is has_compl added to computability.language please?
Eric Wieser (Feb 27 2022 at 15:54):
Via docs#language.complete_boolean_algebra
Eric Wieser (Feb 27 2022 at 15:55):
Which is defined by the line you just linked to!
Martin Dvořák (Feb 27 2022 at 15:55):
Oh, sorry. Thanks for telling me!
Eric Wieser (Feb 27 2022 at 15:56):
Does that complement mean the same thing as the one you're talking about?
Martin Dvořák (Feb 27 2022 at 15:59):
Yes, exactly!
Martin Dvořák (Feb 27 2022 at 16:01):
Why cannot I compile this code then?
import computability.language
example (K L : language char) : K ∩ L = L ∩ K :=
sorry
Martin Dvořák (Feb 27 2022 at 16:01):
It says:
failed to synthesize type class instance for
K L : language char
⊢ has_inter (language char)
Notification Bot (Feb 27 2022 at 16:01):
Martin Dvořák has marked this topic as unresolved.
Last updated: Dec 20 2023 at 11:08 UTC