forall function

Forall forall(
  1. List<ConstVar> bound,
  2. Expr body, {
  3. Expr? when,
  4. int weight = 0,
  5. List<Pat> patterns = const [],
  6. List<Expr> noPatterns = const [],
  7. Sym? id,
  8. Sym? skolem,
})

Creates a Forall quantifier.

Implementation

Forall forall(
  List<ConstVar> bound,
  Expr body, {
  Expr? when,
  int weight = 0,
  List<Pat> patterns = const [],
  List<Expr> noPatterns = const [],
  Sym? id,
  Sym? skolem,
}) =>
    Forall.bind(
      currentContext,
      bound,
      when == null ? body : implies(when, body),
      weight: weight,
      patterns: patterns,
      noPatterns: noPatterns,
      id: id,
      skolem: skolem,
    ).declare();