Skip to content

Commit

Permalink
remove unicode
Browse files Browse the repository at this point in the history
  • Loading branch information
Alex Gryzlov committed Aug 8, 2017
1 parent 218aeb2 commit 40944fa
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/IndPrinciples.lidr
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 40944fa

Please sign in to comment.