Invalid requests have no wire representation. This makes the encoder
fail-closed while keeping construction and static evaluation lightweight.
159def textArtifactRequestEncode =
160 (lambda unrestricted request : (family TextArtifactRequest) .
161 (nat-eliminate
162 (lambda unrestricted current : Nat . Bytes)
163 b""
164 (lambda unrestricted predecessor : Nat .
165 (lambda unrestricted induction : Bytes .
166 (textArtifactRequestEncodeUnchecked request)))
167 (textArtifactRequestFieldsValid request)))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.