addPtr : Address (size : Nat) -> (x : Fin size) -> Address (size - x) (the :: above should have been a single colon) Reads as: "addPtr" is a value of the f

addPtr : Address (size : Nat) -> (x : Fin size) -> Address (size - x) (the :: above should have been a single colon) Reads as: "addPtr" is a value of the following type: Function from two args: "Address (size : Nat)" and "(x : Fin size)" to result "Address (size - x)" "Address (size : Nat)" is the "Address" type applied to one Natural number parameter named "size" (indicating the allocation size the value of that Address points at). (x : Fin size) means it takes an "x" of type "Fin size". The "Fin param" type is a type that can hold a natural number 0..param-1. The resulting Address has a smaller size it points at.