1128def utf8CodepointsInvalidCount =
1129 (lambda unrestricted codepoints : (family UTF8Codepoints) .
1130 (eliminate
1131 UTF8Codepoints
1132 (lambda unrestricted current : (family UTF8Codepoints) . Nat)
1133 codepoints
1134 (branch UTF8CodepointsEnd . zero)
1135 (branch
1136 UTF8CodepointsNext
1137 head
1138 tail
1139 induction
1140 .
1141 (nat-eliminate
1142 (lambda unrestricted valid : Nat . Nat)
1143 (succ induction)
1144 (lambda unrestricted predecessor : Nat .
1145 (lambda unrestricted validInduction : Nat . induction))
1146 (utf8CodepointScalarValid head)))))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.