Skip to content

Draft: Avoid making definitions from stdlib type class transparent

See the discussion here: #Rocq users > Trouble with two libraries interracting. The fact that we made these instances transparent, makes it hard to combine different libraries.

I tried to undo these side effects. The impact is relatively minor:

  • Some "derived" Inj instances relied on compose being transparent. That should be super easy to fix.
  • In the instance id_inj, Rocq somehow unfolds id when written as @id A. I don't understand this. But writing id instead of @id solves it...
  • The lemma list_find_fmap statement does not type check because it cannot find a Decision because compose is no longer unfolded. Perhaps we need a Hint Extern here.

Merge request reports

Loading