2026-07-22T19:33:54Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16713 2024-03-06T10:58:07Z ddc:004 open_access

Use and Abuse of Instance Parameters in the Lean Mathematical Library Baanen, Anne formalization of mathematics dependent type theory typeclasses algebraic hierarchy Lean prover 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Anne Baanen 2022 Is Part Of LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2022.4 urn:nbn:de:0030-drops-167131 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.4 eng https://creativecommons.org/licenses/by/4.0/legalcode