Use and abuse of instance parameters in the Lean mathematical library
Logic in Computer Science
2022-05-03 v3
Abstract
The Lean mathematical library mathlib features extensive use of the typeclass pattern for organising mathematical structures, based on Lean's mechanism of instance parameters. Related mechanisms for typeclasses are available in other provers including Agda, Coq and Isabelle with varying degrees of adoption. This paper analyses representative examples of design patterns involving instance parameters in the current Lean 3 version of mathlib, focussing on complications arising at scale and how the mathlib community deals with them.
Cite
@article{arxiv.2202.01629,
title = {Use and abuse of instance parameters in the Lean mathematical library},
author = {Anne Baanen},
journal= {arXiv preprint arXiv:2202.01629},
year = {2022}
}
Comments
To be published at Interactive Theorem Proving 2022 (Haifa, Israel). Unabridged, interactive versions of the listings are available at https://github.com/lean-forward/mathlib-classes/