<div dir="ltr">I'm finding that code using the <font face="monospace"><b>rewrite</b></font>-construct works in a file that imports Naturals, but the same code fails in a different file, which defines the Naturals locally. In the latter case, expanding the code to its equivalent <font face="monospace"><b>with</b></font>-construct form results in successful compilation.<div><br></div><div>Just wondering if anyone else has observed this, too.</div><div><br></div><div>Thanks,</div><div>-db</div><div><br></div></div>