Zulip Chat Archive

Stream: general

Topic: fact


view this post on Zulip Jeremy Avigad (May 08 2020 at 22:57):

I just learned that fact doesn't mean factorial in Lean, and if nat is open, #check fact is ambiguous. Doesn't that seem unfortunate?

view this post on Zulip Simon Hudon (May 09 2020 at 02:46):

It's a new design in mathlib. It's actually not a shorthand for anything but it helps us have propositions as type classes. We could put it in its own namespace to minimize this kind of surprise

view this post on Zulip Johan Commelin (May 09 2020 at 03:00):

I agree that it is a bit unfortunate. @Jeremy Avigad I usually write n.fact to get around this, and it also reads nice. Even better would be to add

localized "postfix `!` := nat.fact" in nat

To the data/nat/fact file. (Modulo trivial typos). Then we can simply write n! after open_locale nat.

view this post on Zulip Reid Barton (May 09 2020 at 03:02):

We could also rename nat.fact to nat.factorial

view this post on Zulip Johan Commelin (May 09 2020 at 03:06):

I think we should do all of those (-;

view this post on Zulip Kevin Buzzard (May 09 2020 at 07:08):

I'm fine with factorial, it's unambiguous. Mathematicians have this great notation ! for it though :-) How about getting that working then nobody needs to worry about the name :-)

view this post on Zulip Chris Hughes (May 09 2020 at 07:57):

The lemmas still use the name.

view this post on Zulip Patrick Massot (May 09 2020 at 09:03):

I think it makes sense that fact is the abbreviation of the word fact instead of the abbreviation of the word factorial.

view this post on Zulip Gabriel Ebner (May 09 2020 at 09:07):

There are other reasonable synonyms for fact: given or assuming come to mind quickly. But there aren't that many other names for factorial, and n.factorial is quite a bit longer than n.fact. Though the postfix notation also looks nice.

view this post on Zulip Mario Carneiro (May 09 2020 at 09:19):

In fact, fact is one of those "filler" words that conveys little meaning here. Why not something like to_typeclass that says something more informative?

view this post on Zulip Scott Morrison (May 09 2020 at 11:18):

[witness P]?

view this post on Zulip Reid Barton (Aug 30 2020 at 16:52):

What's the story with global instances of fact? I was under the vague impression that there weren't supposed to be any, but some do exist.

view this post on Zulip Ruben Van de Velde (Aug 30 2020 at 19:05):

My understanding was "don't make too many", rather than "don't many any at all"

view this post on Zulip Floris van Doorn (Aug 30 2020 at 21:28):

I prefer to only have local(ized) instances, but I'm also fine with the looser "don't have many"

view this post on Zulip Scott Morrison (Aug 31 2020 at 01:06):

I feel like this is something we could easily regret later. I'd vote for "none, unless they come with a detailed doc-string explaining exactly why local attribute [instance] won't cut it".

view this post on Zulip Scott Morrison (Aug 31 2020 at 01:06):

Ideally enforced by the linter! :-)


Last updated: May 08 2021 at 10:12 UTC