Changes between Initial Version and Version 1 of Ticket #13025, comment 13


Ignore:
Timestamp:
Dec 24, 2016 3:19:09 AM (3 years ago)
Author:
goldfire
Comment:

Legend:

Unmodified
Added
Removed
Modified
  • Ticket #13025, comment 13

    initial v1  
    3939           ty' = ty `mkCastTy` co1
    4040           
    41            co2 = mkInstCo co (mkCoherenceLeftCo (mkNomReflCo ty) (mkSymCo co1))
     41           co2 = mkInstCo co (mkCoherenceLeftCo (mkNomReflCo ty) co1)
    4242           -- co2 :: ty1[ty |> co1 / a1] ~ ty2[ty / a2]
    4343