Is there an easy way for me to create a new hint database that automatically imports all existing hints from another database or more than one database?
for example using typeclasses if i have a typeclass Class X (A : Type) ...
and a database for lemmas that help me prove things about elements of type B, i might want a new database that helps me prove things about elements of a type Instance X B which extends the other database
that way i can add hints to the new one which wouldn't be applicable to the old one
Last updated: Jan 28 2023 at 06:30 UTC