git.iko.soy/Idris-dev
on master help sign in
Fix Multiplicative/Additive docs

They had `(*)` and `(+)` the wrong way round :wink:

commit37845e4c24b95f94bec62eb1e80d2998661a6800 authorBenjamin Hodgson <benjamin.hodgson@huddle.com> dateSat 25 Jul 2015, 18:26 (11 years ago) parent6b062be
1 file changed+2−2
compare with master
unifiedsplit
libs/prelude/Prelude/Nat.idr+2−2
libs/prelude/Prelude/Nat.idr+2−2
@@ -213,12 +213,12 @@ instance MinBound Nat where
213213instance Cast Integer Nat where
214214 cast = fromInteger
215215
216−||| A wrapper for Nat that specifies the semigroup and monad instances that use (+)
216+||| A wrapper for Nat that specifies the semigroup and monad instances that use (*)
217217record Multiplicative where
218218 constructor getMultiplicative
219219 _ : Nat
220220
221−||| A wrapper for Nat that specifies the semigroup and monad instances that use (*)
221+||| A wrapper for Nat that specifies the semigroup and monad instances that use (+)
222222record Additive where
223223 constructor getAdditive
224224 _ : Nat