Stream: Coq users

Topic: creating one hintdb that extends another


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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: Jan 28 2023 at 06:30 UTC