From dab9187323eaaca0cfae7b3c20d62f1994a179f6 Mon Sep 17 00:00:00 2001 From: Paul-Nicolas Madelaine Date: Wed, 21 Feb 2024 10:49:37 +0100 Subject: [PATCH] new post: "norm_cast was upstreamed to Lean4" --- content/2024-02-21-norm-cast.md | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 content/2024-02-21-norm-cast.md diff --git a/content/2024-02-21-norm-cast.md b/content/2024-02-21-norm-cast.md new file mode 100644 index 0000000..0ad6741 --- /dev/null +++ b/content/2024-02-21-norm-cast.md @@ -0,0 +1,16 @@ +--- +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 +coercions. This work was merged into Mathlib and even led to the writing of a +[paper](https://arxiv.org/abs/2001.10594). + +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!