other
(in-package "GL")
other
(include-book "g-primitives-help")
other
(include-book "eval-g-base")
other
(include-book "gtypes")
other
(include-book "g-if")
other
(local (include-book "gtype-thms"))
other
(def-g-fn hide '(gret x) :replace-g-ifs nil)
other
(local (defthm hide-open (equal (hide x) x) :hints (("Goal" :expand ((:free (x) (hide x)))))))
other
(verify-g-guards hide)
other
(def-gobj-dependency-thm hide :hints `(("goal" :expand (,GL::GCALL) :in-theory (disable (:d ,GL::GFN)))))
other
(def-g-correct-thm hide eval-g-base :hints `(("Goal" :in-theory '(hide-open ,GL::GFN))))