You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This typeclass (with instances for modelWithCornersSelf, ModelWithCorners.prod, and ModelWithCorners.pi) will allow us to
add generic to_space/from_space conversions to MDiffContAt etc
instead of formulating lemmas like MDiffContAt.prod twice.
There is a big flaw in this proposal: we still have non-defeq ChartedSpace instances.
The text was updated successfully, but these errors were encountered:
This typeclass (with instances for
modelWithCornersSelf
,ModelWithCorners.prod
, andModelWithCorners.pi
) will allow us toadd generic
to_space
/from_space
conversions toMDiffContAt
etcinstead of formulating lemmas like
MDiffContAt.prod
twice.There is a big flaw in this proposal: we still have non-defeq
ChartedSpace
instances.The text was updated successfully, but these errors were encountered: