fix: typos in docstrings (#822)

leanprover-community · Jun 4, 2024 · 63d7c6f · 63d7c6f
1 parent ee87917
commit 63d7c6f
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/Batteries/Util/Cache.lean b/Batteries/Util/Cache.lean
@@ -132,7 +132,7 @@ the second will store declarations from imports (and will hopefully be "read-onl
 -/
 @[reducible] def DiscrTreeCache (α : Type) : Type := DeclCache (DiscrTree α × DiscrTree α)
 
-/-- Discrimation tree settings for the `DiscrTreeCache`. -/
+/-- Discrimination tree settings for the `DiscrTreeCache`. -/
 def DiscrTreeCache.config : WhnfCoreConfig := {}
 
 /--

diff --git a/Batteries/Util/CheckTactic.lean b/Batteries/Util/CheckTactic.lean
@@ -9,7 +9,7 @@ import Lean.Elab.Term
 /-
 This file is the home for commands to tactics behave as expected.
 
-It currently includes two tactixs:
+It currently includes two tactics:
 
 #check_tactic t ~> res
 

diff --git a/Batteries/WF.lean b/Batteries/WF.lean
@@ -91,7 +91,7 @@ end Acc
 namespace WellFounded
 
 /-- Attaches to `x` the proof that `x` is accessible in the given well-founded relation.
-This can be used in recursive function definitions to explicitly use a differerent relation
+This can be used in recursive function definitions to explicitly use a different relation
 than the one inferred by default:
 
 ```