On Sunday, October 6, 2019 at 12:50:37 AM UTC+2, Mario Carneiro wrote: > > It can also be used together with bitwise type logical operations, such as > df-cad and df-had. >
To give an example, I added http://us.metamath.org/mpeuni/bj-cadif.html bj-cadif |- (cadd ( ph , ps , ch ) <-> if- ( ch , ( ph \/ ps ) , ( ph /\ ps ) ) ) which groups cad0 and cad1. > I think that if df-ifp exists, it is a given that df-if will be rewritten > in terms of it. It would be totally in keeping with other similar > definitions that define a class operation in terms of the logical analogue, > e.g. df-un, df-in, df-v etc. (Actually df-v is an exception; it should > probably read { x | T. } and I guess the use of x = x is a historical > accident?) > I added http://us.metamath.org/mpeuni/bj-df-v.html (and also bj-df-nul and bj-nul). Benoît -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/607178d6-982b-41c8-80b2-1d337d67b92d%40googlegroups.com.
