I am using Btermdn and I am finally seeing something that I had previously suspected to also affect typeclass search: Using Btermdn's
pattern function with the transparency state of a
Hint Variables Transparent database , universally quantified variables of both the section and the current lemma are translated to
_. If I set
Hint Variables Opaque : my_db, the variables appear in the pattern as themselves. I absolutely do not understand how this happens. From my reading of
bounded_constr_pat_discr_st it seems like
Environ.evaluable_named would have to return
true for a
LocalAssum, which it simply doesn't.
I already wondered if maybe I am using the wrong environment but even
Proofview.tclENV should give correct readings for section variables and they are affected just like local variables. Does anyone have any clues as to what might be going on here or how I could debug it further? (Or is this behavior intentional?)
that doesn't exist
_env suffix was added by my fingers without my brain's input!
But I think the right code path is actually the one with
_st at the end.
I have been staring at this code for quite a while and it's just alphabet soup to me now :(
I am still puzzled by this behavior. I can't share my code but if it helps I can share some debug output / generally explain what my code is doing.
Last updated: Jun 08 2023 at 04:01 UTC