fixes

PatrickMassot · Feb 19, 2025 · 69e817b · 69e817b
1 parent 4c929fb
commit 69e817b
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 6 deletions.
diff --git a/GlimpseOfLean/Solutions/Topics/ClassicalPropositionalLogic.lean b/GlimpseOfLean/Solutions/Topics/ClassicalPropositionalLogic.lean
@@ -55,17 +55,17 @@ def Valid (A : Formula) : Prop := ∅ ⊨ A
   using theorems tagged with `@[simp]`. -/
 
 variable {v : Variable → Prop} {A B : Formula}
-@[simp] lemma isTrue_neg : IsTrue v ~A ↔ ¬ IsTrue v A := by simp
+@[simp] lemma isTrue_neg : IsTrue v ~A ↔ ¬ IsTrue v A := by simp [neg]
 
 @[simp] lemma isTrue_top : IsTrue v ⊤ := by {
   -- sorry
-  simp
+  simp [top]
   -- sorry
 }
 
 @[simp] lemma isTrue_equiv : IsTrue v (A ⇔ B) ↔ (IsTrue v A ↔ IsTrue v B) := by {
   -- sorry
-  simp
+  simp [equiv]
   tauto
   -- sorry
 }

diff --git a/GlimpseOfLean/Solutions/Topics/IntuitionisticPropositionalLogic.lean b/GlimpseOfLean/Solutions/Topics/IntuitionisticPropositionalLogic.lean
@@ -62,18 +62,18 @@ def Valid (A : Formula) : Prop := ∅ ⊨ A
   using theorems tagged with `@[simp]`. -/
 
 variable {v : Variable → H} {A B : Formula}
-@[simp] lemma eval_neg : eval v ~A = (eval v A)ᶜ := by simp
+@[simp] lemma eval_neg : eval v ~A = (eval v A)ᶜ := by simp [neg]
 
 @[simp] lemma eval_top : eval v top = ⊤ := by {
   -- sorry
-  simp
+  simp [top]
   -- sorry
 }
 
 @[simp]
 lemma isTrue_equiv : eval v (A ⇔ B) = (eval v A ⇨ eval v B) ⊓ (eval v B ⇨ eval v A) := by {
   -- sorry
-  simp
+  simp [equiv]
   -- sorry
 }