Filtering...

g-always-equal

books/centaur/gl/g-always-equal
other
(in-package "GL")
other
(include-book "g-primitives-help")
other
(include-book "g-if")
other
(include-book "symbolic-arithmetic")
other
(include-book "eval-g-base")
other
(include-book "always-equal-prep")
other
(include-book "g-equal")
other
(local (include-book "eval-g-base-help"))
other
(local (include-book "hyp-fix"))
other
(def-g-fn always-equal
  `(bfr-case :bdd (g-always-equal-core x
      y
      hyp
      clk
      config
      bvar-db
      state)
    :aig (glr equal
      x
      y
      hyp
      clk
      config
      bvar-db
      state)))
other
(verify-g-guards always-equal
  :hints `(("Goal" :in-theory (disable ,GL::GFN))))
other
(def-gobj-dependency-thm always-equal
  :hints `(("Goal" :in-theory (e/d (,GL::GFN)
       (g-always-equal-core gobj-depends-on)))))
other
(def-g-correct-thm always-equal
  eval-g-base
  :hints `(("Goal" :in-theory (e/d (,GL::GFN) (g-always-equal-core)))))