Hi Eric,
On Sun, Apr 14, 2013 at 10:57:43AM -0700, Eric Dobson wrote:
I am working at reimplementing the library Unbound to understand how
it works. One issue I have come up with is that an equation that I
thought held true doesn't. The equation is: Forall e::Rebind a b, e
`aeq` (uncurry
Where I am making the type error (that cannot be caught)? I would
assume it would be the 'let substed = subst x (Var y) rebound', line
in particular the third argument. But the documentation of subst does
not use either t or p in its type signature, so the rule doesn't seem
to apply [1]. And I
I am working at reimplementing the library Unbound to understand how
it works. One issue I have come up with is that an equation that I
thought held true doesn't. The equation is: Forall e::Rebind a b, e
`aeq` (uncurry rebind . unrebind $ e) = True. That is that spliting
the binding of a rebind
