IWrite somehow persisently updates the file without requiring a write
afterwards. This can lead to unexpected behaviour where Idris fails to
recognise that a file has updated and checks the old .ttc version
instead of the file containing the change, e.g. a case-split. Adding an
explicit write at the end of IWrite seems to fix the problem.
IWrite somehow persisently updates the file without requiring a write afterwards. This can lead to unexpected behaviour where Idris fails to recognise that a file has updated and checks the old
.ttcversion instead of the file containing the change, e.g. a case-split. Adding an explicit write at the end ofIWriteseems to fix the problem.