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

Constant

bigops.bigop_body

Type

∀ H, nat.nat → (nat.nat → bool.bool) → H → (H → H → H) → (nat.nat → H) → H

Main Dependencies
Theory

Coq-Jumb
Type

Parameter bigop_body : forall (H:Type), nat.nat -> (nat.nat -> bool.bool) -> H -> (H -> H -> H) -> (nat.nat -> H) -> H



Matita-Jumb
Type

axiom bigop_body : \forall H : Type[0] . nat -> (nat -> bool) -> H -> (H -> H -> H) -> (nat -> H) -> H



Lean-jumb
Type

constant bigop_body : forall (H : Type) , (nat.nat) -> ((nat.nat) -> bool.bool) -> (H) -> ((H) -> (H) -> H) -> ((nat.nat) -> H) -> H



PVS-jumb

Type

bigop_body [H:TYPE+] : [nat_sttfa_th.sttfa_nat -> [[nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool] -> [H -> [[H -> [H -> H]] -> [[nat_sttfa_th.sttfa_nat -> H] -> H]]]]]



OpenTheory

Printing for OpenTheory is not working at the moment.