greg/NNG
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

these need fixing before we can merge to master

Browse Source
This commit is contained in:
Kevin Buzzard
2023-10-14 22:35:44 +01:00
parent d3ffdb507b
commit 63ed90139d
1 changed files with 7 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

7
TODO.txt Normal file
View File

@@ -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