• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
      • Deftagsum
      • Defprod
      • Defflexsum
      • Defbitstruct
      • Deflist
      • Defalist
      • Defbyte
      • Defresult
      • Deffixtype
      • Deffixequiv
      • Fty-discipline
      • Defoption
      • Fty-extensions
      • Defsubtype
        • Defsubtype-implementation
          • Defsubtype-fn
          • Defsubtype-macro-definition
      • Deftypes
      • Defflatsum
      • Deflist-of-len
      • Defbytelist
      • Specific-types
      • Defset
      • Fty::basetypes
      • Defvisitors
      • Deffixtype-alias
      • Defomap
      • Deffixequiv-sk
      • Defunit
      • Deffixequiv-mutual
      • Fty::baselists
      • Defmap
    • Std/util
    • Apt
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Defsubtype

Defsubtype-implementation

Implementation of defsubtype.

Subtopics

Defsubtype-fn

Events generated by defsubtype.

Defsubtype-macro-definition

Definition of the defsubtype macro.