Remove some stray Ms

Author: yurrriq

src/IndProp.lidr

@@ -555,7 +555,7 @@ $\square$
 > namespace R
 >
 
-==== Exercise: 3 stars, recommendedM (R_provability)
+==== Exercise: 3 stars, recommended (R_provability)
 
 We can define three-place relations, four-place relations, etc., in just the
 same way as binary relations. For example, consider the following three-place
@@ -651,7 +651,7 @@ but it is not a subsequence of any of the lists
 $\square$
 
 
-==== Exercise: 2 stars, optionalM (R_provability2)
+==== Exercise: 2 stars, optional (R_provability2)
 
 Suppose we give Idris the following definition:
 

src/Logic.lidr

@@ -371,7 +371,7 @@ $\square$
 $\square$
 
 
-==== Exercise: 1 star, advancedM (informal_not_PNP)
+==== Exercise: 1 star, advanced (informal_not_PNP)
 
 Write an informal proof (in English) of the proposition \idr{Not (p, Not p)}.
 

src/Poly.lidr

@@ -121,7 +121,7 @@ an appropriate type parameter:
 > test_repeat2 = Refl
 
 
-==== Exercise: 2 starsM (mumble_grumble)
+==== Exercise: 2 stars (mumble_grumble)
 
 \ \todo[inline]{Explain implicits and \idr{{x=foo}} syntax first? Move after the
 "Supplying Type Arguments Explicitly" section?}
@@ -448,7 +448,7 @@ standard library calls it \idr{combine}).
 > zip (x::tx) (y::ty) = (x,y) :: zip tx ty
 
 
-==== Exercise: 1 star, optionalM (combine_checks)
+==== Exercise: 1 star, optional (combine_checks)
 
 Try answering the following questions on paper and checking your answers in
 Idris:
@@ -799,7 +799,7 @@ fold andb : List Bool -> Bool -> Bool
 > fold_example3 = Refl
 
 
-==== Exercise: 1 star, advancedM (fold_types_different)
+==== Exercise: 1 star, advanced (fold_types_different)
 
 Observe that the type of \idr{fold} is parameterized by _two_ type variables,
 \idr{x} and \idr{y}, and the parameter \idr{f} is a binary operator that takes
@@ -890,7 +890,7 @@ Prove the correctness of \idr{fold_length}.
 $\square$
 
 
-==== Exercise: 3 starsM (fold_map)
+==== Exercise: 3 stars (fold_map)
 
 We can also define \idr{map} in terms of fold. Finish \idr{fold_map} below.
 
@@ -958,7 +958,7 @@ types of \idr{prod_curry} and \idr{prod_uncurry}?
 $\square$
 
 
-==== Exercise: 2 stars, advancedM (nth_error_informal)
+==== Exercise: 2 stars, advanced (nth_error_informal)
 
 Recall the definition of the \idr{nth_error} function:
 

src/Tactics.lidr

@@ -178,7 +178,7 @@ hypotheses in the context. Remember that `:search` is your friend.)
 $\square$
 
 
-==== Exercise: 1 star, optionalM (apply_rewrite)
+==== Exercise: 1 star, optional (apply_rewrite)
 
 Briefly explain the difference between the tactics \idr{exact} and
 \idr{rewriteWith}. What are the situations where both can usefully be applied?
@@ -717,7 +717,7 @@ The following exercise requires the same pattern.
 $\square$
 
 
-==== Exercise: 2 stars, advancedM (beq_nat_true_informal)
+==== Exercise: 2 stars, advanced (beq_nat_true_informal)
 
 Give a careful informal proof of \idr{beq_nat_true}, being as explicit as possible
 about quantifiers.
@@ -1151,7 +1151,7 @@ $\square$
 $\square$
 
 
-==== Exercise: 3 stars, advancedM (split_combine)
+==== Exercise: 3 stars, advanced (split_combine)
 
 We proved, in an exercise above, that for all lists of pairs, \idr{zip} is the
 inverse of \idr{unzip}. How would you formalize the statement that \idr{unzip}