A text literal is the explicit checked constructor, never a trusted Text node.
2138def decodedTextLiteralTerm =
2139 (lambda unrestricted payload : Bytes .
2140 (constructor
2141 Term
2142 ConstructorApplication
2143 b"StdText"
2144 b"StdTextOf"
2145 (constructor
2146 Term
2147 TermSequenceNext
2148 (constructor Term BytesLiteral payload)
2149 (constructor
2150 Term
2151 TermSequenceNext
2152 (constructor
2153 Term
2154 Application
2155 (constructor
2156 Term
2157 Application
2158 (constructor Term Variable b"refl")
2159 (constructor
2160 Term
2161 FamilyApplication
2162 b"StdBool"
2163 (constructor Term TermSequenceEnd)))
2164 (constructor
2165 Term
2166 ConstructorApplication
2167 b"StdBool"
2168 b"StdTrue"
2169 (constructor Term TermSequenceEnd)))
2170 (constructor Term TermSequenceEnd)))))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.