Convert single-char string to character code.
(s: StringRef)
| 4237 | |
| 4238 | |
| 4239 | def StrToCode(s: StringRef) -> ArithRef: |
| 4240 | """Convert single-char string to character code.""" |
| 4241 | return ArithRef( |
| 4242 | AppNode(_AstVar("str.to_code"), (s._ast,)), |
| 4243 | IntSort(), |
| 4244 | s._vars, |
| 4245 | ) |
| 4246 | |
| 4247 | |
| 4248 | def StrFromCode(c: ArithRef) -> StringRef: |