Don't force extern classes to implement extern traits

[seanmcl]

Imagine we are modeling a toy version of the Java standard library:

trait {:extern} Object {
  function method {:extern} toString(): string
}

class {:extern} Integer extends Object {
  // Error: class 'Integer' does not implement trait function 'Object.toString'
}

Every class will extend Object, and will have toString defined. It would be nice to not need to copy the toString declaration for every extern. This problem is compounded for deep subtyping hierarchies with complex pre/postconditions. A nice feature would be to simply assume externs implement all the methods required of them.

[MikaelMayer]

Not having this makes it impossible to model external class/trait hierarchy without an assume false.

[dschoepe]

I think that's not impossible, just tedious, as one has to repeat the method/function signatures for each class implementing a trait.