We should be able to use Free.Definition as an interface, so we can use the ♯ function using this interface, for all the different structures we will define. Related to #4 and #26.
Some suggestions:
[ ] Use instance arguments to carry around instances of Free, so each structure should implement a Free structure (for a specific signature and equations), and mark it as a public instance.
[x] Prove that if two types are both Free σ τ ε structures, then they're equivalent. We will be using this lemma a few times.
We should be able to use
Free.Definition
as an interface, so we can use the♯
function using this interface, for all the different structures we will define. Related to #4 and #26.Some suggestions:
Free σ τ ε
structures, then they're equivalent. We will be using this lemma a few times.