Today I'm running into several errors of this form:
where the failure is that (fun p -> inv p) and inv are not unifiable. I wonder if we can just make inv a "complete" arrow (^->), and somehow guide the unifier or automatically apply extensionality (probably that would be an F* improvement).
I could work around these problems, but sometimes it's not easy to find out this is what's failing.
Today I'm running into several errors of this form:
where the failure is that
(fun p -> inv p)andinvare not unifiable. I wonder if we can just makeinva "complete" arrow (^->), and somehow guide the unifier or automatically apply extensionality (probably that would be an F* improvement).I could work around these problems, but sometimes it's not easy to find out this is what's failing.