leanprover-community / mathport

Mathport is a tool for porting Lean3 projects to Lean4
Apache License 2.0
41 stars 15 forks source link

refactor: use Parse1 alias to prevent parse errors #185

Closed digama0 closed 1 year ago

digama0 commented 1 year ago

Because user commands and attributes only have one parser invocation, they always parse all their arguments in a tuple, unlike tactics which have several parser invocations. To prevent issues where we call the parser multiple times or zero times, we use the Parse1 alias whose constructor encourages exactly one call to parse.