doc-src/Sledgehammer/sledgehammer.tex
 changeset 43352 597f31069e18 parent 43260 7b875e14b90d child 43571 423f100f1f85
equal inserted replaced
43351:b19d95b4d736 43352:597f31069e18
  1012 Specifies the maximum number of facts that may be returned by the relevance
  1012 Specifies the maximum number of facts that may be returned by the relevance
  1013 filter. If the option is set to \textit{smart}, it is set to a value that was
  1013 filter. If the option is set to \textit{smart}, it is set to a value that was
  1014 empirically found to be appropriate for the prover. A typical value would be
  1014 empirically found to be appropriate for the prover. A typical value would be
  1015 250.
  1015 250.
  1016
  1016
  1017 \opdefault{max\_new\_mono\_instances}{int}{\upshape 400}
  1017 \opdefault{max\_new\_mono\_instances}{int}{\upshape 200}
  1018 Specifies the maximum number of monomorphic instances to generate beyond
  1018 Specifies the maximum number of monomorphic instances to generate beyond
  1019 \textit{max\_relevant}. The higher this limit is, the more monomorphic instances
  1019 \textit{max\_relevant}. The higher this limit is, the more monomorphic instances
  1020 are potentially generated. Whether monomorphization takes place depends on the
  1020 are potentially generated. Whether monomorphization takes place depends on the
  1021 type system used.
  1021 type system used.
  1022
  1022