|
|
|---|
|
|
|
|---|
List of built-in ACL2 functions natively implemented in AIJ.
Currently these are the ACL2 primitive functions plus nonnegative-integer-quotient and string-append.
Definition:
(defconst *aij-natives* (append (strip-cars *primitive-formals-and-guards*) (list 'nonnegative-integer-quotient 'string-append 'len 'char 'hard-error)))