Normalizing Casts and Coercions

This web page collects the auxiliary materials for the paper Normalizing Casts and Coercions by Robert Y. Lewis and Paul-Nicolas Madelaine.

Our paper describes the latest version of norm_cast, on a personal branch of mathlib with an open pull request to master. The last commit before the paper submission is here .

Instructions for Testing

We recommend following the Lean installation instructions here.

Once Lean is installed, you can examine the norm_cast test file with the following:

git clone https://github.com/pnmadelaine/mathlib-norm-cast/
cd mathlib-norm-cast
git checkout origin/norm_cast_numerals
leanpkg configure
lean test/norm_cast.lean --make

The final line will take 10-30 minutes depending on your system. It is building all of the dependencies of the norm_cast test file. Then, open the mathlib_norm_cast DIRECTORY (not any particular file) in VSCode ("Open Folder..."), and navigate to tests/norm_cast.lean.

You can similarly inspect other files, for instance the p-adics. We highly recommend building them first (lean src/data/padics --make).