@@ -1028,6 +1028,9 @@ eqCon = sUN "refl"
1028eqDoc = parseDocstring . T.pack $
1028eqDoc = parseDocstring . T.pack $
1029 "The propositional equality type. A proof that `x` = `y`." ++
1029 "The propositional equality type. A proof that `x` = `y`." ++
1030 "\n\n" ++
1030 "\n\n" ++
1031+ "To use such a proof, pattern-match on it, and the two equal things will " ++
1032+ "then need to be the _same_ pattern." ++
1031 "**Note**: Idris's equality type is _heterogeneous_, which means that it " ++
1034 "**Note**: Idris's equality type is _heterogeneous_, which means that it " ++
1032 "is possible to state equalities between values of potentially different " ++
1035 "is possible to state equalities between values of potentially different " ++
1033 "types. This is sometimes referred to in the literature as \"John Major\" " ++
1036 "types. This is sometimes referred to in the literature as \"John Major\" " ++