I find many references to Gödel's pairing function on ordinals but I have not found a definition. What is it?