Changeset 3517 for Papers


Ignore:
Timestamp:
Nov 18, 2014, 12:02:04 PM (4 years ago)
Author:
mulligan
Message:

more about matita

Location:
Papers/jar-assembler-2014
Files:
2 edited

Legend:

Unmodified
Added
Removed

  • Papers/jar-assembler-2014/boender-jar-2014.tex

    r3516 r3517  
    1616\usepackage[ttdefault=true]{AnonymousPro}
    1717
     18\newcommand{\All}[1]{\forall{#1}.\;}
    1819\newcommand{\deffont}[1]{\textbf{#1}}
     20\newcommand{\lam}[1]{\lambda{#1}.\;}
     21\newcommand{\todo}[1]{\ensuremath{\texttt{[#1]}}}
    1922
    2023\bibliographystyle{alpha}
    … …  
    5760
    5861Matita is a theorem prover based on a variant of the Calculus of (Co-)inductive Constructions~\cite{asperti:user:2007}.
    59 The system features a full spectrum of dependent types and (co-)inductive families, as well as a sophisticated system of coercions, all of which we exploit in the formalisation described in this paper.
    60 
    61 Matita's syntax is largely similar to the syntaxes of mainstream functional programming languages such as OCaml.
     62The system features a full spectrum of dependent types and (co-)inductive families, as well as a sophisticated system of coercions, all of which we exploit in the formalisation described herein.
     63
     64Matita's syntax is largely similar to the syntaxes of mainstream functional programming languages such as OCaml or Standard ML, and the type theory that Matita implements is very similar to that of Coq~\cite{coq:2004} and Agda~\cite{bove:brief:2009}.
    6265Nevertheless, we provide a brief explanation of the main syntactic and type-theoretic features of Matita that will be needed to follow the body of the paper:
    6366\begin{itemize}
    6467\item
    65 Non-recursive functions and definitions are introduced via the \texttt{definition} keyword, whilst recursive functions are introduced with \texttt{let rec}.
     68Non-recursive functions and definitions are introduced via the \texttt{definition} keyword whilst recursive functions are introduced with \texttt{let rec}.
    6669Mutually recursive functions are separated via the \texttt{and} keyword.
     70Matita checks that all recursive functions are terminating before being admitted.
    6771\item
    6872Matita has an infinite hierarchy of type universes.
    69 A single impredicative universe of types, \texttt{Prop}, exists at the base of this hierarchy.
    70 An infinite series of predicative universes, \texttt{Type[0]} : \texttt{Type[1]} : \texttt{Type[2]}, and so on and so forth, sits atop \texttt{Prop}.
    71 Matita, unlike Coq~\cite{coq:2004} or Agda~\cite{bove:brief:2009}, implements no form of typical ambiguity or universe polymorphism, with explicit concrete universe levels being preferred instead.
     73A single \emph{impredicative} universe of types, \texttt{Prop}, exists at the base of this hierarchy.
     74An infinite series of \emph{predicative} universes, \texttt{Type[0]} : \texttt{Type[1]} : \texttt{Type[2]}, and so on and so forth, sits atop \texttt{Prop}.
     75Matita, unlike Coq or Agda, implements no form of typical ambiguity or universe polymorphism, with explicit concrete universe levels being preferred instead.
    7276\item
    7377Matita's type theory plays host to a rich and expressive higher-order logic.
    74 Constant \texttt{True} and \texttt{False} represent truth and (constructive) falsity in \texttt{Prop} respectively.
    75 Inductive families in \texttt{Prop} encode conjunction and disjunction---$\mathtt{P \wedge Q}$ and $\mathtt{P \vee Q}$ respectively---also.
     78Constant \texttt{True} and \texttt{False} represent truth and falsity in \texttt{Prop} respectively.
     79Two inductive families in \texttt{Prop} encode conjunction and disjunction---$\mathtt{P \wedge Q}$ and $\mathtt{P \vee Q}$ respectively.
    7680As is usual, implication and universal quantification are identified with the dependent function space ($\Pi$ types), whereas (constructive) existential quantification is encoded as a dependent sum (a $\Sigma$-type).
    77 \item
    78 Inductive families are introduced via the \texttt{inductive} keyword with named constructor declarations separated with a bar.
     81We write $\All{x : \phi}\psi$ for the dependent function space, and abbreviate this as $\phi \rightarrow \psi$ when $x \not\in fv(\psi)$ as usual.
     82\item
     83Inductive and coinductive families are introduced via the \texttt{inductive} and \texttt{coinductive} keywords respectively, with named constructor declarations separated with a bar.
    7984Mutually inductive data family declarations are separated via \texttt{with}.
     85In the following declaration
     86\begin{lstlisting}
     87inductive I ($P_1$ : $\tau_1$) $\ldots$ ($P_n$ : $\tau_n$) : $\phi_1 \rightarrow \ldots \rightarrow \phi_m \rightarrow \phi$ := $\ldots$
     88\end{lstlisting}
     89we call $P_i$ for $0 \leq i \leq n$ the \deffont{parameters} of \texttt{I} and $\phi_j$ for $0 \leq j \leq m$ the \deffont{indices} of \texttt{I}.
     90Matita checks that constructors have strictly-positive types before admitting an inductive family.
    8091\item
    8192Records are introduced with the \texttt{record} keyword.
    … …  
    89100  | mk_R : nat -> R.
    90101\end{lstlisting}
    91 In particular, declaration of a record \texttt{R} causes a \deffont{constructor} function \texttt{mk\_R} to be entered into the global context as a side effect.
    92 \deffont{Projections}, one for each of the record's fields, are also registered in the global context.
    93 In the example record above, \texttt{F1} of type $R \rightarrow nat$ is registered as a field projection.
     102The declaration of a record \texttt{R} causes a \deffont{constructor} function \texttt{mk\_R} to be entered into the global context as a side effect.
     103\deffont{Projections}, one for each of the record's fields, are also registered in the global context, and in the example record above \texttt{F1} of type $R \rightarrow nat$ is registered as a field projection.
     104A record field's type may depend on fields declared earlier in the record.
    94105
    95106Record fields may be marked as coercions.
    … …  
    97108\begin{lstlisting}
    98109record S : Type[1] :=
    99   {
    100     Carrier :> Type[0];
    101     op : Carrier -> Carrier -> Carrier
    102   }
    103 \end{lstlisting}
    104 the field \texttt{Carrier} is declared to be a coercion with `\texttt{:>}', and the field projection \texttt{Carrier} may be omitted where it could be successfully inferred by Matita's typechecker, thus facilitating the common mathematical practice of confusing a mathematical structure with its underlying carrier set.
    105 \item
    106 There is provision for customising syntax (through Unicode).
    107 Matita has a type-directed system of overloading and resolution so that definitions and proofs look `natural'.
     110{
     111  Carrier :> Type[0];
     112  op : Carrier -> Carrier -> Carrier
     113}
     114\end{lstlisting}
     115the field \texttt{Carrier} is declared to be a coercion with `\texttt{:>}' with the effect that the field projection \texttt{Carrier} may be omitted where it could be successfully inferred by Matita.
     116Field coercions facilitate the informal but common mathematical practice of intentionally confusing a structure with its underlying carrier set.
     117\item
     118Terms may be freely omitted, allowing the user to write down partial types and terms.
     119A question mark, \texttt{?}, denotes a single term that has been omitted by the user.
     120Some omitted terms can be deduced by Matita's refinement system.
     121Other, more complex goals arising from omitted terms may require user input to solve, in which case a proof obligation is opened for each term that cannot be deduced automatically.
     122Three consecutive dots, \texttt{$\ldots$}, denote multiple terms or types that have been omitted.
     123\item
     124Pattern matching is carried out with a \texttt{match} expression.
     125We may sometimes fully annotate a \texttt{match} expression with its return type.
     126This is especially useful when working with indexed families of types or with invariants, expressed as types, on functions.
     127In the following
     128\begin{lstlisting}
     129match t return $\lam{x}x = 0 \rightarrow bool$ with
     130[ 0    $\Rightarrow$ $\lam{prf_1}P_1$
     131| S m $\Rightarrow$ $\lam{prf_2}P_2$
     132] (refl $\ldots$ t)
     133\end{lstlisting}
     134the \texttt{0} branch of the \texttt{match} expression returns a function from $0 = 0$ to \texttt{bool}, whereas the \texttt{S m} branch of the \texttt{match} expression returns a function from \texttt{S m = 0} to \texttt{bool}.
     135In both cases the annotated return type $\lam{x}x = 0 \rightarrow bool$ has been specialised given new information about \texttt{t} revealed by the act of pattern matching.
     136The entire term, with \texttt{match} expression applied to \texttt{refl $\ldots$ t}, has type \texttt{bool}.
     137\item
     138Matita features a liberal system of uniform coercions (distinct from the previously mentioned record field coercions).
     139\todo{dpm: more about coercions}
    108140\end{itemize}
     141Throughout, for reasons of clarity, conciseness, and readability, we may choose to simplify or omit parts of Matita code.
     142We will always ensure that these omissions do not mislead the reader.
    109143
    110144%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%

  • Papers/jar-assembler-2014/lst-grafite.tex

    r3470 r3517  
    99morekeywords={[2]include},
    1010%emph={[1]Type, Prop, nat, real}, emphstyle={[1]\textit},
    11 literate=       
    12         {->}{{$\to$}}3         
    13         {:>}{{$\mathrm{:>}$}}1         
    14         {>->}{{$\mapsto$}}2             
    15         {<=}{{$\leq$}}2                 
    16         {>=}{{$\geq$}}2         
    17         {<>}{{$\neq$}}1
    18         {\\/}{{$\vee$}}1               
    19         {<->}{{$\leftrightarrow$}}2
    20         {FORALL\ }{{$\forall\,$}}1             
    21         {EXISTS\ }{{$\exists\,$}}1
    22         {ALPHA}{{$\alpha$}}1
    23         {LAMBDA}{{$\lambda\,$}}1
    24         {\\lambda}{{$\lambda\,$}}1
    25         {LANGLE}{{$\langle$}}1
    26         {RANGLE}{{$\rangle$}}1
    27         {EQUIV}{{$\equiv$}}1
    28         {SIGMA}{{$\Sigma$}}1
    29         {PSI}{{$\Psi$}}1
    30         {DOTS}{{$\ldots$}}1
    31         {NOT}{{$\neg$}}1
    32         {\\in}{{$\in$}}1
    33         {𝟙}{{$\mathbf{1}$}}1
    34         {𝟘}{{$\mathbf{0}$}}1
    35         {/\\}{$\land$}1
    36         {×}{{$\times\,$}}2
    37         {\\x}{{$\times\,$}}2
    38         {≝}{{:=}}1
    39         {δ}{{$\delta$}}1
    40         {λ}{{$\lambda\,$}}1
    41         {≰}{{$\nleq\,$}}1
    42         {∨}{{$\lor\,$}}1
    43         {⋁}{{$\bigvee$}}1
    44         {≈}{{$\approx\,$}}1
    45         {∀}{{$\forall\,$}}1
    46         {∃}{{$\exists\,$}}1
    47         {⇝}{{$\leadsto\,$}}1
    48         {→}{{$\rightarrow\,$}}1
    49         {↔}{{$\leftrightarrow$}}1
    50         {∧}{{$\land\,$}}1
    51         {⋀}{{$\bigwedge$}}1
    52         {≤}{{$\leq\,$}}1
    53         {¬}{{$\lnot\,$}}1
    54         {≪}{{$\ll\,$}}1
    55         {≫}{{$\gg\,$}}1
    56         {⇒}{{$\,\Rightarrow\,\,$}}2
    57         {=>}{{$\,\Rightarrow\,\,$}}2
    58         {⇒_0}{{$\,\Rightarrow_0\,\,$}}2
    59         {=>_0}{{$\,\Rightarrow_0\,\,$}}2
    60         {⇒_1}{{$\,\Rightarrow_1\,$}}1
    61         {⇒_1.}{{$\,\Rightarrow_1\,$}}1
    62         {⇒_\\r1}{{$\,\Rightarrow_1^{r}\,$}}1
    63         {⇒_\\r2}{{$\,\Rightarrow_2^{r}\,$}}1
    64         {=>_1}{{$\,\Rightarrow_1\,$}}1
    65         {⇒_2}{{$\,\Rightarrow_2\,$}}1
    66         {⇒_\\o2}{{$\,\Rightarrow_2^o\,$}}1
    67         {⇒_\\c2}{{$\,\Rightarrow_2^c\,$}}1
    68         {⇒_\\c3}{{$\,\Rightarrow_3^c\,$}}1
    69         {⇒_\\obp2}{{$\,\Rightarrow_2^{obp}\,$}}1
    70         {⇒_\\bp1}{{$\,\Rightarrow_1^{bp}\,$}}1
    71         {⇒_\\bp2}{{$\,\Rightarrow_2^{bp}\,$}}1
    72         {⇒_\\obt2}{{$\,\Rightarrow_2^{obt}\,$}}1
    73         {⇒_2.}{{$\,\Rightarrow_2\,$}}1
    74         {=>_2}{{$\,\Rightarrow_2\,$}}1
    75         {=_1}{{$=$}}1
    76         {=_2}{{$=$}}1
    77         {⊢}{{$\vdash$}}1
    78         {⊩}{{$\Vdash\,$}}2
    79         {≬}{{$\between$}}2
    80         {><}{{$>\!\!\!\!\!<\,$}}2
    81         {⎻}{{$^-$}}1
    82         {⎻*}{{$^{-*}$}}1
    83         {\\sup\ ⎻}{{$\!^-\,$}}1
    84         {\\sup\ ⎻*}{{$\!^{-*}\,$}}1
    85         {\\sup\ *}{{$\!^{*}\,$}}1
    86         {^*}{{$\!^{*}\,$}}1
    87         {F*}{{F$^*$}}1
    88         {G*}{{G$^*$}}1
    89         {∘}{{$\circ\;$}}2
    90         {Ω}{{$\Omega$}}1
    91         {Ω^carrbt}{{$\Omega^{\mbox{carrbt}}$}}1
    92         {Ω^A}{{$\Omega^A$}}1
    93         {Ω^C}{{$\Omega^C$}}1
    94         {Ω^U}{{$\Omega^U$}}1
    95         {Ω^V}{{$\Omega^V$}}1
    96         {Ω^X}{{$\Omega^X$}}1
    97         {Ω^s}{{$\Omega^s$}}1
    98         {‡}{{$\ddagger$}}1
    99         {†}{{$\dagger$}}1
    100         {⊆}{{$\subseteq\,$}}2
    101         {♮}{{$\natural$}}1
    102         {∩}{{$\cap$}}2
    103         {∪}{{$\cup$}}2
    104         {⋂}{{$\bigcap$}}2
    105         {⋃}{{$\bigcup$}}2
    106         {∈}{{$\in\,$}}2
    107         {⎽o}{{$_o$}}1
    108         {⎽f}{{$_f$}}1
    109         {'\ \\sub\\c}{{'$\!_c$}}1
    110         {\ \\sub\\c}{{$_c$}}1
    111         {'\\sub\\c}{{'$\!_c$}}1
    112         {\\sub\\c}{{$_c$}}1
    113         {'\ \\sub\\f}{{'$\!_f$}}1
    114         {\ \\sub\\f}{{$_f$}}1
    115         {'\\sub\\f}{{'$\!_f$}}1
    116         {\\sub\\f}{{$_f$}}1
    117         {\\sup\ (form\ o)}{{$^{o_f}$}}1
    118         {\\sup\ (concr\ o)}{{$^{o_c}$}}1
    119         {(form\ o)}{{o$_f~$}}2
    120         {(concr\ o)}{{o$_c~$}}2
    121         {form\ o}{{o$_f~$}}2
    122         {concr\ o}{{o$_c~$}}2
    123         {Ω^(form\ o)}{{$\Omega^{o_f}~$}}2
    124         {Ω^(concr\ o)}{{$\Omega^{o_c}~$}}2
    125         {◊⎽t}{{$\Diamond_t$}}1
    126         {□⎽t}{{$\boxempty_t$}}1
    127         {⎽⇒}{{$_\Rightarrow$}}1
    128         {o_operator_of_operator}{{o\_op\_of\_op}}2
    129         {o_saturation_expansive}{{o\_sat\_expa}}2
    130         {o_saturation_monotone}{{o\_sat\_monot}}2
    131         {o_saturation_idempotent}{{o\_sat\_idemp}}2
    132         {o_continuous_relation_of_continuous_relation}{{ocrel\_of\_crel}}2
    133         {o_basic_topology_of_basic_topology}{{obtop\_of\_btop}}2
    134         {basic_topology_of_basic_pair}{{btop\_of\_bp}}2
    135         {o_basic_topology_of_o_basic_pair}{{o\_bt\_of\_o\_bp}}2
    136         {^-1}{{$^{-1}$}}1
    137         {^\ -1}{{$^{-1}$}}1
    138         {\ \\sup\ -1}{{$^{-1}$}}1
    139         {\\sup\ -1}{{$^{-1}$}}1
    140         {\ \\sup-1}{{$^{-1}$}}1
    141         {\\sup-1}{{$^{-1}$}}1
    142         {...}{{$\ldots$}}1
     11% literate=     
     12%       {->}{{$\to$}}3         
     13%       {:>}{{$\mathrm{:>}$}}1         
     14%       {>->}{{$\mapsto$}}2             
     15%       {<=}{{$\leq$}}2                 
     16%       {>=}{{$\geq$}}2         
     17%       {<>}{{$\neq$}}1
     18%       {\\/}{{$\vee$}}1               
     19%       {<->}{{$\leftrightarrow$}}2
     20%       {FORALL\ }{{$\forall\,$}}1             
     21%       {EXISTS\ }{{$\exists\,$}}1
     22%       {ALPHA}{{$\alpha$}}1
     23%       {LAMBDA}{{$\lambda\,$}}1
     24%       {\\lambda}{{$\lambda\,$}}1
     25%       {LANGLE}{{$\langle$}}1
     26%       {RANGLE}{{$\rangle$}}1
     27%       {EQUIV}{{$\equiv$}}1
     28%       {SIGMA}{{$\Sigma$}}1
     29%       {PSI}{{$\Psi$}}1
     30%       {DOTS}{{$\ldots$}}1
     31%       {NOT}{{$\neg$}}1
     32%       {\\in}{{$\in$}}1
     33%       {𝟙}{{$\mathbf{1}$}}1
     34%       {𝟘}{{$\mathbf{0}$}}1
     35%       {/\\}{$\land$}1
     36%       {×}{{$\times\,$}}2
     37%       {\\x}{{$\times\,$}}2
     38%       {≝}{{:=}}1
     39%       {δ}{{$\delta$}}1
     40%       {λ}{{$\lambda\,$}}1
     41%       {≰}{{$\nleq\,$}}1
     42%       {∨}{{$\lor\,$}}1
     43%       {⋁}{{$\bigvee$}}1
     44%       {≈}{{$\approx\,$}}1
     45%       {∀}{{$\forall\,$}}1
     46%       {∃}{{$\exists\,$}}1
     47%       {⇝}{{$\leadsto\,$}}1
     48%       {→}{{$\rightarrow\,$}}1
     49%       {↔}{{$\leftrightarrow$}}1
     50%       {∧}{{$\land\,$}}1
     51%       {⋀}{{$\bigwedge$}}1
     52%       {≤}{{$\leq\,$}}1
     53%       {¬}{{$\lnot\,$}}1
     54%       {≪}{{$\ll\,$}}1
     55%       {≫}{{$\gg\,$}}1
     56%       {⇒}{{$\,\Rightarrow\,\,$}}2
     57%       {=>}{{$\,\Rightarrow\,\,$}}2
     58%       {⇒_0}{{$\,\Rightarrow_0\,\,$}}2
     59%       {=>_0}{{$\,\Rightarrow_0\,\,$}}2
     60%       {⇒_1}{{$\,\Rightarrow_1\,$}}1
     61%       {⇒_1.}{{$\,\Rightarrow_1\,$}}1
     62%       {⇒_\\r1}{{$\,\Rightarrow_1^{r}\,$}}1
     63%       {⇒_\\r2}{{$\,\Rightarrow_2^{r}\,$}}1
     64%       {=>_1}{{$\,\Rightarrow_1\,$}}1
     65%       {⇒_2}{{$\,\Rightarrow_2\,$}}1
     66%       {⇒_\\o2}{{$\,\Rightarrow_2^o\,$}}1
     67%       {⇒_\\c2}{{$\,\Rightarrow_2^c\,$}}1
     68%       {⇒_\\c3}{{$\,\Rightarrow_3^c\,$}}1
     69%       {⇒_\\obp2}{{$\,\Rightarrow_2^{obp}\,$}}1
     70%       {⇒_\\bp1}{{$\,\Rightarrow_1^{bp}\,$}}1
     71%       {⇒_\\bp2}{{$\,\Rightarrow_2^{bp}\,$}}1
     72%       {⇒_\\obt2}{{$\,\Rightarrow_2^{obt}\,$}}1
     73%       {⇒_2.}{{$\,\Rightarrow_2\,$}}1
     74%       {=>_2}{{$\,\Rightarrow_2\,$}}1
     75%       {=_1}{{$=$}}1
     76%       {=_2}{{$=$}}1
     77%       {⊢}{{$\vdash$}}1
     78%       {⊩}{{$\Vdash\,$}}2
     79%       {≬}{{$\between$}}2
     80%       {><}{{$>\!\!\!\!\!<\,$}}2
     81%       {⎻}{{$^-$}}1
     82%       {⎻*}{{$^{-*}$}}1
     83%       {\\sup\ ⎻}{{$\!^-\,$}}1
     84%       {\\sup\ ⎻*}{{$\!^{-*}\,$}}1
     85%       {\\sup\ *}{{$\!^{*}\,$}}1
     86%       {^*}{{$\!^{*}\,$}}1
     87%       {F*}{{F$^*$}}1
     88%       {G*}{{G$^*$}}1
     89%       {∘}{{$\circ\;$}}2
     90%       {Ω}{{$\Omega$}}1
     91%       {Ω^carrbt}{{$\Omega^{\mbox{carrbt}}$}}1
     92%       {Ω^A}{{$\Omega^A$}}1
     93%       {Ω^C}{{$\Omega^C$}}1
     94%       {Ω^U}{{$\Omega^U$}}1
     95%       {Ω^V}{{$\Omega^V$}}1
     96%       {Ω^X}{{$\Omega^X$}}1
     97%       {Ω^s}{{$\Omega^s$}}1
     98%       {‡}{{$\ddagger$}}1
     99%       {†}{{$\dagger$}}1
     100%       {⊆}{{$\subseteq\,$}}2
     101%       {♮}{{$\natural$}}1
     102%       {∩}{{$\cap$}}2
     103%       {∪}{{$\cup$}}2
     104%       {⋂}{{$\bigcap$}}2
     105%       {⋃}{{$\bigcup$}}2
     106%       {∈}{{$\in\,$}}2
     107%       {⎽o}{{$_o$}}1
     108%       {⎽f}{{$_f$}}1
     109%       {'\ \\sub\\c}{{'$\!_c$}}1
     110%       {\ \\sub\\c}{{$_c$}}1
     111%       {'\\sub\\c}{{'$\!_c$}}1
     112%       {\\sub\\c}{{$_c$}}1
     113%       {'\ \\sub\\f}{{'$\!_f$}}1
     114%       {\ \\sub\\f}{{$_f$}}1
     115%       {'\\sub\\f}{{'$\!_f$}}1
     116%       {\\sub\\f}{{$_f$}}1
     117%       {\\sup\ (form\ o)}{{$^{o_f}$}}1
     118%       {\\sup\ (concr\ o)}{{$^{o_c}$}}1
     119%       {(form\ o)}{{o$_f~$}}2
     120%       {(concr\ o)}{{o$_c~$}}2
     121%       {form\ o}{{o$_f~$}}2
     122%       {concr\ o}{{o$_c~$}}2
     123%       {Ω^(form\ o)}{{$\Omega^{o_f}~$}}2
     124%       {Ω^(concr\ o)}{{$\Omega^{o_c}~$}}2
     125%       {◊⎽t}{{$\Diamond_t$}}1
     126%       {□⎽t}{{$\boxempty_t$}}1
     127%       {⎽⇒}{{$_\Rightarrow$}}1
     128%       {o_operator_of_operator}{{o\_op\_of\_op}}2
     129%       {o_saturation_expansive}{{o\_sat\_expa}}2
     130%       {o_saturation_monotone}{{o\_sat\_monot}}2
     131%       {o_saturation_idempotent}{{o\_sat\_idemp}}2
     132%       {o_continuous_relation_of_continuous_relation}{{ocrel\_of\_crel}}2
     133%       {o_basic_topology_of_basic_topology}{{obtop\_of\_btop}}2
     134%       {basic_topology_of_basic_pair}{{btop\_of\_bp}}2
     135%       {o_basic_topology_of_o_basic_pair}{{o\_bt\_of\_o\_bp}}2
     136%       {^-1}{{$^{-1}$}}1
     137%       {^\ -1}{{$^{-1}$}}1
     138%       {\ \\sup\ -1}{{$^{-1}$}}1
     139%       {\\sup\ -1}{{$^{-1}$}}1
     140%       {\ \\sup-1}{{$^{-1}$}}1
     141%       {\\sup-1}{{$^{-1}$}}1
     142%       {...}{{$\ldots$}}1
    143143        ,
    144144tabsize=1,
Note: See TracChangeset for help on using the changeset viewer.