• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
      • Deftagsum
      • Defprod
      • Defflexsum
      • Defbitstruct
      • Deflist
      • Defalist
      • Defbyte
      • Defresult
      • Deffixtype
      • Deffixequiv
      • Fty-discipline
      • Defoption
      • Fty-extensions
      • Defsubtype
      • Deftypes
      • Defflatsum
      • Deflist-of-len
        • Deflist-of-len-implementation
      • Defbytelist
      • Defset
      • Fty::basetypes
      • Specific-types
      • 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

• Fty-extensions
• Fty
• Deflist

Deflist-of-len

Introduce a fixtype of lists of a specified length.

Introduction

deflist introduces fixtypes of lists of arbitrary lengths. Given such a fixtype, the macro deflist-of-len introduces a fixtype of those lists that have a specified length, along with some theorems that relate the recognizers, fixers, and equivalences of the two fixtypes.

The lists may be true or dotted, depending on the :true-listp option used in deflist. The macro deflist-of-len preserves that option.

Future versions of this macro could support richer constraints on list length than equality with a certain value, e.g. introduce fixtypes of lists of lengths below a certain value.

General Form

(deflist-of-len type
                :list-type ...
                :length ...
                :pred ...
                :fix ...
                :equiv ...
                :parents ...
                :short ...
                :long ...
  )

Inputs

type

A symbol that specifies the name of the fixtype.

:list-type

A symbol that names a fixtype previously introduced via deflist. This is the fixtype of the lists of arbitrary lengths, which are a superset of the lists of the generated fixtype.

The recognizer, fixer, and equivalence of the list fixtype must be all guard-verified. Let list-pred, list-fix and list-equiv be their names.

This input must be supplied; there is no default.

:length

A non-negative integer that specifies the length of the lists.

This input must be supplied; there is no default.

:pred

A symbol that specifies the name of the recognizer for type. If this is nil (the default), the name of the recognizer is type followed by -p.

:fix

A symbol that specifies the name of the fixer for type. If this is nil (the default), the name of the fixer is type followed by -fix.

:equiv

A symbol that specifies the name of the equivalence for type. If this is nil (the default), the name of the equivalence is type followed by -equiv.

:parents
:short
:long

These, if present, are added to the XDOC topic generated for the fixtype.

Generated Events

pred

The recognizer for the fixtype, guard-verified.

booleanp-of-pred

A rewrite rule saying that pred is boolean-valued.

list-pred-when-pred-rewrite
list-pred-when-pred-forward

A rewrite rule and a forward chaining rule saying that a value satisfies list-pred when it satisfies pred.

len-when-pred-tau

A tau system rule saying that if a value satisfies pred then its length is the one specified by :length.

fix

The fixer for the fixtype, guard-verified.

It fixes values outside of pred by applying first take with the number specified by :length and then list-fix to the result.

pred-of-fix

A rewrite rule saying that fix always returns a value that satisfies pred.

fix-when-pred

A rewrite rule saying that fix disappears when its argument satisfies pred.

type
equiv

The fixtype, via a call of deffixtype that also introduces the equivalence equiv.

The above items are generated with XDOC documentation.

Subtopics

Deflist-of-len-implementation

Implementation of deflist-of-len.