change ! to * in resistor-color syntax (#174)

Author: oxe-i

exercises/practice/resistor-color/.docs/instructions.append.md

@@ -2,9 +2,9 @@
 
 ## Defining syntax
 
-In this exercise, you must define syntax for colors using the `c!` prefix, e.g., `c!black`.
+In this exercise, you must define syntax for colors using the `c*` prefix, e.g., `c*black`.
 This syntax should expand at compile time to each color's corresponding value as a `Fin 10`, according to the instructions.
-In the same way, you must define syntax for an array of all color values using `c!all`.
+In the same way, you must define syntax for an array of all color values using `c*all`.
 
 This task will likely require you to use either notations or macros.
 You might want to check a [reference][macro-reference].

exercises/practice/resistor-color/.meta/Example.lean

@@ -1,28 +1,28 @@
 /-
-notation "c!black"  => (0 : Fin 10)
-notation "c!brown"  => (1 : Fin 10)
-notation "c!red"    => (2 : Fin 10)
-notation "c!orange" => (3 : Fin 10)
-notation "c!yellow" => (4 : Fin 10)
-notation "c!green"  => (5 : Fin 10)
-notation "c!blue"   => (6 : Fin 10)
-notation "c!violet" => (7 : Fin 10)
-notation "c!grey"   => (8 : Fin 10)
-notation "c!white"  => (9 : Fin 10)
-notation "c!all"    => (Array.finRange 10)
+notation "c*black"  => (0 : Fin 10)
+notation "c*brown"  => (1 : Fin 10)
+notation "c*red"    => (2 : Fin 10)
+notation "c*orange" => (3 : Fin 10)
+notation "c*yellow" => (4 : Fin 10)
+notation "c*green"  => (5 : Fin 10)
+notation "c*blue"   => (6 : Fin 10)
+notation "c*violet" => (7 : Fin 10)
+notation "c*grey"   => (8 : Fin 10)
+notation "c*white"  => (9 : Fin 10)
+notation "c*all"    => (Array.finRange 10)
 -/
 
-syntax "c!" ident:term
+syntax "c*" ident:term
 
 macro_rules
-  | `(c!black)  => `((⟨0, by decide⟩ : Fin 10))
-  | `(c!brown)  => `((⟨1, by decide⟩ : Fin 10))
-  | `(c!red)    => `((⟨2, by decide⟩ : Fin 10))
-  | `(c!orange) => `((⟨3, by decide⟩ : Fin 10))
-  | `(c!yellow) => `((⟨4, by decide⟩ : Fin 10))
-  | `(c!green)  => `((⟨5, by decide⟩ : Fin 10))
-  | `(c!blue)   => `((⟨6, by decide⟩ : Fin 10))
-  | `(c!violet) => `((⟨7, by decide⟩ : Fin 10))
-  | `(c!grey)   => `((⟨8, by decide⟩ : Fin 10))
-  | `(c!white)  => `((⟨9, by decide⟩ : Fin 10))
-  | `(c!all)    => `((Array.finRange 10))
+  | `(c*black)  => `((⟨0, by decide⟩ : Fin 10))
+  | `(c*brown)  => `((⟨1, by decide⟩ : Fin 10))
+  | `(c*red)    => `((⟨2, by decide⟩ : Fin 10))
+  | `(c*orange) => `((⟨3, by decide⟩ : Fin 10))
+  | `(c*yellow) => `((⟨4, by decide⟩ : Fin 10))
+  | `(c*green)  => `((⟨5, by decide⟩ : Fin 10))
+  | `(c*blue)   => `((⟨6, by decide⟩ : Fin 10))
+  | `(c*violet) => `((⟨7, by decide⟩ : Fin 10))
+  | `(c*grey)   => `((⟨8, by decide⟩ : Fin 10))
+  | `(c*white)  => `((⟨9, by decide⟩ : Fin 10))
+  | `(c*all)    => `((Array.finRange 10))

exercises/practice/resistor-color/ResistorColor.lean

@@ -1,8 +1,8 @@
 /-
-  You must define syntax for colors using the `c!` prefix, e.g., `c!black`.
+  You must define syntax for colors using the `c*` prefix, e.g., `c*black`.
   This syntax should expand to its corresponding value as a `Fin 10`, according to the instructions.
 
-  You must also define syntax `c!all` that expands to an array containing all color values.
+  You must also define syntax `c*all` that expands to an array containing all color values.
 
   Macros and notations are not qualified by namespace.
   For this reason, this exercise does not define a namespace.

exercises/practice/resistor-color/ResistorColorTest.lean

@@ -3,17 +3,17 @@ import ResistorColor
 
 open LeanTest
 
-theorem h_black: c!black = (0 : Fin 10) := by rfl
-theorem h_brown: c!brown = (1 : Fin 10) := by rfl
-theorem h_red: c!red = (2 : Fin 10) := by rfl
-theorem h_orange: c!orange = (3 : Fin 10) := by rfl
-theorem h_yellow: c!yellow = (4 : Fin 10) := by rfl
-theorem h_green: c!green = (5 : Fin 10) := by rfl
-theorem h_blue: c!blue = (6 : Fin 10) := by rfl
-theorem h_violet: c!violet = (7 : Fin 10) := by rfl
-theorem h_grey: c!grey = (8 : Fin 10) := by rfl
-theorem h_white: c!white = (9 : Fin 10) := by rfl
-theorem h_all: c!all = #[c!black, c!brown, c!red, c!orange, c!yellow, c!green, c!blue, c!violet, c!grey, c!white] := by rfl
+theorem h_black: c*black = (0 : Fin 10) := by rfl
+theorem h_brown: c*brown = (1 : Fin 10) := by rfl
+theorem h_red: c*red = (2 : Fin 10) := by rfl
+theorem h_orange: c*orange = (3 : Fin 10) := by rfl
+theorem h_yellow: c*yellow = (4 : Fin 10) := by rfl
+theorem h_green: c*green = (5 : Fin 10) := by rfl
+theorem h_blue: c*blue = (6 : Fin 10) := by rfl
+theorem h_violet: c*violet = (7 : Fin 10) := by rfl
+theorem h_grey: c*grey = (8 : Fin 10) := by rfl
+theorem h_white: c*white = (9 : Fin 10) := by rfl
+theorem h_all: c*all = #[c*black, c*brown, c*red, c*orange, c*yellow, c*green, c*blue, c*violet, c*grey, c*white] := by rfl
 
 def main : IO UInt32 := do
   runTestSuitesWithExitCode []

generators/Generator/Generator/ResistorColorGenerator.lean

@@ -22,13 +22,13 @@ def genTestCase (_exercise : String) (case : TreeMap.Raw String Json) : String :
   let funName := getFunName (case.get! "property")
   match funName with
   | "colors" =>
-    let result := expected.getArr?.map (·.map (·.compress |> toLiteral |> (s!"c!{·}"))) |> getOk
+    let result := expected.getArr?.map (·.map (·.compress |> toLiteral |> (s!"c*{·}"))) |> getOk
     let theorems := result.toList.mapIdx fun i color =>
-      let c := color.dropPrefix "c!" |>.copy
+      let c := color.dropPrefix "c*" |>.copy
       s!"
 theorem h_{c}: {color} = ({i} : Fin 10) := by rfl"
     (String.join theorems) ++ s!"
-theorem h_all: c!all = {result} := by rfl"
+theorem h_all: c*all = {result} := by rfl"
   | _ => ""
 
 def genEnd (_exercise : String) : String :=