these need fixing before we can merge to master

leanprover-community · Oct 14, 2023 · 63ed901 · 63ed901
1 parent d3ffdb5
commit 63ed901
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/TODO.txt b/TODO.txt
@@ -0,0 +1,7 @@
+./././Game.lean:106:0: warning: No world introducing right, but required by LessOrEqual
+./././Game.lean:106:0: warning: No world introducing MyNat.succ, but required by LessOrEqual
+./././Game.lean:106:0: warning: No world introducing left, but required by LessOrEqual
+./././Game.lean:106:0: warning: No world introducing MyNat.rfl, but required by LessOrEqual
+./././Game.lean:106:0: warning: No world introducing rcases, but required by LessOrEqual
+./././Game.lean:106:0: warning: No world introducing change, but required by LessOrEqual
+./././Game.lean:106:0: warning: No world introducing sorry, but required by Power