论文标题
在精益数学库中使用和滥用实例参数
Use and abuse of instance parameters in the Lean mathematical library
论文作者
论文摘要
精益数学库Mathlib基于实例参数的机制，具有整理数学结构的类型模式的广泛使用。类型类别的相关机制在其他摊贩中提供，包括AGDA，COQ和ISABELLE的采用程度不同。本文分析了涉及当前精益3版本的Mathlib中实例参数的设计模式的代表性示例，重点是大规模出现的并发症以及Mathlib社区如何处理它们。
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.
