Commit 2022-11-19 11:25 36e2bac5

View on Github →

feat(scripts): add a script to update port comments (#17600) Also updates all existing port comments Currently this relies on an unreleased mathlibtools, which can be installed with pip install git+https://github.com/leanprover-community/mathlib-tools

Estimated changes