From 212e250861f65fdddadbae1e8c79e4617ea36051 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sat, 13 Jan 2024 18:01:25 +0100
Subject: Minor, rename wellDefinedLt to wellDefinedLe

---
 Common/BinaryHeap.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'Common/BinaryHeap.lean')

diff --git a/Common/BinaryHeap.lean b/Common/BinaryHeap.lean
index 9d93c97..624caa1 100644
--- a/Common/BinaryHeap.lean
+++ b/Common/BinaryHeap.lean
@@ -38,7 +38,7 @@ def HeapPredicate {α : Type u} {n : Nat} (heap : CompleteTree α n) (le : α 
 structure BinaryHeap (α : Type u) (le : α → α → Bool) (n : Nat) where
   tree : CompleteTree α n
   valid : HeapPredicate tree le
-  wellDefinedLt : transitive_le le ∧ total_le le
+  wellDefinedLe : transitive_le le ∧ total_le le
 
 /--Please do not use this for anything meaningful. It's a debug function, with horrible performance.-/
 instance {α : Type u} [ToString α] : ToString (CompleteTree α n) where
@@ -321,10 +321,10 @@ theorem CompleteTree.heapInsertIsHeap {elem : α} {heap : CompleteTree α o} {le
           exact h₁.right.right.left
 
 def BinaryHeap.insert {α : Type u} {lt : α → α → Bool} {n : Nat} : α → BinaryHeap α lt n → BinaryHeap α lt (n+1)
-| elem, BinaryHeap.mk tree valid wellDefinedLt =>
-  let valid := tree.heapInsertIsHeap valid wellDefinedLt.left wellDefinedLt.right
+| elem, BinaryHeap.mk tree valid wellDefinedLe =>
+  let valid := tree.heapInsertIsHeap valid wellDefinedLe.left wellDefinedLe.right
   let tree := tree.heapInsert lt elem
-  {tree, valid, wellDefinedLt}
+  {tree, valid, wellDefinedLe}
 
 /--Helper function for CompleteTree.indexOf.-/
 def CompleteTree.indexOfAux {α : Type u} [BEq α] (elem : α) (heap : CompleteTree α o) (currentIndex : Nat) : Option (Fin (o+currentIndex)) :=
-- 
cgit v1.2.3

