Typechecker, A11_10

[AdamBJ]

For question A11_10: (\ Write a type checking function [tyeq: tm -> ty -> bool].**)

Do we need to take into account the possibility of the typechecker function being passed badly typed input, eg tsucc ( ttrue)?

[jaewooklee93]

Yes, otherwise, for example, if t=tsucc (ttrue) can satisfy tycheck t T=true with some T, the first correctness theorem below will imply |- t \in T, so that the theorem becomes unprovable. You should return false for every badly typed term.

[AdamBJ]

That makes sense, thanks