		Search-engine friendly clone of the ACL2 documentation.

Transformation-tools

Split-all-gso

A transformation to split all global struct objects.

Introduction

This is a meta transformation which repeatedly applies splitgso to any global struct object it can.

General Form

(split-all-gso const-old
               const-new
  )

Inputs

const-old

Specifies the code to be transformed.
This must be a symbol that names an existing ACL2 constant that contains a validated code ensemble, i.e. a value of type code-ensemble whose translation unit ensemble results from validation, and in particular containing validation information. This constant could result from c$::input-files, or from some other transformation.

const-new

Specifies the name of the constant for the transformed code.
This must be a symbol that is valid name for a new ACL2 constant.

Subtopics

Split-all-gso-implementation: Implementation of split-all-gso.