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

Constant

nat.filter_nat_type

Type

∀ return, (nat.nat → return) → nat.nat → return

Main Dependencies
Theory

Coq-Jumb
Type

Parameter filter_nat_type : forall (return_:Type), (nat -> return_) -> nat -> return_



Matita-Jumb
Type

axiom filter_nat_type : \forall return_ : Type[0] . (nat -> return_) -> nat -> return_



Lean-jumb
Type

constant filter_nat_type : forall (return : Type) , ((nat.nat) -> return) -> (nat.nat) -> return



PVS-jumb

Type

filter_nat_type [return:TYPE+] : [[nat_sttfa.sttfa_nat -> return] -> [nat_sttfa.sttfa_nat -> return]]



OpenTheory

Printing for OpenTheory is not working at the moment.