The older elaborator for ExprHigh fails to be imported correctly by the new module system. It runs, however, it always returns false for the defEq check, which checks that a certain port is in the Module. This could maybe be because the body of the contains function is not available at meta-expansion time.
Addressing this, would allow LoopRewrite.lean and JoinRewrite.lean to be transitioned to the new module system.
The older elaborator for
ExprHighfails to be imported correctly by the new module system. It runs, however, it always returnsfalsefor thedefEqcheck, which checks that a certain port is in theModule. This could maybe be because the body of thecontainsfunction is not available at meta-expansion time.Addressing this, would allow
LoopRewrite.leanandJoinRewrite.leanto be transitioned to the new module system.