"Gamma" in STLC

[AdamBJ]

Can someone help me better understand the concept of gamma as it applies to STLC? Here is what I understand: gamma is related to type, and somehow maps each of the variables in a term to a type which allows us to determine the overall type of the term. I'm a bit confused about the specifics of how it accomplishes this though. Also, I don't understand some of the auxiliary functions related to gamma such as extend and extend_neq. What do these functions do and how are they related to the gamma of a term?

Thanks

[justlaugh05]

Think of states in the previous chapters. extend would be like update. empty Gamma would be empty_state. Instead of holding values of variables, it holds the Types