Command:def or eval - Walnut-Theorem-Prover/Walnut GitHub Wiki

The "def" and "eval" commands are identical. The syntax for them is as follows:

def <name> <predicate>

Results saved in: Result/, Automata Library/.

For example, to create and save an automaton that accepts an input of "a" if and only if a is the msd_2 representation of 4 (i.e. it belongs to 0*100), one can create the following automaton:

def four "a=4";

In previous versions of Walnut, word automata names in eval/def commands could not begin with A, E, or I. This restriction has now been lifted using a new delimiter for word automata: putting "." (without quotation marks) before the name of a word automaton now signals that the following string of characters is the name of the word automaton. If there is a word automaton named AUTOMATON, you can write ".AUTOMATON" (without quotation marks) to refer to it in eval/def commands. For example, the following is now valid:

def test ".AUTOMATON[n] = @1";

Please refer to section 7 of the Arxiv manual for a more detailed description of the "def"/"eval" commands and what one can do with them.