Type Inference does not work

[ANinjaRabbit]

Type Inference does not work compared with vscode

for the same line of code

in cornelis , the inference looks like this :

however , it should behave like this in vscode:

Or maybe,there is something wrong with my usage or configuration , thanks for answering me! :)

[jakio6]

maybe try different normalization modes when calling :CornelisTypeContext? Like :CornelisTypeContext Normalised.

[eldritch-cookie]

where is the bug? suc x + y can be rewritten by agda into suc (x + y) as it is an equation of + if you don't believe me try making

suc-case-+ : suc x + y ≡ suc (x + y)
suc-case-+ = refl

although i do agree with the previous commenter, this is a difference of normalization and at least one normalization mode will give what you want, but given that agda knows the suc x + y to be the same as the suc (x + y) you can pass one instead of the other and implicitly exchange between the 2