| ||||
| ||||
![]() Title:Automatically Generalizing Theorems Using Typeclasses Authors:Alexander Best Conference:CICM 2021 Tags:automation, formal proof, interactive theorem prover, lean theorem prover, library maintainence, theorem prover and typeclasses Abstract: When producing large formally verified mathematical developments that make use of typeclasses it is easy to introduce overly strong assumptions for theorems and definitions. We consider the problem of recognizing from the elaborated proof terms when typeclass assumptions are stronger than necessary. We introduce a metaprogram for the Lean theorem prover that finds and informs the user about possible generalizations. Automatically Generalizing Theorems Using Typeclasses ![]() Automatically Generalizing Theorems Using Typeclasses | ||||
Copyright © 2002 – 2025 EasyChair |