## Stream: general

### Topic: fact

#### 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?

#### 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

#### 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.

#### Reid Barton (May 09 2020 at 03:02):

We could also rename nat.fact to nat.factorial

#### Johan Commelin (May 09 2020 at 03:06):

I think we should do all of those (-;

#### 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 :-)

#### Chris Hughes (May 09 2020 at 07:57):

The lemmas still use the name.

#### 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.

#### 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.

#### 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?

#### Scott Morrison (May 09 2020 at 11:18):

[witness P]?

#### 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.

#### 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"

#### 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"

#### 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".

#### Scott Morrison (Aug 31 2020 at 01:06):

Ideally enforced by the linter! :-)

Last updated: May 08 2021 at 10:12 UTC