I am working through Software Foundations by myself and am trying the exercises, but I am stuck on the exercise for writing the function grade_comparison
.
Definition grade_comparison (g1 g2 : grade) : comparison
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
The definition of the type grade
is given by
Inductive grade : Type :=
Grade (l:letter) (m:modifier).
and we are given a function letter_comparison
which takes two letters and returns if they are equal, or if one is greater or less than the other.
I want to apply the letter_comparison
function to the letter portion of the two given grades since the instructions say to "do case analysis on the result of a suitable call to letter_comparison
to end up with just 3 possibilities."
However, I am not sure how to call letter comparison
correctly.
I have tried treating Grade
as a record type,
(letter_comparison (Grade A Plus).(l) (Grade C Plus).(l))
(letter_comparison (Grade A Plus).(letter) (Grade C Plus).(letter))
but nothing I have tried so far compiles.
I can write a separate function that returns the letter from a grade
Definition get_letter (g : grade) : letter :=
match g with
| Grade A _ => A
| Grade B _ => B
| Grade C _ => C
| Grade D _ => D
| Grade F _ => F
end.
Compute ((letter_comparison (get_letter (Grade C Plus)) (get_letter (Grade B Plus)))).
However, I think there is a way to do this without having to define this function.
I also don't know of an alternative way to get the letter from the grade other than a simplified get_letter
:
Definition get_letter (g : grade) :=
match g with Grade x _ => x end.
I think this is more or less standard. For example, the pair
type is defined similarly to grade
and the way we obtain the first or second elements of the pair is through dedicated functions, fst
and snd
in this case.