		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-literal

Check if a literal is statically well-formed.

Signature
(check-literal lit) → result
Arguments: lit — Guard (literalp lit).
Returns: result — Type (type-resultp result).

A literal is always well-formed, but we have this function so that we can return a type result, uniformly with other kinds of expressions. A literal never engenders any proof obligation. A literal is always single-valued.

Definitions and Theorems

Function: check-literal

(defun check-literal (lit)
  (declare (xargs :guard (literalp lit)))
  (let ((__function__ 'check-literal))
    (declare (ignorable __function__))
    (make-type-result-ok :types (list (literal-type lit))
                         :obligations nil)))

Theorem: type-resultp-of-check-literal

(defthm type-resultp-of-check-literal
  (b* ((result (check-literal lit)))
    (type-resultp result))
  :rule-classes :rewrite)

Theorem: check-literal-of-literal-fix-lit

(defthm check-literal-of-literal-fix-lit
  (equal (check-literal (literal-fix lit))
         (check-literal lit)))

Theorem: check-literal-literal-equiv-congruence-on-lit

(defthm check-literal-literal-equiv-congruence-on-lit
  (implies (literal-equiv lit lit-equiv)
           (equal (check-literal lit)
                  (check-literal lit-equiv)))
  :rule-classes :congruence)