ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-22 22:47:12 +03:00
Code Issues Projects Releases Wiki Activity

Correct error message in proof docs

Browse Source
This commit is contained in:
Edwin Brady 2015-03-23 23:04:10 +00:00
parent be93168682
commit 9f4aea3bfa
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
docs/proofs/pluscomm.rst
View File

@ -88,9 +88,9 @@ error:
When elaborating right hand side of four_eq_five:
Can't unify
5 = 5
x = x (Type of Refl)
with
4 = 5
4 = 5 (Expected type)
Type checking equality proofs
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~