From c8371da0cbc68f6a2455da7c64c3d3346b7f4d45 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Tue, 23 Jul 2024 22:19:57 +0200
Subject: Split code in multiple source files. Separate proofs and logic.

---
 BinaryHeap.lean | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'BinaryHeap.lean')

diff --git a/BinaryHeap.lean b/BinaryHeap.lean
index cd0e63f..9d1da1b 100644
--- a/BinaryHeap.lean
+++ b/BinaryHeap.lean
@@ -1,3 +1,6 @@
+/-
+  This file contains the Binary Heap type and its basic operations.
+-/
 import BinaryHeap.CompleteTree
 
 structure BinaryHeap (α : Type u) (le : α → α → Bool) (n : Nat) where
-- 
cgit v1.2.3