Commit 2023-03-28 23:28 869fc2fd

View on Github →

chore: rename mkpair → pair (#2324) We rename the ported mkpair to pair, as mkpair didn't follow the naming convention and pair pairs well with unpair. A poll for this decision was held on zulip.

Estimated changes

deleted theorem Nat.Primrec'.mkpair
added theorem Nat.Primrec'.natPair
deleted theorem Primrec₂.mkpair
added theorem Primrec₂.natPair
deleted theorem Nat.add_le_mkpair
added theorem Nat.add_le_pair
deleted theorem Nat.left_le_mkpair
added theorem Nat.left_le_pair
deleted def Nat.mkpair
deleted def Nat.mkpairEquiv
deleted theorem Nat.mkpair_eq_mkpair
deleted theorem Nat.mkpair_lt_mkpair_left
deleted theorem Nat.mkpair_unpair'
deleted theorem Nat.mkpair_unpair
added def Nat.pair
added def Nat.pairEquiv
added theorem Nat.pair_eq_pair
added theorem Nat.pair_lt_pair_left
added theorem Nat.pair_lt_pair_right
added theorem Nat.pair_unpair'
added theorem Nat.pair_unpair
deleted theorem Nat.right_le_mkpair
added theorem Nat.right_le_pair
deleted theorem Nat.unpair_mkpair
added theorem Nat.unpair_pair
modified theorem Encodable.encode_prod_val
modified theorem Encodable.encode_sigma_val