Single-element sequence.
(e: ExprRef)
| 3939 | |
| 3940 | |
| 3941 | def Unit(e: ExprRef) -> ExprRef: |
| 3942 | """Single-element sequence.""" |
| 3943 | if isinstance(e, StringRef): |
| 3944 | return e |
| 3945 | if isinstance(e, CharRef): |
| 3946 | return e |
| 3947 | return SeqRef(SeqUnitNode(e._ast), SeqSortRef(e._sort), e._vars) |
| 3948 | |
| 3949 | |
| 3950 | def SubSeq(s: StringRef, lo: ArithRef | int, length: ArithRef | int) -> StringRef: |