Renamed simp_hash to CollisionResistant_def

reilabs · Nov 29, 2023 · 0b6258f · 0b6258f
1 parent b67599c
commit 0b6258f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/ProvenZk/Hash.lean b/ProvenZk/Hash.lean
@@ -4,7 +4,7 @@ def Hash (F: Type) (n: Nat) : Type := Vector F n -> F
 
 def CollisionResistant {F n} (h: Hash F n): Prop := ∀{i1 i2}, h i1 = h i2 → i1 = i2
 
-@[simp] theorem simp_hash {h : Hash F n} [Fact (CollisionResistant h)] {a b : Vector F n}: h a = h b ↔ a = b := by
+@[simp] theorem CollisionResistant_def {h : Hash F n} [Fact (CollisionResistant h)] {a b : Vector F n}: h a = h b ↔ a = b := by
     have : CollisionResistant h := (inferInstance : Fact (CollisionResistant h)).elim
     apply Iff.intro
     { apply (inferInstance : Fact (CollisionResistant h)).elim }