Zulip Chat Archive

Stream: general

Topic: mono and ac_mono in the nursery


Simon Hudon (Aug 22 2018 at 17:07):

My mono and ac_mono are, I believe, ready for use. I have put them in the nursery https://github.com/leanprover-community/mathlib-nursery so that people can try them out as I get them merged into mathlib.

Patrick Massot (Aug 22 2018 at 19:42):

Why is there so much meta and lemmas in the test file? Is it meant to be part of mathlib?

Simon Hudon (Aug 22 2018 at 19:44):

It is. It's meant to test individual parts of the tactics. Maybe I should split it into test and example

Patrick Massot (Aug 22 2018 at 19:44):

I see

Patrick Massot (Aug 22 2018 at 19:46):

I always find it hard to read your examples or tests which actually don't prove anything, either because the announced statement is true or because it ends with admit

Patrick Massot (Aug 22 2018 at 19:48):

Where is monotonicity when the target is an equality as in https://github.com/leanprover-community/mathlib-nursery/blob/master/test/tactic/monotonicity.lean#L326?

Simon Hudon (Aug 22 2018 at 19:49):

In that case, monotonicity is a generalization of congr

Patrick Massot (Aug 22 2018 at 19:50):

Maybe you could explain that in the documentation (and add a couple of example there too)

Patrick Massot (Aug 22 2018 at 19:51):

It looks very useful

Simon Hudon (Aug 22 2018 at 19:52):

I see what you mean with true. I state those theorems using suffices : x * y < w * z, trivial, just so that I don't have to complete all the proofs. I could use assumptions instead of guard_target maybe , that would be clearer

Simon Hudon (Aug 22 2018 at 19:53):

Thanks for the advice, I'll try to select the ones that illustrate best the obvious use cases

Simon Hudon (Aug 22 2018 at 19:56):

It looks very useful

I'm hoping it will be. Please report any trouble you run across, I feel like I must have overlooked lots of cases and lots of lemmas.

Patrick Massot (Aug 22 2018 at 20:00):

Unfortunately I don't think any of my current projects will need this, but certainly I will need it at some point.


Last updated: Dec 20 2023 at 11:08 UTC