existsIndexed function

Exists existsIndexed(
  1. Map<String, Sort> args,
  2. Expr body, {
  3. Expr? when,
  4. int weight = 0,
  5. Iterable<Pat> patterns = const [],
  6. Iterable<Expr> noPatterns = const [],
  7. String? id,
  8. String? skolem,
})

Creates a Exists quantifier, like exists but arguments must manually de-Bruijn indexed.

Implementation

Exists existsIndexed(
  Map<String, Sort> args,
  Expr body, {
  Expr? when,
  int weight = 0,
  Iterable<Pat> patterns = const [],
  Iterable<Expr> noPatterns = const [],
  String? id,
  String? skolem,
}) =>
    Exists(
      args.map((key, value) => MapEntry(Sym(key), value)),
      when == null ? body : implies(when, body),
      weight: weight,
      patterns: patterns.toList(),
      noPatterns: noPatterns.toList(),
      id: id == null ? null : Sym(id),
      skolem: skolem == null ? null : Sym(skolem),
    ).declare();