Explain pattern exhaustiveness checking

[Nadrieril]

A first pass at documenting pattern exhaustiveness. Given that the algorithm is very self-contained and well-explained in the source file, I didn't think it was useful to give more details.

See #657
Ping @mark-i-m

[jyn514]

This is a really good explanation, btw, I'd never thought of 'exhaustiveness checking' as 'see if _ is applicable' but it's absolutely the same thing :)

[Nadrieril]

This is a really good explanation, btw, I'd never thought of 'exhaustiveness checking' as 'see if _ is applicable' but it's absolutely the same thing :)

Yeah, it's quite clever! That comes from the paper from which we got the algorithm: http://moscova.inria.fr/~maranget/papers/warn/index.html (this paper is mentioned in the docs).

[jyn514]

src/pat-exhaustive-checking.md
	21 : Finally, we can ask whether the whole match is exhaustive by asking whether the wildcard pattern (`_`)
	38 : and ensuring that matches are exhaustive (which is important for soundness, because a match expression can return a value).
2 offending lines found.
The command "MAX_LINE_LENGTH=100 bash ci/check_line_lengths.sh src/**/*.md" failed and exited with 1 during .

CI is unhappy :( you can check this locally with the pre-commit hook, there are instructions in the readme. Looks great other than that!

[jyn514]

Thanks for writing this up!

[Nadrieril]

No problem!