From d859c9924e9b1cced4a7213d947815b90e17cb30 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 16 Oct 2020 22:48:00 +0100 Subject: [PATCH] Explain why exhaustiveness is necessary for soundness --- src/pat-exhaustive-checking.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/pat-exhaustive-checking.md b/src/pat-exhaustive-checking.md index da4dab3b..767b7de5 100644 --- a/src/pat-exhaustive-checking.md +++ b/src/pat-exhaustive-checking.md @@ -37,7 +37,8 @@ match x { Thus usefulness is used for two purposes: detecting unreachable code (which is useful to the user), -and ensuring that matches are exhaustive (which is important for soundness). +and ensuring that matches are exhaustive (which is important for soundness, +because a match expression can return a value). ## Where it happens