Proofscape-flavored JSON

In Proofscape modules, assignment values are given in a relaxed and generalized form of JSON, which we call “Proofscape-flavored JSON,” or PF-JSON for short.

Strings

In PF-JSON, strings are largely like those in the Python programming language, in that:

• Four different delimiters are allowed:

  • """ (triple double quotes)

  • ''' (triple single quotes)

  • " (double quotes)

  • ' (single quotes)

• Inside double-quoted strings, the delimiter can occur if escaped, as in \".

• Inside single-quoted strings, the delimiter can occur if escaped, as in \'.

However, strings in Proofscape modules differ from those in Python in that:

• Any type of string, including double-quoted (") and single-quoted ('), may span multiple lines, i.e. may contain newline characters.

Unquoted keys

As in JavaScript, when objects are given by key-value pairs, the keys may be given by strings with quotation marks around them, or the quotation marks may be omitted when the contents are of a particularly simple form; namely, when they consist only of alphanumerics and underscores, and when the first character is not a digit.

Example:

{
    "foo": 42,
    bar: 43
}

Trailing commas

When you write a list or object, you may include a trailing comma after the last entry.

Example:

{
    foo: [42, 84,],
    bar: null,
}

Libpaths

A libpath is a valid primitive, along with the usual primitives, i.e. strings, integers, floats, and the constants true, false, and null.

Example:

Listing 50 Using a libpath as a primitive

from ... import Pf

foo = {
    great_proof: true,
    favorite_node: Pf.A10,
}

In Listing 50, the libpath Pf.A10 is used as a primitive. (In particular, it is not a string, since it is not surrounded by quotation marks of any kind.)