bool.andb
λb1. λb2. if b1 then b2 else false
Definition andb : bool -> bool -> bool := fun (b1:bool) => fun (b2:bool) => match_bool_type (bool) b2 false b1
definition andb : bool -> bool -> bool := \lambda b1 : bool. \lambda b2 : bool. (match_bool_type) (bool) b2 (false) b1
noncomputable def andb : (bool.bool) -> (bool.bool) -> bool.bool := fun (b1 : bool.bool) , fun (b2 : bool.bool) , ((((bool.match_bool_type) (bool.bool)) (b2)) ((bool.false) )) (b1)
andb : [bool_sttfa.sttfa_bool -> [bool_sttfa.sttfa_bool -> bool_sttfa.sttfa_bool]] = (LAMBDA(b1:bool_sttfa.sttfa_bool):(LAMBDA(b2:bool_sttfa.sttfa_bool):bool_sttfa.match_bool_type[bool_sttfa.sttfa_bool](b2)(bool_sttfa.sttfa_false)(b1)))
Printing for OpenTheory is not working at the moment.