1107def utf8CodepointsWidthCount =
1108 (lambda unrestricted expected : Nat .
1109 (lambda unrestricted codepoints : (family UTF8Codepoints) .
1110 (eliminate
1111 UTF8Codepoints
1112 (lambda unrestricted current : (family UTF8Codepoints) . Nat)
1113 codepoints
1114 (branch UTF8CodepointsEnd . zero)
1115 (branch
1116 UTF8CodepointsNext
1117 head
1118 tail
1119 induction
1120 .
1121 (nat-eliminate
1122 (lambda unrestricted matches : Nat . Nat)
1123 induction
1124 (lambda unrestricted predecessor : Nat .
1125 (lambda unrestricted matchInduction : Nat . (succ induction)))
1126 (naturalEqual (utf8CodepointWidth head) expected))))))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.