chore: updates for new versions #251
Annotations
4 errors
|
Prose linter:
_out/html-vale/Notations-and-Macros/index.html#L1194
[vale] reported by reviewdog 🐶
[Lean.Spelling] Did you really mean 'declaratively'?
Raw Output:
{"message": "[Lean.Spelling] Did you really mean 'declaratively'?", "location": {"path": "_out/html-vale/Notations-and-Macros/index.html", "range": {"start": {"line": 1194, "column": 385}}}, "severity": "ERROR"}
|
|
Prose linter:
_out/html-vale/Notations-and-Macros/Macros/index.html#L1228
[vale] reported by reviewdog 🐶
[Lean.Spelling] Did you really mean 'macro_rules'?
Raw Output:
{"message": "[Lean.Spelling] Did you really mean 'macro_rules'?", "location": {"path": "_out/html-vale/Notations-and-Macros/Macros/index.html", "range": {"start": {"line": 1228, "column": 5}}}, "severity": "ERROR"}
|
|
Prose linter:
_out/html-vale/Tactic-Proofs/The-Tactic-Language/index.html#L1442
[vale] reported by reviewdog 🐶
[Lean.Spelling] Did you really mean 'optConfig'?
Raw Output:
{"message": "[Lean.Spelling] Did you really mean 'optConfig'?", "location": {"path": "_out/html-vale/Tactic-Proofs/The-Tactic-Language/index.html", "range": {"start": {"line": 1442, "column": 129}}}, "severity": "ERROR"}
|
|
Prose linter
Vale and reviewdog exited with status code: 1
|
Loading