From 63ed90139d36484b775bf08fdd1be0c959c89efd Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sat, 14 Oct 2023 22:35:44 +0100 Subject: [PATCH] these need fixing before we can merge to master --- TODO.txt | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 TODO.txt diff --git a/TODO.txt b/TODO.txt new file mode 100644 index 0000000..5459682 --- /dev/null +++ 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