Lines Matching refs:parameter
175 \texttt{implication\_concl\_qp} is a quantifier parameter that looks for valid guesses in the conclusion of an implication.
280 There is a quantifier heuristic parameter called \holtxt{pair\_default\_qp}. It first looks for
283 is found, $x$ is instantiated as well. This parameter therefore allows simplifications like:
291 quantifier heuristic parameter \holtxt{pair\_qp}, which allows the
308 by \holtxt{record\_qp}. In contrast to the pair parameter, the one for records gets only one function instead of a
311 The quantifier heuristic parameter \holtxt{default\_record\_qp} expands all records.
315 The parameter for records is stateful, as it uses knowledge from
317 but for general datatypes. The quantifier heuristic parameter
326 The standard quantifier heuristic parameter \holtxt{std\_qp} combines
490 As an example, lets define a parameter that states that every list is non-empty:
542 parameter.