Small step type inference algorithm
- STLC
- unification based ←> worklist?
- HM
termination proof is easier, by ind on steps, without logical relation
Small step type inference algorithm
termination proof is easier, by ind on steps, without logical relation