Documentation

Miri.Input.NormalizationBody

Resolve the body carried by compiler normalization evidence.

Legacy exports embed the normalized body. Compact exports may instead point at the source body's top-level JSON when the two complete serialized bodies are equal. Unknown references and malformed encodings fail closed.

Equations
  • One or more equations did not get rendered due to their size.
Instances For