git.iko.soy/Idris-dev
on master help sign in
Update docs for equality type
2aed52aDavid Raymond Christiansen
libs/prelude/Builtins.idr+8−4
compare with master
unifiedsplit
@@ -15,12 +15,16 @@ FalseElim : _|_ -> a
15||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
15||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
16data Symbol_ : String -> Type where
16data Symbol_ : String -> Type where
17
17
18−-- Eq_ : a -> a -> Type
18+
19−-- Eq_ x y = (=) _ _ x y
20−
21infix 5 ~=~
19infix 5 ~=~
22
20
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
23−(~=~) : a -> b -> Type
27+(~=~) : (x : a) -> (y : b) -> Type
24(~=~) x y = (=) _ _ x y
28(~=~) x y = (=) _ _ x y
25
29
26-- ------------------------------------------------------ [ For rewrite tactic ]
30-- ------------------------------------------------------ [ For rewrite tactic ]
src/Idris/AbsSyntaxTree.hs+3−5
@@ -1070,13 +1070,11 @@ eqDoc = parseDocstring . T.pack $
1070 "To use such a proof, pattern-match on it, and the two equal things will " ++
1070 "To use such a proof, pattern-match on it, and the two equal things will " ++
1071 "then need to be the _same_ pattern." ++
1071 "then need to be the _same_ pattern." ++
1072 "\n\n" ++
1072 "\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 " ++
1074 "is possible to state equalities between values of potentially different " ++
1074 "is possible to state equalities between values of potentially different " ++
1075− "types. This is sometimes referred to in the literature as \"John Major\" " ++
1075+ "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1076− "equality." ++
1077 "\n\n" ++
1076 "\n\n" ++
1078− "Thus, if Idris can't infer the type of one side of the equality, then " ++
1077+ "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1079− "you may need to annotate it. See the function `the`."
1080
1078
1081eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]
1079eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]
1082 (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1080 (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]