blob: b7e7f10c5a315c6144f369d5409b032c1e25335d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Class RepConversions (T:Type) (RT:Type) : Type :=
{
toRep : T -> RT;
unRep : RT -> T
}.
Definition RepConversionsOK {T RT} (RC:RepConversions T RT) := forall x, unRep (toRep x) = x.
Definition RepFunOK {T RT} `(RC:RepConversions T RT) (f:T->T) (rf : RT -> RT) :=
forall x, f (unRep x) = unRep (rf x).
Definition RepBinOpOK {T RT} `(RC:RepConversions T RT) (op:T->T->T) (rop : RT -> RT -> RT) :=
forall x y, op (unRep x) (unRep y) = unRep (rop x y).
|
