diff agda/laws.agda @ 131:d205ff1e406f InfiniteDeltaWithMonad

Cleanup proofs
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 03 Feb 2015 12:57:13 +0900
parents 5902b2a24abf
children 575de2e38385
line wrap: on
line diff
--- a/agda/laws.agda	Tue Feb 03 12:46:20 2015 +0900
+++ b/agda/laws.agda	Tue Feb 03 12:57:13 2015 +0900
@@ -1,5 +1,6 @@
 open import Relation.Binary.PropositionalEquality
 open import Level
+
 open import basic
 
 module laws where