Documentation

VCVio.Prelude

VCVio Prelude #

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

source
def Parser.Attr.game_rule :
Lean.ParserDescr

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

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

    Simplification procedure

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

      Simp set for opening common query-handler definitions and run-shapes.

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

        Simplification procedure

        Instances For