pub type Pos<A> = Or<Tauto<A>, Theory<A>>;Expand description
◇p := p^true ⋁ theory(p).
A proposition is theoretical possibly true if it is either a tautology or a theory.
This is a stronger notion of possibly true than in most modal logics. For a corresponding weaker notion of possibly true, see NNPos.