@@ -986,40 +986,77 @@ primNames = [unitTy, unitCon,
986 falseTy, pairTy, pairCon,
986 falseTy, pairTy, pairCon,
987 eqTy, eqCon, inferTy, inferCon]
987 eqTy, eqCon, inferTy, inferCon]
989+unitDoc = parseDocstring . T.pack $ "The canonical single-element type, also known as the trivially true proposition."
989unitTy = sMN 0 "__Unit"
990unitTy = sMN 0 "__Unit"
990unitCon = sMN 0 "__II"
991unitCon = sMN 0 "__II"
991unitDecl = PDatadecl unitTy PType
992unitDecl = PDatadecl unitTy PType
992− [(emptyDocstring, [], unitCon, PRef bi unitTy, bi, [])]
993+ [(parseDocstring . T.pack $ "The trivial constructor for `()`. ", [], unitCon, PRef bi unitTy, bi, [])]
993unitOpts = [DefaultEliminator]
994unitOpts = [DefaultEliminator]
996+falseDoc = parseDocstring . T.pack $
997+ "The empty type, also known as the trivially false proposition." ++
999+ "Use `FalseElim` or `absurd` to prove anything if you have a variable " ++
1000+ "of type `_|_` in scope."
995falseTy = sMN 0 "__False"
1001falseTy = sMN 0 "__False"
996falseDecl = PDatadecl falseTy PType []
1002falseDecl = PDatadecl falseTy PType []
997falseOpts = []
1003falseOpts = []
1005+pairDoc = parseDocstring . T.pack $ "The non-dependent pair type, also known as conjunction."
999pairTy = sMN 0 "__Pair"
1006pairTy = sMN 0 "__Pair"
1000pairCon = sMN 0 "__MkPair"
1007pairCon = sMN 0 "__MkPair"
1001pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
1008pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
1009+ [(pairConDoc, pairConParamDoc,
1002− [(emptyDocstring, [], pairCon, PPi impl (n "A") PType (
1010+ pairCon, PPi impl (n "A") PType (
1003− PPi impl (n "B") PType (
1011+ PPi impl (n "B") PType (
1004− PPi expl (n "a") (PRef bi (n "A")) (
1012+ PPi expl (n "a") (PRef bi (n "A")) (
1005− PPi expl (n "b") (PRef bi (n "B"))
1013+ PPi expl (n "b") (PRef bi (n "B"))
1006− (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
1014+ (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
1007− pexp (PRef bi (n "B"))])))), bi, [])]
1015+ pexp (PRef bi (n "B"))])))), bi, [])]
1008 where n a = sMN 0 a
1016 where n a = sMN 0 a
1017+ pairConDoc = parseDocstring . T.pack $ "A pair of elements"
1018+ pairConParamDoc = [(n "a", parseDocstring . T.pack $ "the left element of the pair"),
1019+ (n "b", parseDocstring . T.pack $ "the right element of the pair")]
1009pairOpts = []
1020pairOpts = []
1021+pairParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left elements in the pair"),
1022+ (n "B", parseDocstring . T.pack $ "the type of the left elements in the pair")]
1023+ where n a = sMN 0 a
1011eqTy = sUN "="
1025eqTy = sUN "="
1012eqCon = sUN "refl"
1026eqCon = sUN "refl"
1027+eqDoc = parseDocstring . T.pack $
1028+ "The propositional equality type. A proof that `x` = `y`." ++
1030+ "**Note**: Idris's equality type is _heterogeneous_, which means that it " ++
1031+ "is possible to state equalities between values of potentially different " ++
1032+ "types. This is sometimes referred to in the literature as \"John Major\" " ++
1035+ "Thus, if Idris can't infer the type of one side of the equality, then " ++
1036+ "you may need to annotate it. See the function `the`."
1013eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),
1038eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),
1014 (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1039 (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1041+ [(reflDoc, reflParamDoc,
1016− [(emptyDocstring, [], eqCon, PPi impl (n "A") PType (
1042+ eqCon, PPi impl (n "A") PType (
1017− PPi impl (n "x") (PRef bi (n "A"))
1043+ PPi impl (n "x") (PRef bi (n "A"))
1018− (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1044+ (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1019− pimp (n "B") Placeholder False,
1045+ pimp (n "B") Placeholder False,
1020− pexp (PRef bi (n "x")),
1046+ pexp (PRef bi (n "x")),
1021− pexp (PRef bi (n "x"))])), bi, [])]
1047+ pexp (PRef bi (n "x"))])), bi, [])]
1022 where n a = sMN 0 a
1048 where n a = sMN 0 a
1049+ reflDoc = parseDocstring . T.pack $
1050+ "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1051+ "shown that both sides are in fact equal."
1052+ reflParamDoc = [(n "A", parseDocstring . T.pack $ "the type at which the equality is proven"),
1053+ (n "x", parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1055+eqParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left side of the equality"),
1056+ (n "B", parseDocstring . T.pack $ "the type of the right side of the equality")
1058+ where n a = sMN 0 a
1023eqOpts = []
1060eqOpts = []
1025elimName = sUN "__Elim"
1062elimName = sUN "__Elim"