Created
October 31, 2025 11:06
-
-
Save qexat/6d3815beae18d392f873d76e01718d6a to your computer and use it in GitHub Desktop.
oh my god lexa will you ever stop defining peano integers in every language on earth a thousand times AND differently every time like seriously im starting to get worried for your mental health i mean what even is your goal with that what do you gain from it because i dont see it and look im not trying to be dismissive or anything but you could …
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| import enum | |
| import typing | |
| class Nat(enum.Enum): | |
| O = enum.auto() | |
| S = enum.auto() | |
| type nat = typing.Literal[Nat.O] | tuple[typing.Literal[Nat.S], nat] | |
| O = Nat.O | |
| def S(n: nat) -> nat: | |
| return (Nat.S, n) | |
| def add(n: nat, m: nat) -> nat: | |
| match m: | |
| case Nat.O: | |
| return n | |
| case (Nat.S, m_): | |
| return add(S(n), m_) | |
| def mul(n: nat, m: nat) -> nat: | |
| match m: | |
| case Nat.O: | |
| return O | |
| case (Nat.S, m_): | |
| return add(n, mul(n, m_)) | |
| def fact(n: nat) -> nat: | |
| match n: | |
| case Nat.O: | |
| return S(O) | |
| case (Nat.S, n_): | |
| return mul(n, fact(n_)) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment