From 4d325c4e294b0a465f08e86b42ca07c8f4ea2038 Mon Sep 17 00:00:00 2001 From: Paul-Nicolas Madelaine Date: Wed, 21 Feb 2024 10:50:55 +0100 Subject: [PATCH] add link to mathlib --- content/2024-02-21-norm-cast.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/content/2024-02-21-norm-cast.md b/content/2024-02-21-norm-cast.md index 0ad6741..aede070 100644 --- a/content/2024-02-21-norm-cast.md +++ b/content/2024-02-21-norm-cast.md @@ -8,8 +8,9 @@ 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). +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). 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