I am trying to write a test for
Hint Transparent and
Hint Opaque but I am having trouble coming up with a situation which only works in either case. It seems to me that hint search is disregarding the opaqueness, or perhaps I don't really understand what is going on?
So if anybody has a small example demonstrating how this works that would be great!
For examples I tried something like this:
Axiom A : Type. Axiom P : A -> Type. Definition Q := P. Existing Class P. Existing Class Q. Axiom a : A. Axiom pa : P a. #[local] Existing Instance pa. Goal sigT P. Proof. eexists. typeclasses eauto. Qed. #[local] Typeclasses Transparent Q. Goal sigT Q. Proof. eexists. typeclasses eauto.
But for whatever reason the second goal doesn't work, am I missing something?
Sorry ignore the #[local] for typeclasses transparent, that was something I was hacking.
transparency is used for
Definition b := a. Check _ : P b. Typeclasses Opaque b. Check _ : P b.
but not when deciding what class we're looking at
Last updated: Jan 31 2023 at 14:03 UTC