首页|Use and Abuse of Instance Parameters in the Lean Mathematical Library
Use and Abuse of Instance Parameters in the Lean Mathematical Library
扫码查看
点击上方二维码区域，可以放大扫码查看
原文链接
NETL
NSTL
Springer Nature
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 finalized Lean 3 version of Mathlib, focussing on complications arising at scale and how the Mathlib community deals with them.
NETL
NSTL
Springer Nature
