Stable diagnostics for the closed literal failure vocabulary; other parser
failures retain their caller-owned code.
882def quotedLiteralDiagnosticCode =
883 (lambda unrestricted code : Nat .
884 (lambda unrestricted fallback : Bytes .
885 (app
886 (nat-eliminate
887 (lambda unrestricted matched : Nat . (pi unrestricted force : Nat . Bytes))
888 (lambda unrestricted force : Nat .
889 (app
890 (nat-eliminate
891 (lambda unrestricted matched : Nat . (pi unrestricted force : Nat . Bytes))
892 (lambda unrestricted force : Nat .
893 (app
894 (nat-eliminate
895 (lambda unrestricted matched : Nat . (pi unrestricted force : Nat . Bytes))
896 (lambda unrestricted force : Nat .
897 (app
898 (nat-eliminate
899 (lambda unrestricted matched : Nat .
900 (pi unrestricted force : Nat . Bytes))
901 (lambda unrestricted force : Nat .
902 (app
903 (nat-eliminate
904 (lambda unrestricted matched : Nat .
905 (pi unrestricted force : Nat . Bytes))
906 (lambda unrestricted force : Nat .
907 (app
908 (nat-eliminate
909 (lambda unrestricted matched : Nat .
910 (pi unrestricted force : Nat . Bytes))
911 (lambda unrestricted force : Nat .
912 (app
913 (nat-eliminate
914 (lambda unrestricted matched : Nat .
915 (pi unrestricted force : Nat . Bytes))
916 (lambda unrestricted force : Nat .
917 (app
918 (nat-eliminate
919 (lambda unrestricted matched : Nat .
920 (pi unrestricted force : Nat . Bytes))
921 (lambda unrestricted force : Nat .
922 (app
923 (nat-eliminate
924 (lambda unrestricted matched : Nat .
925 (pi unrestricted force : Nat . Bytes))
926 (lambda unrestricted force : Nat . fallback)
927 (lambda unrestricted predecessor : Nat .
928 (lambda unrestricted unused : (pi unrestricted force : Nat . Bytes) .
929 (lambda unrestricted force : Nat .
930 b"ALPHA-SOURCE-INVALID-UTF8")))
931 (Std.Natural/naturalEqual
932 code
933 (quotedLiteralFailureCode
934 (constructor QuotedLiteralFailure QuotedInvalidUTF8))))
935 zero))
936 (lambda unrestricted predecessor : Nat .
937 (lambda unrestricted unused : (pi unrestricted force : Nat . Bytes) .
938 (lambda unrestricted force : Nat .
939 b"ALPHA-LITERAL-SCALAR")))
940 (Std.Natural/naturalEqual
941 code
942 (quotedLiteralFailureCode
943 (constructor QuotedLiteralFailure QuotedInvalidScalar))))
944 zero))
945 (lambda unrestricted predecessor : Nat .
946 (lambda unrestricted unused : (pi unrestricted force : Nat . Bytes) .
947 (lambda unrestricted force : Nat .
948 b"ALPHA-LITERAL-UNICODE-ESCAPE")))
949 (Std.Natural/naturalEqual
950 code
951 (quotedLiteralFailureCode
952 (constructor QuotedLiteralFailure QuotedUnicodeSyntax))))
953 zero))
954 (lambda unrestricted predecessor : Nat .
955 (lambda unrestricted unused : (pi unrestricted force : Nat . Bytes) .
956 (lambda unrestricted force : Nat .
957 b"ALPHA-LITERAL-UNTERMINATED")))
958 (Std.Natural/naturalEqual
959 code
960 (quotedLiteralFailureCode
961 (constructor QuotedLiteralFailure QuotedUnterminated))))
962 zero))
963 (lambda unrestricted predecessor : Nat .
964 (lambda unrestricted unused : (pi unrestricted force : Nat . Bytes) .
965 (lambda unrestricted force : Nat .
966 b"ALPHA-LITERAL-NEWLINE")))
967 (Std.Natural/naturalEqual
968 code
969 (quotedLiteralFailureCode
970 (constructor QuotedLiteralFailure QuotedNewline))))
971 zero))
972 (lambda unrestricted predecessor : Nat .
973 (lambda unrestricted unused : (pi unrestricted force : Nat . Bytes) .
974 (lambda unrestricted force : Nat .
975 b"ALPHA-LITERAL-BYTES-NON-ASCII")))
976 (Std.Natural/naturalEqual
977 code
978 (quotedLiteralFailureCode
979 (constructor QuotedLiteralFailure QuotedNonASCII))))
980 zero))
981 (lambda unrestricted predecessor : Nat .
982 (lambda unrestricted unused : (pi unrestricted force : Nat . Bytes) .
983 (lambda unrestricted force : Nat .
984 b"ALPHA-LITERAL-BYTE-ESCAPE")))
985 (Std.Natural/naturalEqual
986 code
987 (quotedLiteralFailureCode (constructor QuotedLiteralFailure QuotedBadHex))))
988 zero))
989 (lambda unrestricted predecessor : Nat .
990 (lambda unrestricted unused : (pi unrestricted force : Nat . Bytes) .
991 (lambda unrestricted force : Nat .
992 b"ALPHA-LITERAL-INCOMPLETE-ESCAPE")))
993 (Std.Natural/naturalEqual
994 code
995 (quotedLiteralFailureCode
996 (constructor QuotedLiteralFailure QuotedIncompleteEscape))))
997 zero))
998 (lambda unrestricted predecessor : Nat .
999 (lambda unrestricted unused : (pi unrestricted force : Nat . Bytes) .
1000 (lambda unrestricted force : Nat .
1001 b"ALPHA-LITERAL-UNKNOWN-ESCAPE")))
1002 (Std.Natural/naturalEqual
1003 code
1004 (quotedLiteralFailureCode (constructor QuotedLiteralFailure QuotedUnknownEscape))))
1005 zero)))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.