SubExpr doesn't work for implemented fields

JetBrains / Arend

The Arend Proof Assistant

https://arend-lang.github.io/

Apache License 2.0

694 stars 33 forks source link

Closed ice1000 closed 4 years ago

ice1000 commented 4 years ago

Need a test

ice1000 commented 4 years ago

This code typechecks in the sandbox IDE:

However, when passing it to the test case, it gives me error:

Do you know what's happening here? @valis