Mercurial > meta
changeset 12:a6730c3cfea7
Record.equal
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Tue, 08 Feb 2011 16:52:41 -0500 |
| parents | 67b33be5d56a |
| children | d05943db55e8 |
| files | record.ur record.urs |
| diffstat | 2 files changed, 9 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/record.ur Thu Feb 03 14:22:02 2011 -0500 +++ b/record.ur Tue Feb 08 16:52:41 2011 -0500 @@ -6,3 +6,9 @@ (fn [nm ::_] [r ::_] [[nm] ~ r] y acc => acc || x = y) False fl r + +fun equal [ts ::: {Type}] (eqs : $(map eq ts)) (fl : folder ts) (r1 : $ts) (r2 : $ts) : bool = + @foldR3 [eq] [id] [id] [fn _ => bool] + (fn [nm ::_] [t ::_] [r ::_] [[nm] ~ r] isEq x y acc => + acc && @eq isEq x y) + True fl eqs r1 r2
--- a/record.urs Thu Feb 03 14:22:02 2011 -0500 +++ b/record.urs Tue Feb 08 16:52:41 2011 -0500 @@ -2,3 +2,6 @@ val mem : a ::: Type -> ns ::: {Unit} -> eq a -> folder ns -> a -> $(mapU a ns) -> bool (* Is a value found in a record? *) + +val equal : ts ::: {Type} -> $(map eq ts) -> folder ts -> $ts -> $ts -> bool +(* Are two records equal? *)