@@ -1074,9 +1074,9 @@ eqDoc = parseDocstring . T.pack $
1074 "Thus, if Idris can't infer the type of one side of the equality, then " ++
1074 "Thus, if Idris can't infer the type of one side of the equality, then " ++
1075 "you may need to annotate it. See the function `the`."
1075 "you may need to annotate it. See the function `the`."
1077−eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),
1077+eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]
1078− (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1078+ (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1079− PType)
1079+ PType))
1080 [(reflDoc, reflParamDoc,
1080 [(reflDoc, reflParamDoc,
1081 eqCon, PPi impl (n "A") PType (
1081 eqCon, PPi impl (n "A") PType (
1082 PPi impl (n "x") (PRef bi (n "A"))
1082 PPi impl (n "x") (PRef bi (n "A"))