# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1422348593 -32400
# Node ID 2779a09e152698c826b14f0abdee8777a368d00e
# Parent  e6499a50ccbdd29a819d4f69b381a8683d616980
Delete Revision

diff -r e6499a50ccbd -r 2779a09e1526 agda/revision.agda
--- a/agda/revision.agda	Tue Jan 27 17:49:25 2015 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-open import Relation.Binary.PropositionalEquality
-module revision where
-
-data Rev : Set where
-  init   : Rev
-  commit : Rev -> Rev
-
-merge : Rev -> Rev -> Rev
-merge init b       = commit b
-merge (commit a) b = commit (merge a b)
-
-tip : Rev -> Rev -> Rev
-tip init init             = init
-tip init (commit b)       = commit b
-tip (commit a) init       = commit a
-tip (commit a) (commit b) = commit (tip a b)
-
-open ≡-Reasoning
-
-same-tip : (a : Rev) -> tip a a ≡ a
-same-tip init       = refl
-same-tip (commit v) = begin
-     tip (commit v) (commit v) ≡⟨ refl ⟩
-     commit (tip v v)          ≡⟨ cong commit (same-tip v) ⟩
-     commit v                  ∎