Zulip Chat Archive

Stream: new members

Topic: classes

Lucas (Jan 20 2022 at 03:13):

Hi, I am trying to formalize some (basic) theorems about prime numbers, and the definition includes the definition irreducible, which appears to be a class. I don't know anything about classes in lean, and the lean reference manual 4.10 just links to some 1994 paper and that's it. Where is documentation about classes in lean, and how do you use irreducible p in a proof?

Alex J. Best (Jan 20 2022 at 03:16):

Check out https://leanprover.github.io/theorem_proving_in_lean/type_classes.html, its quite often a more helpful resource than the reference manual.

Lucas (Jan 20 2022 at 03:18):

cool, this looks like exactly what I was looking for

Last updated: Dec 20 2023 at 11:08 UTC