is_conj
boolSyntax.is_conj : term -> bool
Tests a term to see if it is a conjunction.
If M has the form t1 /\ t2, then is_conj M returns true. If M is not a conjunction the result is false.
M
t1 /\ t2
is_conj M
true
false
Never fails.
boolSyntax.mk_conj, boolSyntax.dest_conj
boolSyntax.mk_conj
boolSyntax.dest_conj