Filtering...

printtree-fty

books/std/strings/printtree-fty
other
(in-package "STR")
other
(include-book "printtree-concat")
other
(include-book "centaur/fty/fixequiv" :dir :system)
other
(local (include-book "printtree-fix"))
other
(deffixtype printable
  :pred printable-p
  :fix printable-fix
  :equiv printable-equiv
  :define t)
other
(deffixtype printtree
  :pred printtree-p
  :fix printtree-fix
  :equiv printtree-equiv
  :define t)
other
(deffixequiv printable->str
  :args ((x printable-p))
  :hints (("Goal" :in-theory (enable printable->str printable-fix))))
other
(deffixequiv printable-empty-p$inline
  :args ((x printable-p))
  :hints (("Goal" :in-theory (enable printable-empty-p printable-fix))))
other
(deffixequiv printtree->strlist
  :args ((x printtree-p))
  :hints (("Goal" :in-theory (enable printtree->strlist printtree-fix))))
other
(deffixequiv printtree->str
  :args ((x printtree-p))
  :hints (("Goal" :in-theory (enable printtree->str printtree-fix))))
other
(deffixequiv printtree->str-left2right
  :args ((x printtree-p))
  :hints (("Goal" :in-theory (enable printtree->str-left2right
       printtree-fix))))
other
(deffixequiv printtree-obviously-empty-p$inline
  :args ((x printtree-p))
  :hints (("Goal" :in-theory (enable printtree-obviously-empty-p
       printtree-fix))))
other
(deffixequiv printtree-concat
  :args ((x printtree-p) (y printtree-p))
  :hints (("Goal" :in-theory (enable printtree-concat))))