|
|
|---|
|
|
|
|---|
A translator from the JSON parser's output to our model of JSON values.
The JSON parser in
Thus, here we provide a translator
from the parser's output to the JSON values.
Since at the time that this translator was first written
the parser did not include a type (i.e. recognizer) for its output,
the translator is defined over all possible ACL2 values,
but it returns an error if given something
that does not belong to the parser's implicit output type.
After that, recognizers have been added in