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

Axiom

nat.pred

Statement

λn. match_nat_type O (λp. p) n

Main Dependencies
Theory

Coq-Jumb
Statement

Definition pred : nat -> nat := fun (n:nat) => match_nat_type (nat) O (fun (p:nat) => p) n



Matita-Jumb
Statement

definition pred : nat -> nat := \lambda n : nat. (match_nat_type) (nat) (O) (\lambda p : nat. p) n



Lean-jumb
Statement

noncomputable def pred : (nat.nat) -> nat.nat := fun (n : nat.nat) , ((((nat.match_nat_type) (nat.nat)) ((nat.O) )) (fun (p : nat.nat) , p)) (n)



PVS-jumb

Statement

pred : [nat_sttfa.sttfa_nat -> nat_sttfa.sttfa_nat] = (LAMBDA(n:nat_sttfa.sttfa_nat):nat_sttfa.match_nat_type[nat_sttfa.sttfa_nat](nat_sttfa.sttfa_O)((LAMBDA(p:nat_sttfa.sttfa_nat):p))(n))



OpenTheory

Printing for OpenTheory is not working at the moment.