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