Georg Stefan Schmid

I stumbled upon this PR looking for that exact functionality. From my point of view it's a perfectly legitimate feature. Consider for instance this case where the internal model doesn't...

The change doesn't seem to have any tremendous impact on performance. Integration tests run in roughly the same amount of time, while non-integration tests might be marginally slower. It seems...

Thanks, that's very interesting! Viktor actually mentioned something like `mergeFunctions` the other day, so I shouldn't be surprised to discover that you actually foresaw this :-) The changes in this...

We currently don't have a way of representing term-level function applications in types. You might be able to work around this using the usual tricks of replicating the term-level structure...

What's the deal with https://github.com/epfl-lara/inox/blob/master/src/main/scala/inox/evaluators/RecursiveEvaluator.scala#L525 anyways? It seems that lookup is contextual on the `tps` stored in `rctx` via `newTypes` in the `FunctionInvocation` case. But the corresponding update methods for...