git.iko.soy/Idris-dev
on master help sign in
Update docs for equality type

Fixes #1393

commit2aed52aed2a20dcfa364fad9f2130d2bb2cd5500 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 17 Jul 2014, 14:37 (12 years ago) parentdbc0539
2 files changed+11−9
compare with master
unifiedsplit
libs/prelude/Builtins.idr+8−4 src/Idris/AbsSyntaxTree.hs+3−5
libs/prelude/Builtins.idr+8−4
@@ -15,12 +15,16 @@ FalseElim : _|_ -> a
1515||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
1616data Symbol_ : String -> Type where
1717
18−-- Eq_ : a -> a -> Type
19−-- Eq_ x y = (=) _ _ x y
20−
18+
2119infix 5 ~=~
2220
23−(~=~) : a -> b -> Type
21+||| Explicit heterogeneous ("John Major") equality. Use this when Idris
22+||| incorrectly chooses homogeneous equality for `(=)`.
23+||| @ a the type of the left side
24+||| @ b the type of the right side
25+||| @ x the left side
26+||| @ y the right side
27+(~=~) : (x : a) -> (y : b) -> Type
2428(~=~) x y = (=) _ _ x y
2529
2630-- ------------------------------------------------------ [ For rewrite tactic ]
src/Idris/AbsSyntaxTree.hs+3−5
@@ -1070,13 +1070,11 @@ eqDoc = parseDocstring . T.pack $
10701070 "To use such a proof, pattern-match on it, and the two equal things will " ++
10711071 "then need to be the _same_ pattern." ++
10721072 "\n\n" ++
1073− "**Note**: Idris's equality type is _heterogeneous_, which means that it " ++
1073+ "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
10741074 "is possible to state equalities between values of potentially different " ++
1075− "types. This is sometimes referred to in the literature as \"John Major\" " ++
1076− "equality." ++
1075+ "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
10771076 "\n\n" ++
1078− "Thus, if Idris can't infer the type of one side of the equality, then " ++
1079− "you may need to annotate it. See the function `the`."
1077+ "You may need to use `(~=~)` to explicitly request heterogeneous equality."
10801078
10811079eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]
10821080 (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]