+ Definition handleExpr' (ce:@CoreExpr CoreVar) : ???string :=
+ addErrorMessage ("input CoreSyn: " +++ ce)
+ (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) (
+ coreExprToWeakExpr ce >>= fun we =>
+ addErrorMessage ("WeakExpr: " +++ we)
+ ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we))
+ ((weakTypeOfWeakExpr we) >>= fun t =>
+ (addErrorMessage ("WeakType: " +++ t)
+ ((weakTypeToType'' φ t ★) >>= fun τ =>
+ addErrorMessage ("HaskType: " +++ τ)
+ ((weakExprToStrongExpr Γ Δ φ ψ ξ τ nil we) >>= fun e =>
+ OK (eol+++"$$"+++ nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e)+++"$$"+++eol)
+ )))))))).
+