The Coq mailing list

["John Wiegley" <johnw AT newartisans.com>]

I have a type class with some defined members:

Class Adjunction := {
  adj_iso  {a b} : F a ~{C}~> b ≊ a ~{D}~> U b;
  adj_left  {X Y} := to (@adj_iso X Y);
  adj_left_nat_l {a b c} (f : F b ~> c) (g : a ~> b) :
    adj_left _ _ (f ∘ fmap[F] g) ≈ adj_left _ _ f ∘ g
}.

As you can see, adj_left is defined directly in terms of adj_iso.

My problem is that I cannot rewrite suing adj_left_nat_l when I see a use of
"adj_left" in my goal, because adj_left_nat_l has already unfolded the
definition of adj_left and is actually now in terms of adj_iso. I have to
simplify my goal to unfold adj_left to a use of adj_iso, and then the rewrite
works.

Is there any way to make the member adj_left so that it does not unfold on
simplification, and is not unfolded in the type of adj_left_nat_l?

-- 
John Wiegley                  GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com                          60E1 46C4 BD1A 7AC1 4BA2