search

leanprover-community / mathport

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

Dropped notation #188

Closed PatrickMassot closed 2 years ago

PatrickMassot commented 2 years ago

In algebra.abs there is a line notation `|`a`|` := abs a that was completely dropped by mathport.

gebner commented 2 years ago

This is on purpose. The |a| notation causes extreme issues with parsing (since they're now used much more). See leanprover-community/mathlib4#307

Once we have decided on a new notation, we can change mathport to produce it.

Closed as duplicate of leanprover-community/mathlib4#307