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