summaryrefslogtreecommitdiff
path: root/transfer/lib/pair.tr
diff options
context:
space:
mode:
authorbringert <bringert@cs.chalmers.se>2005-11-30 16:00:06 +0000
committerbringert <bringert@cs.chalmers.se>2005-11-30 16:00:06 +0000
commitcba2fcb9b118cedb603b171ac7d7581c5adb844c (patch)
tree5f777207338134402d07486d334dcc764d933027 /transfer/lib/pair.tr
parent86df2a69b149c1f4ff2cb9139447f5a6faccd483 (diff)
Moved transfer libraries to transfer/lib
Diffstat (limited to 'transfer/lib/pair.tr')
-rw-r--r--transfer/lib/pair.tr11
1 files changed, 11 insertions, 0 deletions
diff --git a/transfer/lib/pair.tr b/transfer/lib/pair.tr
new file mode 100644
index 000000000..1b70411e8
--- /dev/null
+++ b/transfer/lib/pair.tr
@@ -0,0 +1,11 @@
+Pair : Type -> Type -> Type
+Pair A B = sig { p1 : A; p2 : B }
+
+pair : (A:Type) -> (B:Type) -> A -> B -> Pair A B
+pair _ _ x y = rec { p1 = x; p2 = y }
+
+fst : (A:Type) -> (B:Type) -> Pair A B -> A
+fst _ _ p = case p of Pair _ _ x _ -> x
+
+snd : (A:Type) -> (B:Type) -> Pair A B -> B
+snd _ _ p = case p of Pair _ _ x _ -> x