forked from leanprover-community/NNG4
-
Notifications
You must be signed in to change notification settings - Fork 0
/
TODO.txt
7 lines (7 loc) · 620 Bytes
/
TODO.txt
1
2
3
4
5
6
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