From 77c0d7c3e55d7d01947a6b046adbc6d3105c927c Mon Sep 17 00:00:00 2001 From: Matthew Wilson Date: Thu, 11 Jul 2019 23:14:08 -0400 Subject: [PATCH] typo? in TypeDD --- TypeDD.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/TypeDD.md b/TypeDD.md index fc27116..c07e297 100644 --- a/TypeDD.md +++ b/TypeDD.md @@ -146,7 +146,7 @@ views explicit: In `SnocList.idr`, in `my_reverse`, the link between `Snoc rec` and `xs ++ [x]` needs to be made explicit. Idris 1 would happily decide that `xs` and `x` were the relevant implicit arguments to `Snoc` but this was little more than a guess -based on what would make it type checker, whereas Idris 2 is more precise in +based on what would make it type check, whereas Idris 2 is more precise in what it allows to unify. So, `x` and `xs` need to be explicit arguments to `Snoc`: