From 40944fa4cb44cd45f7be4aa402b6e4891dc4e799 Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <alexander.gryzlov@adform.com>
Date: Tue, 8 Aug 2017 16:01:58 +0300
Subject: [PATCH] remove unicode

---
 src/IndPrinciples.lidr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/IndPrinciples.lidr b/src/IndPrinciples.lidr
index f31455d..65759c6 100644
--- a/src/IndPrinciples.lidr
+++ b/src/IndPrinciples.lidr
@@ -523,7 +523,7 @@ is equivalent to the cleaner inductive definition \idr{Ev}:
 The precise form of a \idr{data} definition can affect the induction principle
 Idris generates.
 
-For example, in chapter `IndProp`, we defined ≤ as:
+For example, in chapter `IndProp`, we defined \idr{Le} as:
 
 ```idris
 data Le : Nat -> Nat -> Type where