15 citations · 34 across the 6 of their papers we have counts for
Showing cs.PLShow all
2 papers · 1 filter
cs.PL2020★ 15 cited
Maintaining a Library of Formal Mathematics
Floris van Doorn, Gabriel Ebner, Robert Y. Lewis
The Lean mathematical library mathlib is developed by a community of users with very different backgrounds and levels of experience. To lower the barrier of entry for contributors…
cs.PL2020
Simplifying Casts and Coercions
Robert Y. Lewis, Paul-Nicolas Madelaine
This paper introduces norm_cast, a toolbox of tactics for the Lean proof assistant designed to manipulate expressions containing coercions and casts. These expressions can be frust…