knisht opened this issue 4 years ago · 1 comments
Don't even ask why I need such construction. There should be no problems with this code, because it typechecks without \let.
\let
\data Y | bar (\let a => 1 \in Y)
I can ask the same question as in #284. Should positivity checker normalize everything before the check?
