ACL2 predicate denoted by an ATJ type.
(atj-type-to-pred type) → pred
The predicate recognizes the values of the type.
The predicates for the
Function:
(defun atj-type-to-pred (type) (declare (xargs :guard (atj-typep type))) (let ((__function__ 'atj-type-to-pred)) (declare (ignorable __function__)) (atj-type-case type :acl2 (atj-atype-case type.get :integer 'integerp :rational 'rationalp :number 'acl2-numberp :character 'characterp :string 'stringp :symbol 'symbolp :boolean 'booleanp :cons 'consp :value '(lambda (_) 't)) :jprim (primitive-type-case type.get :boolean 'boolean-valuep :char 'char-valuep :byte 'byte-valuep :short 'short-valuep :int 'int-valuep :long 'long-valuep :float 'float-valuep :double 'double-valuep) :jprimarr (primitive-type-case type.comp :boolean 'boolean-arrayp :char 'char-arrayp :byte 'byte-arrayp :short 'short-arrayp :int 'int-arrayp :long 'long-arrayp :float 'float-arrayp :double 'double-arrayp))))
Theorem:
(defthm pseudo-termfnp-of-atj-type-to-pred (b* ((pred (atj-type-to-pred type))) (pseudo-termfnp pred)) :rule-classes :rewrite)
Theorem:
(defthm atj-type-to-pred-of-atj-type-fix-type (equal (atj-type-to-pred (atj-type-fix type)) (atj-type-to-pred type)))
Theorem:
(defthm atj-type-to-pred-atj-type-equiv-congruence-on-type (implies (atj-type-equiv type type-equiv) (equal (atj-type-to-pred type) (atj-type-to-pred type-equiv))) :rule-classes :congruence)