website/content/2024-02-21-norm-cast.md

713 B

title date summary
norm_cast was upstreamed to Lean4 2024-02-21 I am now a contributor to Lean!

In 2019, I was an intern at Matryoshka in Amsterdam. There, I worked with Robert Y. Lewis on a tactic for the Lean prover called norm_cast. The goal was to reduce the frustration of mathematicians when working with expressions containing casts and coercions. This work was merged into Mathlib and even led to the writing of a paper.

Well, after a brief transit in Lean's standard library, the tactic was merged yesterday into the core language!