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

Definition

gcd.gcd

Body

λn. λm. if (leb n m) then (gcd_aux n m n) else (gcd_aux m n m)

Main Dependencies
Theory

Coq-Jumb
Body

Definition gcd : nat.nat -> nat.nat -> nat.nat := fun (n:nat.nat) => fun (m:nat.nat) => bool.match_bool_type (nat.nat) (gcd_aux n m n) (gcd_aux m n m) (nat.leb n m)



Matita-Jumb
Body

definition gcd : nat -> nat -> nat := \lambda n : nat. \lambda m : nat. (match_bool_type) (nat) ((gcd_aux) n m n) ((gcd_aux) m n m) ((leb) n m)



Lean-jumb
Body

noncomputable def gcd : (nat.nat) -> (nat.nat) -> nat.nat := fun (n : nat.nat) , fun (m : nat.nat) , ((((bool.match_bool_type) (nat.nat)) (((((gcd.gcd_aux) ) (n)) (m)) (n))) (((((gcd.gcd_aux) ) (m)) (n)) (m))) ((((nat.leb) ) (n)) (m))



PVS-jumb

Body

gcd : [nat_sttfa_th.sttfa_nat -> [nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]] = (LAMBDA(n:nat_sttfa_th.sttfa_nat):(LAMBDA(m:nat_sttfa_th.sttfa_nat):bool_sttfa_th.match_bool_type[nat_sttfa_th.sttfa_nat](gcd_sttfa.gcd_aux(n)(m)(n))(gcd_sttfa.gcd_aux(m)(n)(m))(nat_sttfa_th.leb(n)(m))))



OpenTheory

Printing for OpenTheory is not working at the moment.