[Agda] Users of --no-coverage-check !?

[Andreas Abel]

Hi Agda users,

anyone using --no-coverage-check seriously?  We are considering to 
remove this option, as incomplete matches can be easily completed with a 
catch-all clause (and possibly a postulate to return something on the rhs).

See https://github.com/agda/agda/issues/1918

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/