idris-lang/Idris-dev — pull request #1204 by david-christiansen (2014-05-06 17:38:30+00:00)
Title: Make totality a warning until compiling

Now, totality errors will not prevent loading a file. This means that
features such as :missing and :addmissing can be used to fix the
problem.

However, the compiler will fail if there are totality errors, just as it
does with metavariables.