INNER CODE UNIT · Python

_

lean-dojo/TorchLean · torchlean/__init__.py:109

            outputs, _ = torch.utils._pytree.tree_flatten(model(*examples))
        if not all(isinstance(value, torch.Tensor) for value in outputs):
            raise ValueError("sample comparison requires tensor outputs")
        artifact["reference_outputs"] = [adapter._constant(value) for value in outputs]
    return artifact


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):

View source record →