Mercurial > hg > Members > atton > delta_monad
view agda/revision.agda @ 104:ebd0d6e2772c
Trying redenition Delta with length constraints
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 26 Jan 2015 23:00:05 +0900 |
parents | |
children |
line wrap: on
line source
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 ∎