Definition of or.rec

Stream: new members

[Steven Ulin]

o/ Hi yall, I'm new to theorem proving and I've been having lots of fun learning lean! I've been using the source code as a guide of best practices.

qq regarding or.rec:

• what does rec stand for?
• where is it defined in the codebase? I cannot find it in init/logic.lean
• should this function only be used by lean's implementers?

Thanks yall!

[Yakov Pechersky]

rec stands for recursor. It is generated automatically for any inductive type. It can be used by anyone! It is the most powerful statement about any inductive type, and the underlying way anything about that inductive type can be proven. But you'd like want to use the rest of the or API developed. You might want to read:
https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html, sections 7 and 8
https://xenaproject.wordpress.com/2021/04/03/induction-and-inductive-types/