		Search-engine friendly clone of the ACL2 documentation.

Expr-tycompat

Make-expr-tycompat

Basic constructor macro for expr-tycompat structures.

Syntax

(make-expr-tycompat [:type1 <type1>] 
                    [:type2 <type2>])

This is the usual way to construct expr-tycompat structures. It simply conses together a structure with the specified fields.

This macro generates a new expr-tycompat structure from scratch. See also change-expr-tycompat, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-expr-tycompat

(defmacro make-expr-tycompat (&rest args)
  (std::make-aggregate 'expr-tycompat
                       args '((:type1) (:type2))
                       'make-expr-tycompat
                       nil))

Function: expr-tycompat

(defun expr-tycompat (type1 type2)
  (declare (xargs :guard (and (tynamep type1) (tynamep type2))))
  (declare (xargs :guard t))
  (let ((__function__ 'expr-tycompat))
    (declare (ignorable __function__))
    (b* ((type1 (mbe :logic (tyname-fix type1)
                     :exec type1))
         (type2 (mbe :logic (tyname-fix type2)
                     :exec type2)))
      (cons :tycompat (list type1 type2)))))