diff options
Diffstat (limited to 'src/Rep.v')
-rw-r--r-- | src/Rep.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/Rep.v b/src/Rep.v new file mode 100644 index 000000000..b7e7f10c5 --- /dev/null +++ b/src/Rep.v @@ -0,0 +1,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). |