VCVio Prelude

Shared project-wide declarations and simp attributes imported throughout VCVio.

def Parser.Attr.game_rule_proc : Lean.ParserDescr

Simplification procedure

Equations

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

def Parser.Attr.game_rule : Lean.ParserDescr

Simp set for game-hopping proofs: evalDist, probOutput, simulateQ, wp, relTriple rules.

Equations

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