Skip to content

Commit 40944fa

Browse files
author
Alex Gryzlov
committed
remove unicode
1 parent 218aeb2 commit 40944fa

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/IndPrinciples.lidr

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -523,7 +523,7 @@ is equivalent to the cleaner inductive definition \idr{Ev}:
523523
The precise form of a \idr{data} definition can affect the induction principle
524524
Idris generates.
525525

526-
For example, in chapter `IndProp`, we defined as:
526+
For example, in chapter `IndProp`, we defined \idr{Le} as:
527527

528528
```idris
529529
data Le : Nat -> Nat -> Type where

0 commit comments

Comments
 (0)