INNER CODE UNIT · Python
_lean_string
lean-dojo/TorchLean · torchlean/__init__.py:116
def _lean_string(value: str) -> str:
escapes = {'"': '\\"', '\\': '\\\\', '\n': '\\n', '\r': '\\r', '\t': '\\t'}
return '"' + ''.join(escapes.get(char, f"\\u{ord(char):04x}" if ord(char) < 32 else char)
for char in value) + '"'
def _lean_json(value: Any, indent: int = 2) -> str:
"""Quote JSON constructors so Lean can reduce the importer inside proofs."""
if value is None:
return ".null"
if isinstance(value, bool):
return ".bool " + ("true" if value else "false")
if isinstance(value, (int, Decimal)):
number = Decimal(value)
sign, digits, exponent = number.as_tuple()
mantissa = int("".join(map(str, digits))) * (-1 if sign else 1)
if exponent > 0:
mantissa *= 10 ** exponent