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

Axiom

bool.match_bool_type

Statement

∀ return, return → return → bool.bool → return

Main Dependencies
Theory

Coq-Jumb
Statement

Parameter match_bool_type : forall (return_:Type), return_ -> return_ -> bool -> return_



Matita-Jumb
Statement

axiom match_bool_type : \forall return_ : Type[0] . return_ -> return_ -> bool -> return_



Lean-jumb
Statement

constant match_bool_type : forall (return : Type) , (return) -> (return) -> (bool.bool) -> return



PVS-jumb

Statement

match_bool_type [return:TYPE+] : [return -> [return -> [bool_sttfa.sttfa_bool -> return]]]



OpenTheory

Printing for OpenTheory is not working at the moment.