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

Definition

permutation.transpose

Body

λi. λj. λn. if (n = i) then j else (if (n = j) then i else n)

Main Dependencies
Theory

Coq-Jumb
Body

Definition transpose : nat.nat -> nat.nat -> nat.nat -> nat.nat := fun (i:nat.nat) => fun (j:nat.nat) => fun (n:nat.nat) => bool.match_bool_type (nat.nat) j (bool.match_bool_type (nat.nat) i n (nat.eqb n j)) (nat.eqb n i)



Matita-Jumb
Body

definition transpose : nat -> nat -> nat -> nat := \lambda i : nat. \lambda j : nat. \lambda n : nat. (match_bool_type) (nat) j ((match_bool_type) (nat) i n ((eqb) n j)) ((eqb) n i)



Lean-jumb
Body

noncomputable def transpose : (nat.nat) -> (nat.nat) -> (nat.nat) -> nat.nat := fun (i : nat.nat) , fun (j : nat.nat) , fun (n : nat.nat) , ((((bool.match_bool_type) (nat.nat)) (j)) (((((bool.match_bool_type) (nat.nat)) (i)) (n)) ((((nat.eqb) ) (n)) (j)))) ((((nat.eqb) ) (n)) (i))



PVS-jumb

Body

transpose : [nat_sttfa_th.sttfa_nat -> [nat_sttfa_th.sttfa_nat -> [nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]]] = (LAMBDA(i:nat_sttfa_th.sttfa_nat):(LAMBDA(j:nat_sttfa_th.sttfa_nat):(LAMBDA(n:nat_sttfa_th.sttfa_nat):bool_sttfa_th.match_bool_type[nat_sttfa_th.sttfa_nat](j)(bool_sttfa_th.match_bool_type[nat_sttfa_th.sttfa_nat](i)(n)(nat_sttfa_th.eqb(n)(j)))(nat_sttfa_th.eqb(n)(i)))))



OpenTheory

Printing for OpenTheory is not working at the moment.