Specify type signatures for polymorphic functions
(sig nthcdr (nat (listof :a)) => (listof :a))
(sig binary-append ((listof :a) (listof :a)) => (listof :a))
(sig nth (nat (listof :a)) => :a
:satisfies (< x1 (len x2)))
;; xi corresponds to the ith type appearing in the sig form. For example,
;; x1 corresponds to nat and x2 to (listof :a)
(sig fun-name arg-types => return-type
where arg-types is a list of defdata type expressions
and return-type is a defdata type expression with the
added capability of referring to type variables, which in our
syntax are represented using keyword symbols :a, :b, :c, ....
Note: sig is currently limited to only 12 type variables.
Check :pe *allowed-type-vars* to view them. We have never encountered
type signatures with more than 3 type variables, so we hope that this is
not a limitation in practice. There are several other limitations
we impose on sig. If you would like more comprehensive
support, contact Pete and Harsh.
The following keyword arguments are supported by the sig macro:
- :satisfies -- specify additional dependent type hypotheses.
- :hints -- ACL2::hints option to the generic type signature.
- :gen-rule-classes -- ACL2::rule-classes option to the generic type signature.
- :rule-classes -- ACL2::rule-classes option to the generated theorems.
- :verbose -- for debugging.