From 14a2c8e444c9e05b4f34f25b79939b118aeacab8 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Tue, 8 Dec 2015 11:54:15 -0500
Subject: [PATCH] fix(init/nat): add spaces around inequalities

---
 hott/init/nat.hlean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/hott/init/nat.hlean b/hott/init/nat.hlean
index 30d1ad053a..e66a88d4ac 100644
--- a/hott/init/nat.hlean
+++ b/hott/init/nat.hlean
@@ -17,15 +17,15 @@ namespace nat
   | refl : le a a
   | step : Π {b}, le a b → le a (succ b)
 
-  infix `≤` := le
+  infix ` ≤ ` := le
   attribute le.refl [refl]
 
   definition lt [reducible] (n m : ℕ) := succ n ≤ m
   definition ge [reducible] (n m : ℕ) := m ≤ n
   definition gt [reducible] (n m : ℕ) := succ m ≤ n
-  infix `<` := lt
-  infix `≥` := ge
-  infix `>` := gt
+  infix ` < ` := lt
+  infix ` ≥ ` := ge
+  infix ` > ` := gt
 
   definition pred [unfold 1] (a : nat) : nat :=
   nat.cases_on a zero (λ a₁, a₁)