other
(in-package "OMAP")
other
(include-book "core")
other
(include-book "kestrel/fty/map" :dir :system)
other
(defsection emptyp-fix
:extension emptyp
(deffixequiv emptyp))
other
(defsection head-fix
:extension head
(deffixequiv head))
other
(defsection tail-fix
:extension tail
(deffixequiv tail))
other
(defsection update-fix :extension update (deffixequiv update :hints (("Goal" :in-theory (enable update)))))
other
(defsection update*-fix :extension update* (deffixequiv update* :hints (("Goal" :in-theory (enable update*)))))
other
(defsection delete-fix :extension delete (deffixequiv delete :hints (("Goal" :in-theory (enable delete)))))
other
(defsection delete*-fix :extension delete* (deffixequiv delete* :hints (("Goal" :in-theory (enable delete*)))))
other
(defsection assoc-fix :extension assoc (deffixequiv assoc :hints (("Goal" :in-theory (enable assoc)))))
other
(defsection in*-fix :extension in* (deffixequiv in* :hints (("Goal" :in-theory (enable in*)))))
other
(defsection list-in-fix :extension list-in (deffixequiv list-in :hints (("Goal" :in-theory (enable list-in)))))
other
(defsection list-notin-fix :extension list-notin (deffixequiv list-notin :hints (("Goal" :in-theory (enable list-notin)))))
other
(defsection lookup-fix
:extension lookup
(deffixequiv lookup))
other
(defsection lookup*-fix :extension lookup* (deffixequiv lookup* :hints (("Goal" :in-theory (enable lookup*)))))
other
(defsection list-lookup-fix :extension list-lookup (deffixequiv list-lookup :hints (("Goal" :in-theory (enable list-lookup)))))
other
(defsection rlookup-fix :extension rlookup (deffixequiv rlookup :hints (("Goal" :in-theory (enable rlookup)))))
other
(defsection rlookup*-fix :extension rlookup* (deffixequiv rlookup* :hints (("Goal" :in-theory (enable rlookup*)))))
other
(defsection restrict-fix :extension restrict (deffixequiv restrict :hints (("Goal" :in-theory (enable restrict)))))
other
(defsection keys-fix :extension keys (deffixequiv keys :hints (("Goal" :in-theory (enable keys)))))
other
(defsection values-fix :extension values (deffixequiv values :hints (("Goal" :in-theory (enable values)))))
other
(defsection compatiblep-fix :extension compatiblep (deffixequiv compatiblep :hints (("Goal" :in-theory (enable compatiblep)))))
other
(defsection submap-fix :extension submap (deffixequiv submap :hints (("Goal" :in-theory (enable submap)))))
other
(defsection size-fix :extension size (deffixequiv size :hints (("Goal" :in-theory (enable size)))))
other
(defsection from-lists :extension from-lists (deffixequiv from-lists :hints (("Goal" :in-theory (enable from-lists)))))