Unicode is legal only in a quoted token or a comment, never an identifier.
1010def parserOutsideSourceByte =
1011 (lambda unrestricted bytePrefix : Nat .
1012 (lambda unrestricted offset : Nat .
1013 (lambda unrestricted head : Byte .
1014 (lambda unrestricted stripState : Nat .
1015 (lambda unrestricted continue : (pi unrestricted quoteState : Nat . (pi unrestricted stripState : Nat . (family StreamingStructuralState))) .
1016 (parserChooseStreamingState
1017 (parserStripIsComment stripState)
1018 (lambda unrestricted force : Nat .
1019 (parserOutsideSourceByteUnchecked bytePrefix offset head stripState continue))
1020 (lambda unrestricted force : Nat .
1021 (parserChooseStreamingState
1022 (byte-less-than head (byte 128))
1023 (lambda unrestricted force : Nat .
1024 (parserChooseStreamingState
1025 (parserSourceControlInvalid head)
1026 (lambda unrestricted force : Nat .
1027 (constructor
1028 StreamingStructuralState
1029 StreamingStructuralFailed
1030 (byte-to-nat (byte 103))
1031 (constructor SyntaxOrigin SyntaxOriginUnknown)
1032 b""
1033 (constructor SyntaxOrigin SyntaxOriginUnknown)))
1034 (lambda unrestricted force : Nat .
1035 (parserOutsideSourceByteUnchecked
1036 bytePrefix
1037 offset
1038 head
1039 stripState
1040 continue))))
1041 (lambda unrestricted force : Nat .
1042 (constructor
1043 StreamingStructuralState
1044 StreamingStructuralFailed
1045 (byte-to-nat (byte 102))
1046 (constructor SyntaxOrigin SyntaxOriginUnknown)
1047 b""
1048 (constructor SyntaxOrigin SyntaxOriginUnknown)))))))))))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.