From a9d385d8c0430154ef8a628fb233fc83fd62344f Mon Sep 17 00:00:00 2001 From: Matthias Hutzler Date: Sat, 16 Jul 2022 15:37:00 +0200 Subject: [PATCH] markdown typo in NAMING.md --- NAMING.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/NAMING.md b/NAMING.md index cae934cb24..c9aa7589b5 100644 --- 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 :