### Lexical conventions

Single-line
comments take the form "`// ... \n`".

Lower-case identifiers are any sequence of alphanumeric characters
that start with a lower-case identifiers (`a-z`).
Upper-case identifiers are any sequence of alphanumeric characters, underscores,
and single quotes (`'`) that start with a capital letter (`A-Z`).
A string of numeric characters (`0-9`) is a natural number literal,
and the quote character (`"`),
followed by a series of alphanumeric characters,
underscores, single quotes, and spaces and terminated by another
quote character is a string literal.

Reserved identifiers are:

- Negation
`not` and existential quantification `Ex`.
- Built-in types and kinds
`t`,
`nat`,
`string`,
`world`,
`type`,
and `rel`.

An underscore is treated as a special upper-case identifier
that we do not care about.

### Terms and atomic propositions

Terms and atomic propositions are both formed from the same very basic
grammar; the only interesting special case is addition, which computes
the addition of two known natural numbers.

UCID ::= (upper-case identifiers) | _
ID ::= (lower-case identifiers) | (natural number literals) | (string literals)
TERM ::= UCID | ID | TERM TERM | TERM + TERM

### Propositions and rules

Premises and conclusions are basically a series of atomic propositions,
though some premises may be negated or be the special comparison
propositions. Equality and equality are valid on terms of any type,
but inequality can only be used on terms of the `nat` type of
natural numbers.

ATOM ::= ID | ATOM TERM
ATOMS ::= ATOM | ATOM, ATOMS
PAT ::= ATOM | Ex ID. PREM
PREM ::= PAT | not PAT
| TERM == TERM | TERM != TERM
| TERM < TERM | TERM <= TERM
| TERM => TERM | TERM > TERM
PREMS ::= PREM | PREM, PREMS
RULE ::= PREMS | PREMS -> ATOMS

### Classifiers, declarations, and the signature

ATYPE ::= t | nat | string | LCID // Atomic types
TYPE ::= ATYPE // Constant type
| ATYPE -> TYPE // Constructor type
| {LCID : ATYPE} TYPE // Named constructor type
KIND ::= ATYPE -> KIND // Argument
| {LCID : ATYPE} KIND // Named argument
| type // Type
| world // World
| rel @ ATOM // Forward-chaining proposition
DECL ::= LCID : TYPE. // New constant of a given type
| LCID : KIND. // New world/type/proposition
| RULE. // New rule
| LCID = PROPS @ WORLD. // Perform a computation
SIG ::= // Empty signature
| DECL SIG // Declaration

There is also a backwards-facing arrow `<-` that is syntatic
sugar for a forward-facing arrow with the front and back switched.

### Precedence

Application binds more tightly than anything else.

binds least tightly ---> = :
<- (left associative)
-> (right associative)
, (left associative)
@
== != > < >= <=
+ (left associative)
binds most tightly ---> (application)