# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1682899681 -32400
# Node ID edfeedb455959963bc5a092cd51dbecfbc442f56
# Parent  08f752ecf32e3358f4571dc562c2c1ce42497bb5
merge

diff -r 08f752ecf32e -r edfeedb45595 redBlackTreeHoare.agda
--- a/redBlackTreeHoare.agda	Mon May 01 09:05:24 2023 +0900
+++ b/redBlackTreeHoare.agda	Mon May 01 09:08:01 2023 +0900
@@ -1,4 +1,4 @@
-module RedBlackTreeHoare where
+module redBlackTreeHoare where
 
 
 open import Level hiding (zero)