// This prints the left floatting menu
Dedukti    Load Matita      Load Coq         Load Lean        Load PVS         Load OpenTheory Load
Dedukti-jumb

Definition

bool.andb

Body

λb1. λb2. if b1 then b2 else false

Main Dependencies
Theory

Coq-Jumb
Body

Definition andb : bool -> bool -> bool := fun (b1:bool) => fun (b2:bool) => match_bool_type (bool) b2 false b1



Matita-Jumb
Body

definition andb : bool -> bool -> bool := \lambda b1 : bool. \lambda b2 : bool. (match_bool_type) (bool) b2 (false) b1



Lean-jumb
Body

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)



PVS-jumb

Body

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)))



OpenTheory

Printing for OpenTheory is not working at the moment.