1148def utf8BytesCountWhere =
1149 (lambda unrestricted predicate : (pi unrestricted value : Byte . Nat) .
1150 (lambda unrestricted input : Bytes .
1151 (bytes-eliminate
1152 (lambda unrestricted current : Bytes . Nat)
1153 zero
1154 (lambda unrestricted head : Byte .
1155 (lambda unrestricted tail : Bytes .
1156 (lambda unrestricted induction : Nat .
1157 (nat-eliminate
1158 (lambda unrestricted matches : Nat . Nat)
1159 induction
1160 (lambda unrestricted predecessor : Nat .
1161 (lambda unrestricted matchInduction : Nat . (succ induction)))
1162 (predicate head)))))
1163 input)))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.