More useful links about surreal numbers in Lean

Changes

1 changed files (+4/-0)

• Surreal.lean
  • @@ -1,6 +1,10 @@
    import Mathlib -- Based on Knuth's book "Surreal Numbers" + -- https://github.com/oersted/lean-surreal-numbers is incomplete but has some helpful stuff + -- https://leanprover-community.github.io/archive/stream/113489-new-members/topic/defining.20surreal.20numbers.html + -- https://leanprover-community.github.io/archive/stream/217875-Is-there-code-for-X%3F/topic/Surreal.20numbers.html + -- Also, mathlib4 and https://github.com/vihdzp/combinatorial-games/ both have implementations of surreal numbers -- Apparently using Set instead of List here can cause paradoxes -- Which is a bit sad since this definition can't have infinite lists