Correct error message in proof docs
commit9f4aea3bfa95fe87e6c33c6077e6a0d5846232ba
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateMon 23 Mar 2015, 23:04 (12 years ago)
parentbe93168
docs/proofs/pluscomm.rst+2−2
@@ -88,9 +88,9 @@ error:
8888
8989 When elaborating right hand side of four_eq_five:
9090 Can't unify
91− 5 = 5
91+ x = x (Type of Refl)
9292 with
93− 4 = 5
93+ 4 = 5 (Expected type)
9494
9595Type checking equality proofs
9696~~~~~~~~~~~~~~~~~~~~~~~~~~~~~