Patrick Nicodemus (Jan 01 2022 at 18:45): Patrick Nicodemus (Jan 01 2022 at 18:45):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?
Patrick Nicodemus (Jan 01 2022 at 18:47):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
Patrick Nicodemus (Jan 01 2022 at 18:47):that way i can add hints to the new one which wouldn't be applicable to the old one
Last updated: Oct 01 2023 at 19:01 UTC