		Search-engine friendly clone of the ACL2 documentation.

Struct-recursion

Topdecl-struct-graph

Struct graph induced by a top-level definition.

Signature
(topdecl-struct-graph decl) → graph
Arguments: decl — Guard (topdeclp decl).
Returns: graph — Type (alistp graph).

A function declaration induces nothing for this graph. A struct declaration contributes a graph.

Definitions and Theorems

Function: topdecl-struct-graph

(defun topdecl-struct-graph (decl)
  (declare (xargs :guard (topdeclp decl)))
  (let ((__function__ 'topdecl-struct-graph))
    (declare (ignorable __function__))
    (topdecl-case decl
                  :function nil
                  :struct (structdecl-struct-graph decl.get)
                  :mapping nil)))

Theorem: alistp-of-topdecl-struct-graph

(defthm alistp-of-topdecl-struct-graph
  (b* ((graph (topdecl-struct-graph decl)))
    (alistp graph))
  :rule-classes :rewrite)

Theorem: topdecl-struct-graph-of-topdecl-fix-decl

(defthm topdecl-struct-graph-of-topdecl-fix-decl
  (equal (topdecl-struct-graph (topdecl-fix decl))
         (topdecl-struct-graph decl)))

Theorem: topdecl-struct-graph-topdecl-equiv-congruence-on-decl

(defthm topdecl-struct-graph-topdecl-equiv-congruence-on-decl
  (implies (topdecl-equiv decl decl-equiv)
           (equal (topdecl-struct-graph decl)
                  (topdecl-struct-graph decl-equiv)))
  :rule-classes :congruence)