show error on duplicated level number

2023-10-07 21:03:44 +02:00
parent c50517b5e6
commit 6e046d72b6
2 changed files with 11 additions and 3 deletions
@@ -13,8 +13,11 @@ Level 1
 Statement foo.bar : 5 ≤ 7 := by
  simp

-- Shows warning on `foo.bar₂`:
+Game "Test"
+World "TestW"
+Level 2 -- should warn if set to `1`

+-- Shows warning on `foo.bar₂`:
 Statement foo.bar2 : 3 ≤ 7 := by
  simp