Gabriel Ebner

Notations no longer work in binport

4

Like ≅+* or ℝ

Extreme runtime increase

8

The latest timeouts don't seem to be caused by a simple infinite loop. It's just that many files now take a *lot* longer than they used to. For example here...

Translate coe constants

5

That is, translate `coe` to `(↑ ⬝)`. And `coeFn` to `(· ·)`.

`tt` is sometimes not translated

1

Mathlib (data/nat/basic): ```lean @[simp] lemma bodd_bit1 (n) : bodd (bit1 n) = tt := bodd_bit tt n ``` Synport: ```lean @[simp] theorem bodd_bit1 (n) : bodd (bit1 n) = tt...

dot-notation is often omitted

1

Lean 3: ```lean /-- Matches one out of a list of characters. -/ def one_of (cs : list char) : parser char := decorate_errors (do c ← cs, return c.to_string)...

Synport: ```lean namespace Bool theorem coe_sort_tt : coeSort.{1, 1} true = True := coe_sort_tt ``` In Lean 3 `coe_sort_tt` would resolve to `_root_.coe_sort_tt` resulting in a non-recursive alias definition. But...

Translate local notation with `(priority := high)`

3

This is closer to the Lean 3 semantics.

Impossible `intermediate_field.adjoin` notation

1

Lean 3: ```lean notation K`⟮`:std.prec.max_plus l:(foldr `, ` (h t, insert.insert t h) ∅) `⟯` := adjoin K l lemma induction2 {α β γ : solvable_by_rad F E} (hγ :...

For example the unit interval `I` is global notation in the binport. This breaks the variable declaration `(I : ModelWithCorners 𝕜 E H)` in `Geometry.Manifold.Mfderiv`.