Zulip Chat Archive

Stream: new members

Topic: Getting stuff out of a definition using dite

view this post on Zulip Alexandru-Andrei Bosinta (Nov 25 2018 at 23:34):

How do I use a definition that uses dite? All my attempts of writing the definition, it's required arguments followed by a proof of the if condition failed, with Lean giving me an error like it had no idea what I was trying to do.

view this post on Zulip Kenny Lau (Nov 25 2018 at 23:36):

dif_pos / dif_neg

view this post on Zulip Kevin Buzzard (Nov 26 2018 at 08:24):

in tactic mode perhaps split_ifs can also help.

Last updated: May 06 2021 at 22:13 UTC