Atj-gen-deep-term
Generate Java code to build a deeply embedded ACL2 term.
- Signature
(atj-gen-deep-term term jvar-value-base
jvar-value-index jvar-term-base
jvar-term-index jvar-lambda-base
jvar-lambda-index guards$)
→
(mv block expr
new-jvar-value-index new-jvar-term-index
new-jvar-lambda-index)
- Arguments
- term — Guard (pseudo-termp term).
- jvar-value-base — Guard (stringp jvar-value-base).
- jvar-value-index — Guard (posp jvar-value-index).
- jvar-term-base — Guard (stringp jvar-term-base).
- jvar-term-index — Guard (posp jvar-term-index).
- jvar-lambda-base — Guard (stringp jvar-lambda-base).
- jvar-lambda-index — Guard (posp jvar-lambda-index).
- guards$ — Guard (booleanp guards$).
- Returns
- block — Type (jblockp block).
- expr — Type (jexprp expr).
- new-jvar-value-index — Type (posp new-jvar-value-index), given (posp jvar-value-index).
- new-jvar-term-index — Type (posp new-jvar-term-index), given (posp jvar-term-index).
- new-jvar-lambda-index — Type (posp new-jvar-lambda-index), given (posp jvar-lambda-index).
