Zulip Chat Archive

Stream: new members

Topic: assumption?

Nicolò Cavalleri (Jul 09 2020 at 15:15):

Is there anything like assumption?? I mean when you have a lot of hypotheses see if assumption closes the goal and then know with what hypothesis?

Jalex Stark (Jul 09 2020 at 15:22):

we tried to make this in lean#281 and got stuck, something about writing the tests

Jalex Stark (Jul 09 2020 at 15:23):

gabriel noted that there might be a way to implement this in mathlib instead of in lean

Nicolò Cavalleri (Jul 09 2020 at 15:46):

Ok thanks!

Last updated: Dec 20 2023 at 11:08 UTC