License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2022.4
URN: urn:nbn:de:0030-drops-167131
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16713/
Baanen, Anne
Use and Abuse of Instance Parameters in the Lean Mathematical Library
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.
BibTeX - Entry
@InProceedings{baanen:LIPIcs.ITP.2022.4,
author = {Baanen, Anne},
title = {{Use and Abuse of Instance Parameters in the Lean Mathematical Library}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {4:1--4:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16713},
URN = {urn:nbn:de:0030-drops-167131},
doi = {10.4230/LIPIcs.ITP.2022.4},
annote = {Keywords: formalization of mathematics, dependent type theory, typeclasses, algebraic hierarchy, Lean prover}
}
