Documentation

VCVio.Prelude.Core

Shared utilities and semantic normalization #

General finite-data utilities and proof attributes used by oracle programs, measure semantics, and program logic.

source
def Parser.Attr.game_rule :
Lean.ParserDescr

Simp set for game-hopping proofs of program and semantic equations.

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

    Simplification procedure

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

      VCVio-specific extension of PolyFun's handler_nf normalization set.

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

        Simplification procedure

        Instances For