Arend icon indicating copy to clipboard operation
Arend copied to clipboard

Published 20 hours ago • verified publisher icon JetBrains

More general classifying expressions

Open valis opened this issue 5 years ago • 1 comments

Currently, pi-types and sigma-types are not allowed in classifying expressions of instances. Also, only a restricted form of lambda expressions is allowed.

valis avatar Feb 21 '20 19:02 valis

Is it this code that does such restriction?

https://github.com/JetBrains/Arend/blob/3e8cfd5bd27421a8f78f5e7af326e21f55f3fab6/base/src/main/java/org/arend/typechecking/instance/pool/GlobalInstancePool.java#L122-L130

ice1000 avatar Sep 25 '20 21:09 ice1000