Skip to content

Comment on Formally Verifying Rust's Opaque Typesparent

Comments

P and Q are propositions. P takes one parameter and Q takes none. For example P(x) might be "x is odd". The term `P(x)` by itself refers to P(x) being true.

So `∃ x. P(x)` is read as "There exists an x for which P of x is true." or "There exists an x such that P of x is true."

So `((∃ x. P(x)) → Q)` is read as "If there exists an x such that P of x is true, then Q is true."

And `(∀ x. (P(x) → Q))` is read as "For all x, if P(x) is true then Q is true."

The `⇔` indicates that the left hand side is true if and only if the right hand side is true, or in other words that they're equivalent, which you can tell from the descriptions above that they are.

AboutSource Built by g1lg1l

Hackerly is an independent reader for Hacker News, built on the public HN API. Not affiliated with Y Combinator.