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

need to deal with these warnings

Browse Source
This commit is contained in:
Kevin Buzzard
2023-08-05 17:18:53 +01:00
parent 5e4ee9be02
commit f821d48570
1 changed files with 7 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

7
actionable_warnings_for_Addition_world Normal file
View File

@@ -0,0 +1,7 @@
stdout:
./././Game.lean:66:0: warning: Could not find a docstring for tactic decide, consider adding one using `TacticDoc decide "some doc"`
./././Game.lean:66:0: warning: No world introducing MyNat.add_succ, but required by Tutorial
./././Game.lean:66:0: warning: No world introducing MyNat.two_eq_succ_one, but required by Addition
./././Game.lean:66:0: warning: No world introducing MyNat.add_succ, but required by Addition
./././Game.lean:66:0: warning: No world introducing nth_rewrite, but required by Addition
./././Game.lean:66:0: warning: No world introducing MyNat.three_eq_succ_two, but required by Addition