diff --git a/exercises/practice/resistor-color/.docs/instructions.append.md b/exercises/practice/resistor-color/.docs/instructions.append.md index 3eea3b8..de96658 100644 --- a/exercises/practice/resistor-color/.docs/instructions.append.md +++ b/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]. diff --git a/exercises/practice/resistor-color/.meta/Example.lean b/exercises/practice/resistor-color/.meta/Example.lean index 69f2307..0bbc909 100644 --- a/exercises/practice/resistor-color/.meta/Example.lean +++ b/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)) diff --git a/exercises/practice/resistor-color/ResistorColor.lean b/exercises/practice/resistor-color/ResistorColor.lean index 82e59bb..de2c758 100644 --- a/exercises/practice/resistor-color/ResistorColor.lean +++ b/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. diff --git a/exercises/practice/resistor-color/ResistorColorTest.lean b/exercises/practice/resistor-color/ResistorColorTest.lean index 813be64..42e4f8d 100644 --- a/exercises/practice/resistor-color/ResistorColorTest.lean +++ b/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 [] diff --git a/generators/Generator/Generator/ResistorColorGenerator.lean b/generators/Generator/Generator/ResistorColorGenerator.lean index 4c96587..1652a5d 100644 --- a/generators/Generator/Generator/ResistorColorGenerator.lean +++ b/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 :=