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