|
|
|---|
|
|
|
|---|
(alternation-fix x) is a usual ACL2::fty list fixing function.
(alternation-fix x) → fty::newx
In the logic, we apply concatenation-fix to each member of the x. In the execution, none of that is actually necessary and this is just an inlined identity function.