# Use and abuse of instance parameters in the Lean mathematical library

Preprint · Anne Baanen

- Archive id: arxiv:2202.01629
- Published: 2022-02-03
- arXiv: https://arxiv.org/abs/2202.01629
- Source URL: https://arxiv.org/abs/2202.01629
- PDF: https://arxiv.org/pdf/2202.01629
- Provenance: arxiv

## 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.

_Abstract reproduced under CC0-1.0 (arXiv descriptive metadata)._

---
Space Kitty Archive · https://space-kitty.com · API: https://space-kitty.com/api/v1 · MCP: https://space-kitty.com/mcp · Premium: $0.20/request via x402 (Base Sepolia (testnet)). Metadata: arXiv (CC0), OpenAlex (CC0), Europe PMC (CC BY/CC0 works), ClinicalTrials.gov.