leanprover-community / mathport

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

fix: truncate precedence to 1024 #115

Closed gebner closed 2 years ago

gebner commented 2 years ago

Fixes #114.

digama0 commented 2 years ago

What about max_plus? That is also 1025 AFAIK.

gebner commented 2 years ago

That's an "unsupported advanced precedence syntax", and is translated to 999...

gebner commented 2 years ago

If it were parsed correctly, it would be translated to :max which would work.

gebner commented 2 years ago

Fix accidentally pushed to master instead.