1062def utf8CodepointWidth =
1063 (lambda unrestricted codepoint : (family UTF8Codepoint) .
1064 (eliminate
1065 UTF8Codepoint
1066 (lambda unrestricted current : (family UTF8Codepoint) . Nat)
1067 codepoint
1068 (branch
1069 UTF8CodepointValue
1070 word
1071 .
1072 (app
1073 (lambda unrestricted value : Nat .
1074 (nat-eliminate
1075 (lambda unrestricted valid : Nat . Nat)
1076 zero
1077 (lambda unrestricted validPredecessor : Nat .
1078 (lambda unrestricted validInduction : Nat .
1079 (nat-eliminate
1080 (lambda unrestricted ascii : Nat . Nat)
1081 (nat-eliminate
1082 (lambda unrestricted twoByte : Nat . Nat)
1083 (nat-eliminate
1084 (lambda unrestricted threeByte : Nat . Nat)
1085 (byte-to-nat (byte 4))
1086 (lambda unrestricted threePredecessor : Nat .
1087 (lambda unrestricted threeInduction : Nat . utf8NaturalThree))
1088 (nat-less-than value utf8NaturalSixtyFiveThousandFiveHundredThirtySix))
1089 (lambda unrestricted twoPredecessor : Nat .
1090 (lambda unrestricted twoInduction : Nat . utf8NaturalTwo))
1091 (nat-less-than value utf8NaturalTwoThousandFortyEight))
1092 (lambda unrestricted asciiPredecessor : Nat .
1093 (lambda unrestricted asciiInduction : Nat . utf8NaturalOne))
1094 (nat-less-than value utf8NaturalOneHundredTwentyEight))))
1095 (utf8WordScalarValid word)))
1096 (modelWord32ToNatural word)))))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.