fact: Definition QuantOp (q : Quantifier) : Int.t -> Int.t -> Int.t := match q with | Sum => Int.add | Product => Int.mul | Min => fun a b => Int.const (Z.min (Int.toZ a) (Int.toZ b)) | Max => fun a b => Int.const (Z.min (Int.toZ a) (Int.toZ b)) | _ => fun a b => Int.const 0 end.
imports: Coq(List) Coq(ListSet) Coq(FSetInterface) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers)