2024-02-21 09:49:37 +00:00
|
|
|
---
|
|
|
|
|
title: "norm_cast was upstreamed to Lean4"
|
|
|
|
|
date: 2024-02-21
|
|
|
|
|
summary: I am now a contributor to Lean!
|
|
|
|
|
---
|
|
|
|
|
|
|
|
|
|
In 2019, I was an intern at [Matryoshka](https://matryoshka-project.github.io/)
|
|
|
|
|
in Amsterdam. There, I worked with [Robert Y. Lewis](https://robertylewis.com/)
|
|
|
|
|
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
|
2024-02-21 09:50:55 +00:00
|
|
|
coercions. This work was merged into
|
|
|
|
|
[Mathlib](https://github.com/leanprover-community/mathlib4) and even led to the
|
|
|
|
|
writing of a [paper](https://arxiv.org/abs/2001.10594).
|
2024-02-21 09:49:37 +00:00
|
|
|
|
|
|
|
|
Well, after a brief transit in Lean's standard library, the tactic was
|
|
|
|
|
[merged](https://github.com/leanprover/lean4/pull/3322) yesterday into the core
|
|
|
|
|
language!
|
