I've started work on chapter 6, but I am completely lost. I think it's probably a culmination of misunderstandings, but I feel that I won't be producing useful feedback if I press on. A non exhaustive list of issues:
The => operator: What does it do? It seems to be required to solve 6.1, but I can't figure out how to use it
Single = on the rhs: Specifications in chapter 6 do this a lot. How does this work? For a minute I began to wonder if I misremembered, and the equality operator was single = rather than double ==.
6.1 in general leaves me with the impression I've missed something big. It seems like I'd need to be able to assign a specification to each equation. How can I tell it that the first list should be empty, or the second list should be empty, or they should have the same length? How do I tell it which to use for which equation?
In general, a lot of syntaxes are being introduced, and not really explained. In chapter 6, the predicate keyword was used, and it seems obvious what it does. But I'm sure there's some subtlety to it that bears explanation.
Here is a link to what I've done so far. I'll probably restart this chapter, and hopefully it clicks next time.
I've started work on chapter 6, but I am completely lost. I think it's probably a culmination of misunderstandings, but I feel that I won't be producing useful feedback if I press on. A non exhaustive list of issues:
The => operator: What does it do? It seems to be required to solve 6.1, but I can't figure out how to use it
Single = on the rhs: Specifications in chapter 6 do this a lot. How does this work? For a minute I began to wonder if I misremembered, and the equality operator was single = rather than double ==.
6.1 in general leaves me with the impression I've missed something big. It seems like I'd need to be able to assign a specification to each equation. How can I tell it that the first list should be empty, or the second list should be empty, or they should have the same length? How do I tell it which to use for which equation?
In general, a lot of syntaxes are being introduced, and not really explained. In chapter 6, the predicate keyword was used, and it seems obvious what it does. But I'm sure there's some subtlety to it that bears explanation.
Here is a link to what I've done so far. I'll probably restart this chapter, and hopefully it clicks next time.
https://drive.google.com/file/d/0Bx6BpheCXcBWVnVoQk11RkRsTUk/view?usp=sharing