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