Skip to content

Instantly share code, notes, and snippets.

@nagat01

nagat01/proof.scala

Created September 3, 2024 09:34
Show Gist options
  • Save nagat01/1e58b6a33aed15de82840c36149d4c12 to your computer and use it in GitHub Desktop.
Save nagat01/1e58b6a33aed15de82840c36149d4c12 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
proof.scala
class Nat
case class Add(val l: Nat, val r: Nat)
extension (a: Add)
def comm = Add(a.r, a.l)
@main def main =
val n = Nat()
val m = Nat()
val el = Add(n, m)
val er = Add(m, n)
println(el.comm == er)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment