A few examples of trickier syntax constructs¶
Math¶
\[\sum_{k=1}^\infty \frac{1}{k^2} = \frac{\pi^2}{6}\]
It's also easy to define special environments when needed:
\[
\newcommand{\WF}[2]{{\cal W\!F}(#1)[#2]}
\newcommand{\WFE}[1]{\WF{E}{#1}}
\newcommand{\WT}[4]{#1[#2] \vdash #3 : #4}
\newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}}
\newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}}
\newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3}
\newcommand{\subst}[3]{#1\{#2/#3\}}
\newcommand{\mto}{.\;}
\newcommand{\kw}[1]{\textsf{#1}}
\newcommand{\lb}{\lambda}
\newcommand{\Sort}{\cal S}
\newcommand{\alors}{\textsf{then}}
\newcommand{\alter}{\textsf{alter}}
\newcommand{\bool}{\textsf{bool}}
\newcommand{\conc}{\textsf{conc}}
\newcommand{\cons}{\textsf{cons}}
\newcommand{\consf}{\textsf{consf}}
\newcommand{\emptyf}{\textsf{emptyf}}
\newcommand{\EqSt}{\textsf{EqSt}}
\newcommand{\false}{\textsf{false}}
\newcommand{\filter}{\textsf{filter}}
\newcommand{\forest}{\textsf{forest}}
\newcommand{\from}{\textsf{from}}
\newcommand{\hd}{\textsf{hd}}
\newcommand{\haslength}{\textsf{has\_length}}
\newcommand{\length}{\textsf{length}}
\newcommand{\List}{\textsf{list}}
\newcommand{\nilhl}{\textsf{nil\_hl}}
\newcommand{\conshl}{\textsf{cons\_hl}}
\newcommand{\ident}{\textsf{ident}}
\newcommand{\nat}{\textsf{nat}}
\newcommand{\nO}{\textsf{O}}
\newcommand{\nS}{\textsf{S}}
\newcommand{\node}{\textsf{node}}
\newcommand{\Nil}{\textsf{nil}}
\newcommand{\Prop}{\textsf{Prop}}
\newcommand{\Set}{\textsf{Set}}
\newcommand{\si}{\textsf{if}}
\newcommand{\sinon}{\textsf{else}}
\newcommand{\Str}{\textsf{Stream}}
\newcommand{\tl}{\textsf{tl}}
\newcommand{\tree}{\textsf{tree}}
\newcommand{\true}{\textsf{true}}
\newcommand{\Type}{\textsf{Type}}
\newcommand{\unfold}{\textsf{unfold}}
\newcommand{\zeros}{\textsf{zeros}}
\newcommand{\even}{\textsf{even}}
\newcommand{\odd}{\textsf{odd}}
\newcommand{\evenO}{\textsf{even\_O}}
\newcommand{\evenS}{\textsf{even\_S}}
\newcommand{\oddS}{\textsf{odd\_S}}
\newcommand{\Prod}{\textsf{prod}}
\newcommand{\Pair}{\textsf{pair}}
\]
- Prod-Type\[\frac{% \WTEG{T}{\Type(i)}% \hspace{3em}% \WTE{\Gamma::(x:T)}{U}{\Type(i)}% }{% \WTEG{\forall~x:T,U}{\Type(i)}% }\]
Interaction with CoqTop¶
Done using a new directive, .. coqtop::. It takes arguments saying what to
display (inputs, outputs, or both), whether to reset the environment (and
optionally whether to undo the commands of that block), highlights the input
with CoqDoc and the output by translating ANSI sequences produced by CoqTop.
The arguments are for input and output are "in", "out", "all", and "none".
- Require Import Nat.
- Print sub.
- sub = fix sub (n m : nat) {struct n} : nat := match n with | 0 => n | S k => match m with | 0 => n | S l => sub k l end end : nat -> nat -> nat Argument scopes are [nat_scope nat_scope]
- Definition a := 1.
- a is defined
- Definition a := 2.
- Toplevel input, characters 0-18: > Definition a := 2. > ^^^^^^^^^^^^^^^^^^ Error: a already exists.
Grammars¶
Sphinx has a construct for grammars, and it can cross-reference tokens between
grammars, too (curlies). For example:
Parsing rules¶
top ::=blocksEOF blocks ::=block((whitespace)?block)* block ::=atomic|hole|repeat|curliesrepeat ::=LGROUP(ATOM)?WHITESPACEblocks(WHITESPACE)?RBRACEcurlies ::=LBRACE(whitespace)?blocks(whitespace)?RBRACEwhitespace ::=WHITESPACEatomic ::=ATOMhole ::=ID
Lexing rules¶
LGROUP ::= { [+*?]
LBRACE ::= {
RBRACE ::= }
ATOM ::= ~[@{} ]+
ID ::= @ [a-zA-Z0-9_]+
WHITESPACE ::= ( )+