edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-24 13:23:10 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #10 from diakopter/patch-2

Browse Source 
typo? in TypeDD
This commit is contained in:
Edwin Brady 2019-07-12 09:03:26 +02:00 committed by GitHub
commit d969a6f356
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
TypeDD.md
View File

@ -146,7 +146,7 @@ views explicit:
In `SnocList.idr`, in `my_reverse`, the link between `Snoc rec` and `xs ++ [x]` 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 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 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 what it allows to unify. So, `x` and `xs` need to be explicit arguments to
`Snoc`: `Snoc`: