document metis options better
Wed, 16 Nov 2011 11:16:23 +0100
changeset 45518 8ca7e3f25ee4
parent 45517 e1d9f0fa80d3
child 45519 cd6e78cb6ee8
document metis options better
--- a/doc-src/Sledgehammer/sledgehammer.tex	Wed Nov 16 10:44:36 2011 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Wed Nov 16 11:16:23 2011 +0100
@@ -655,16 +655,26 @@
 The \textit{metis} proof method has the syntax
-where \qty{type\_enc} is a type encoding specification with the same semantics
-as Sledgehammer's \textit{type\_enc} option (\S\ref{problem-encoding}) and
-\qty{facts} is a list of arbitrary facts. In addition to the values listed in
-\S\ref{problem-encoding}, \qty{type\_enc} may also be \textit{full\_types}, in
-which case an appropriate type-sound encoding is chosen, \textit{partial\_types}
-(the default type-unsound encoding), or \textit{no\_types}, a synonym for
+where \qty{facts} is a list of arbitrary facts and \qty{options} is a
+comma-separated list consisting of at most one $\lambda$ translation scheme
+specification with the same semantics as Sledgehammer's \textit{lam\_trans}
+option (\S\ref{problem-encoding}) and at most one type encoding specification
+with the same semantics as Sledgehammer's \textit{type\_enc} option
+The supported $\lambda$ translation schemes are \textit{hide\_lams},
+\textit{lam\_lifting}, and \textit{combinators} (the default).
+All the untyped type encodings listed in \S\ref{problem-encoding} are supported.
+For convenience, the following aliases are provided:
+\item[\labelitemi] \textbf{\textit{full\_types}:} An appropriate type-sound encoding.
+\item[\labelitemi] \textbf{\textit{partial\_types}:} Synonym for \textit{poly\_args}.
+\item[\labelitemi] \textbf{\textit{no\_types}:} Synonym for \textit{erased}.
 \section{Option Reference}