@@ -147,7 +147,7 @@ lteSuccRight : LTE n m -> LTE n (S m)
147147lteSuccRight LTEZero = LTEZero
148148lteSuccRight (LTESucc x) = LTESucc (lteSuccRight x)
149149
150−||| n + 1 < m implies n < m
150+||| n + 1 < m implies n < m
151151lteSuccLeft : LTE (S n) m -> LTE n m
152152lteSuccLeft (LTESucc x) = lteSuccRight x
153153
@@ -236,7 +236,10 @@ Cast Integer Nat where
236236 cast = fromInteger
237237
238238Cast String Nat where
239− cast str = cast (the Integer (cast str))
239+ cast str = cast (the Integer (cast str))
240+
241+Cast Nat String where
242+ cast n = cast (the Integer (cast n))
240243
241244||| A wrapper for Nat that specifies the semigroup and monoid implementations that use (*)
242245record Multiplicative where