Stream: new members
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.
Kenny Lau (Nov 25 2018 at 23:36):
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