Using Free.Definition you can show that Tree X is Free when the equations are empty.
There might be some circularity because the definition of ⊨ is using Tree.sharp, but we could make sharp private to the internal module and only expose the Free instance of Tree.
Using
Free.Definition
you can show thatTree X
is Free when the equations are empty.There might be some circularity because the definition of
⊨
is usingTree.sharp
, but we could makesharp
private to the internal module and only expose theFree
instance ofTree
.Depends on #26