Topic: induction on fin
Albert ten Napel (Sep 09 2020 at 10:07):
I see a nice definition of fin in terms of a structure here: https://github.com/leanprover/lean/blob/master/library/init/data/fin/basic.lean . But where is induction on this fin defined?
Rob Lewis (Sep 09 2020 at 10:11):
Are you looking for docs#fin.succ_rec ?
Albert ten Napel (Sep 09 2020 at 10:15):
Last updated: May 14 2021 at 04:22 UTC