kdrag.modal.Valid

kdrag.modal.Valid(p: PBoolRef, prefix='t') → BoolRef

Convert from modal truth to regular Bool

https://en.wikipedia.org/wiki/Validity_(logic)#Valid_formula

>>> t = smt.Const("t", smt.IntSort())
>>> Valid(Box(smt.Lambda([t], t > 0)))
ForAll(t!..., ForAll(t1!..., Implies(t!... <= t1!..., t1!... > 0)))

Parameters:

p (PBoolRef)

Return type:

BoolRef