option.elpi

/*
 * Copyright (C) BlueRock Security Inc. 2024
 *
 * SPDX-License-Identifier: LGPL-2.1 WITH BedRock Exception for use over network, see repository root for details.
 */

/** * Options */

namespace option {

  pred app! i:option A, i:A -> prop.

  /*
  Implementation
  */

  app! O F :- std.omap O (x\ _\ F x, !) _.
}