Zulip Chat Archive

Stream: general

Topic: inductionI?

Patrick Massot (Aug 08 2019 at 20:24):

Should we have an inductionI tactic to avoid things like https://github.com/leanprover-community/lean-sensitivity/blob/lean-3.4.2/src/sensitivity.lean#L95-L97 which reads really weird?

Chris Hughes (Aug 08 2019 at 20:59):

A nicer way of writing that is with induction and resetI.

Patrick Massot (Aug 08 2019 at 21:23):

Git blames Reid

Reid Barton (Aug 09 2019 at 17:55):

I can never get the hang of induction

Last updated: Dec 20 2023 at 11:08 UTC