Documentation

VCVio.Prelude

VCVio Prelude #

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

source
def Parser.Attr.game_rule_proc :
Lean.ParserDescr

Simplification procedure

Instances For
    source
    def Parser.Attr.game_rule :
    Lean.ParserDescr

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

    Instances For