Way to debug expressions that don't typecheck

[jldodds]

It would be very useful if there was a function that took an expr and if that expr doesn't typecheck returns a (possibly) smaller expression along with the type it is expected to have

[jldodds]

or just a smaller expression that fails to typecheck on its own

[gmalecha]

I think the easiest thing to do right now is to call [typeof_expr](in https://github.com/gmalecha/mirror-core/blob/master/theories/Lambda/ExprDI.v#L105). It returns [None] if the term is well-typed and otherwise it returns [Some].

[jldodds]

Yep, I did that, but my term was huge. It would be nice if there was a function that found the part that didn't typecheck. I eventually found it my manually testing many parts of the term