{{ message }}

Instantly share code, notes, and snippets.

# yohhoy/subsume-P0717R1.txt

Last active Sep 11, 2019
C++20 Concepts constraints subsumption analysis
 constraint-expressions: - C1^c && C2^c - C1^d # concept version template concept C1 = true^a; template concept C2 = true^b; normal form of P = true^a ∧ true^b normal form of Q = true^a P_1 = (true^a ∧ true^b) Q_1 = (true^a) ⇒ P_11=(true^a) identical Q_11=(true^a) ⇒ P_11 subsume Q_11 ⇒ (true^a && true^b) subsume (true^a) normal form of P = true^a normal form of Q = true^a ∧ true^b P_1 = (true^a) Q_1 = (true^a), Q_2=(true^b) { P_11=(true^a) identical Q_11=(true^a) ⇒ P_11 subsume Q_11, P_11=(true^a) NOT identical Q_21=(true^b) ⇒ P_11 NOT subsume Q_21 } ⇒ (true^a) NOT subsume (true^a && true^b) # non-concept version template inline constexpr bool C1 = true^a; template inline constexpr bool C2 = true^b; normal form of P = C1^c ∧ C2^c normal form of Q = C1^d P_1 = (C1^c ∧ C2^c) Q_1 = (C1^d) { P_11=(C1^c) NOT identical Q_11=(C1^c) ⇒ P_11 NOT subsume Q_11, { P_12=(C2^c) NOT identical Q_11=(C1^c) ⇒ P_12 NOT subsume Q_11 } ⇒ (C1^c && C2^c) NOT subsume (C1^d) normal form of P = C1^d normal form of Q = C1^c ∧ C2^c P_1 = (C1^d) Q_1 = (C1^c), Q_2 = (C2^c) { P_11=(C1^d) NOT identical Q_11=(C1^c) ⇒ P_11 NOT subsume Q_11, P_11=(C1^d) NOT identical Q_21=(C2^c) ⇒ P_11 NOT subsume Q_21 } ⇒ (C1^d) NOT subsume (C1^c && C2^c)
 constraint-expressions: - C1 && C2 - C1 # concept version template concept C1 = true; template concept C2 = true; normal form of P = true ∧ true normal form of Q = true P_1 = (true ∧ true) Q_1 = (true) ⇒ P_11=(true) identical Q_11=(true) ⇒ P_11 subsume Q_11 ⇒ (true && true) subsume (true) normal form of P = true normal form of Q = true ∧ true P_1 = (true) Q_1 = (true), Q_2=(true) { P_11=(true) identical Q_11=(true) ⇒ P_11 subsume Q_11, P_11=(true) identical Q_21=(true) ⇒ P_11 subsume Q_21 } ⇒ true subsume (true && true) # non-concept version template inline constexpr bool C1 = true; template inline constexpr bool C2 = true; normal form of P = C1 ∧ C2 normal form of Q = C1 P_1 = (C1 ∧ C2) Q_1 = (C1) ⇒ P_11=(C1) identical Q_11=(C1) ⇒ P_11 subsume Q_11 ⇒ (C1 && C2) subsume (C1) normal form of P = C1 normal form of Q = C1 ∧ C2 P_1 = (C1) Q_1 = (C1), Q_2 = (C2) { P_11=(C1) identical Q_11=(C1) ⇒ P_11 subsume Q_11, P_11=(C1) NOT identical Q_21=(C2) ⇒ P_11 NOT subsume Q_21 } ⇒ C1 NOT subsume (C1 && C2)