(*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
Definition ψ : CoreVar->HaskCoVar nil Δ
(*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
Definition ψ : CoreVar->HaskCoVar nil Δ
(* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
* free tyvars in them *)
Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
match coreVarToWeakVar cv with
| WExprVar wev => match weakTypeToType' φ wev ★ with
(* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
* free tyvars in them *)
Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
match coreVarToWeakVar cv with
| WExprVar wev => match weakTypeToType' φ wev ★ with
- | WTypeVar _ => fail "top-level xi got a type variable"
- | WCoerVar _ => fail "top-level xi got a coercion variable"
+ | WTypeVar _ => Prelude_error "top-level xi got a type variable"
+ | WCoerVar _ => Prelude_error "top-level xi got a coercion variable"
| OK τ => match τ with
| haskTypeOfSomeKind ★ τ' =>
match weakExprToStrongExpr Γ Δ φ ψ ξ τ' nil (*(makeClosedExpression*) we (* ) *) with
| OK τ => match τ with
| haskTypeOfSomeKind ★ τ' =>
match weakExprToStrongExpr Γ Δ φ ψ ξ τ' nil (*(makeClosedExpression*) we (* ) *) with
| OK e' => eol+++"$$"+++ nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e')+++"$$"+++eol
end
| haskTypeOfSomeKind κ τ' =>
| OK e' => eol+++"$$"+++ nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e')+++"$$"+++eol
end
| haskTypeOfSomeKind κ τ' =>