@@ -147,7 +147,7 @@ lteSuccRight : LTE n m -> LTE n (S m)
147lteSuccRight LTEZero = LTEZero
147lteSuccRight LTEZero = LTEZero
148lteSuccRight (LTESucc x) = LTESucc (lteSuccRight x)
148lteSuccRight (LTESucc x) = LTESucc (lteSuccRight x)
150−||| n + 1 < m implies n < m
150+||| n + 1 < m implies n < m
151lteSuccLeft : LTE (S n) m -> LTE n m
151lteSuccLeft : LTE (S n) m -> LTE n m
152lteSuccLeft (LTESucc x) = lteSuccRight x
152lteSuccLeft (LTESucc x) = lteSuccRight x
@@ -236,7 +236,10 @@ Cast Integer Nat where
236 cast = fromInteger
236 cast = fromInteger
238Cast String Nat where
238Cast String Nat where
239− cast str = cast (the Integer (cast str))
239+ cast str = cast (the Integer (cast str))
241+Cast Nat String where
242+ cast n = cast (the Integer (cast n))
241||| A wrapper for Nat that specifies the semigroup and monoid implementations that use (*)
244||| A wrapper for Nat that specifies the semigroup and monoid implementations that use (*)
242record Multiplicative where
245record Multiplicative where