kdrag.FinP

kdrag.FinP(n: ExprRef | int) → QuantifierRef

Predicate for finite index less than n >>> FinP(3) Lambda(i, And(i >= 0, i < 3)) >>> x = smt.Const(“x”, FinP(3)) # Predicate defined constants have predicate auto inserted in quantifiers >>> prove(smt.ForAll([x], x < 4)) |= ForAll(x, Implies(And(x >= 0, x < 3), x < 4))