		Search-engine friendly clone of the ACL2 documentation.

Group-literal-affine

Group-literal-affine->x

Get the x field from a group-literal-affine.

Signature
(group-literal-affine->x lit) → x
Arguments: lit — Guard (group-literalp lit).
Returns: x — Type (coordinatep x).

This is an ordinary field accessor created by fty::defprod.

Definitions and Theorems

Function: group-literal-affine->x$inline

(defun group-literal-affine->x$inline (lit)
  (declare (xargs :guard (group-literalp lit)))
  (declare (xargs :guard (equal (group-literal-kind lit)
                                :affine)))
  (let ((__function__ 'group-literal-affine->x))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((lit (and (equal (group-literal-kind lit) :affine)
                        lit)))
           (coordinate-fix (std::da-nth 0 (cdr lit))))
         :exec (std::da-nth 0 (cdr lit)))))

Theorem: coordinatep-of-group-literal-affine->x

(defthm coordinatep-of-group-literal-affine->x
  (b* ((x (group-literal-affine->x$inline lit)))
    (coordinatep x))
  :rule-classes :rewrite)

Theorem: group-literal-affine->x$inline-of-group-literal-fix-lit

(defthm group-literal-affine->x$inline-of-group-literal-fix-lit
  (equal (group-literal-affine->x$inline (group-literal-fix lit))
         (group-literal-affine->x$inline lit)))

Theorem: group-literal-affine->x$inline-group-literal-equiv-congruence-on-lit

(defthm
 group-literal-affine->x$inline-group-literal-equiv-congruence-on-lit
 (implies (group-literal-equiv lit lit-equiv)
          (equal (group-literal-affine->x$inline lit)
                 (group-literal-affine->x$inline lit-equiv)))
 :rule-classes :congruence)

Theorem: group-literal-affine->x-when-wrong-kind

(defthm group-literal-affine->x-when-wrong-kind
  (implies (not (equal (group-literal-kind lit)
                       :affine))
           (equal (group-literal-affine->x lit)
                  (coordinate-fix nil))))