From d914baf772242500a56259a30924e77c17f4f07a Mon Sep 17 00:00:00 2001
From: mehbark <terezi@pyrope.net>
Date: Tue, 8 Apr 2025 22:13:50 -0400
Subject: [PATCH] all: use standard theorem identifier scheme

https://leanprover-community.github.io/contribute/naming.html
---
 SimpleCounterexamples/FinitudeOfPropositions.lean | 4 ++--
 SimpleCounterexamples/RunMEvil.lean               | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/SimpleCounterexamples/FinitudeOfPropositions.lean b/SimpleCounterexamples/FinitudeOfPropositions.lean
index 12b8eb9..ed5cb91 100644
--- a/SimpleCounterexamples/FinitudeOfPropositions.lean
+++ b/SimpleCounterexamples/FinitudeOfPropositions.lean
@@ -1,13 +1,13 @@
 -- I actually thought that ∀p, ∃q, (q ≠ p) ∧ q!
 -- However, propositional extensionality tells us that (p ↔ q) → p = q
 
-theorem finiteTrueProps
+theorem finite_true_props
     : ¬∀p, ∃q, (q ≠ p) ∧ q := by
   intro h
   have := h True
   simp at this
 
-theorem finiteFalseProps
+theorem finite_false_props
     : ¬∀p, ∃q, (q ≠ p) ∧ ¬q := by
   intro h
   have := h False
diff --git a/SimpleCounterexamples/RunMEvil.lean b/SimpleCounterexamples/RunMEvil.lean
index 69735cd..5dd38c9 100644
--- a/SimpleCounterexamples/RunMEvil.lean
+++ b/SimpleCounterexamples/RunMEvil.lean
@@ -1,8 +1,8 @@
-theorem runMEvil
+theorem runM_evil
     (runM : {α : Type} → {m : Type → Type} → [Monad m] → m α → α) : False :=
   runM (none : Option Empty) |>.elim
 
-theorem lawfulRunMEvil
+theorem lawfulRunM_evil
     (runM : {α : Type} → {m : Type → Type} → [Monad m] → [LawfulMonad m] → m α → α)
     : False :=
   runM (none : Option Empty) |>.elim