diff options
| -rw-r--r-- | docs/tutorial.md | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/docs/tutorial.md b/docs/tutorial.md index 1c82cb6..fa6fc04 100644 --- a/docs/tutorial.md +++ b/docs/tutorial.md @@ -18,12 +18,12 @@ You can define the following: Kind | Pattern | Example ---- | ---- | ---- -Nouns | `<VARIABLE> is a <NOUN PATTERN> iff <STATEMENT>` | `$k$ is a divisor of $n$ iff ...` -Adjectives | `<VARIABLE> is <ADJECTIVE PATTERN> iff <STATEMENT>` | `$n$ is divisible by $k$ iff ...` -Verbs | `<VARIABLE> <VERB PATTERN> iff <STATEMENT>` | `$k$ divides $n$ iff ...` +Nouns | `<VAR> is a <NOUN PATTERN> iff <STATEMENT>` | `$k$ is a divisor of $n$ iff ...` +Adjectives | `<VAR> is <ADJECTIVE PATTERN> iff <STATEMENT>` | `$n$ is divisible by $k$ iff ...` +Verbs | `<VAR> <VERB PATTERN> iff <STATEMENT>` | `$k$ divides $n$ iff ...` Operators | `$<MIXFIX PATTERN> = <TERM>$` | `$n + k = ...$` -Relators | `$<RELATOR PATTERN>$ iff <STATEMENT>` | `$n < k$ iff ...` -Predicate | `$\<PREDICATE COMMAND>{<ARG 1>}...{<ARG n>} iff <STATEMENT>` | `$\Cong{a}{b}{c}{d}$ iff ...` +Relators | `$<VAR> <RELATOR PATTERN> <VAR>$ iff <STATEMENT>` | `$n < k$ iff ...` +Predicates | `$\<PREDICATE COMMAND>{<VAR>}...{<VAR>} iff <STATEMENT>` | `$\Cong{a}{b}{c}{d}$ iff ...` Source fixity declarations are line-leading pragmas such as `%! infixl 4`. User declarations may use literal levels 0 through 7; the two higher internal @@ -32,6 +32,9 @@ authority separate from exact proof/declaration validation. Its authorization summary lists only direct source axioms and syntactic `Omitted` sites, not facts that merely inherit their safety. +## Abbreviations + +Abbreviationas are definitions that are always automatically expanded by Felix. ## Proof vernacular |