factic

Stream: general

[Johan Commelin]

What do people think of having a fact tactic? All it does is exact fact.out _. It's just a little bit shorter, and arguably more readable.
It means that if your goals is 0 < x, and you have fact (0 < x) in your context (or it can be derived by TC), then you can close the goal with fact.

[Kevin Buzzard]

I really like the idea of being able to close a goal by saying fact. Can we make it fact!?

[Johan Commelin]

Maybe fact! should first call norm_num?

[Johan Commelin]

And fact!! can combine linarith, norm_num, and tidy?

[Johan Commelin]

fact!!! could maybe post the goal on Zulip, and pull the replies into the source code?

[Patrick Massot]

fact!!! should be able to close any goal which has ever been proved by a human being.

[Johan Commelin]

actually, a zulip tactic would be quite nice to have :grinning:

[Filippo A. E. Nuccio]

Speaking about the fact tactic, it might would be worthwhile to add the fact.out _ tactic (is it a tactic?) to the docs. What do you think?

[Eric Wieser]

Is docs#fact.out not documented?

[Filippo A. E. Nuccio]

Well, I think that what got me trapped is that I normally use the pop-up window shown by VS-Code rather than going online. And the name of the constructor does not appear there.

[Filippo A. E. Nuccio]

What appears in this case is only the doc between Wrapper around... and ..first order logic

[Notification Bot]

This topic was moved by Johan Commelin to #new members > Darren Chen