markdown typo in NAMING.md (#863)

agda · Jul 16, 2022 · 1dde7b2 · 1dde7b2
1 parent 823531d
commit 1dde7b2
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/NAMING.md b/NAMING.md
@@ -56,8 +56,8 @@ For naming conventions specific to the Algebra subfolder, see
 
 * The `elim` and `rec` should be used as much as possible without
   renaming, but by importing and renaming the module.
-  For instance use "open import Cubical.Data.Empty as ⊥`
-  then use `⊥.rec` or `⊥.elim' rather than doing
+  For instance use `open import Cubical.Data.Empty as ⊥`
+  then use `⊥.rec` or `⊥.elim` rather than doing
   `renaming (rec to rec-⊥)` and using `rec-⊥`.
 
   Some convetional naming :