gistfile1.txt

augur> now, the last piece of phase 1:
augur> well, let me first be precise now about function application:
augur> if    Γ ⊢ M : a → b    and    Γ ⊢ N : a    then    Γ ⊢ M(N) : b
augur> ok now, the last thing we have to worry abot:
augur> if    Γ, x : a ⊢ M : b    then    Γ ⊢ λx:a.M : a → b
augur> this is called lambda abstraction
augur> it just says: if M : b, relying on a variable x : a, then we can use up that variable and get a function out instead
augur> for instance:   x : e ⊢ Dog(x) : prop    so    ⊢ λx:e. Dog(x) : e → prop
augur> or for example:
augur> φ : prop, ψ : prop ⊢ φ ∧ ψ : prop    so    ⊢ λφ:prop. λψ:prop. φ ∧ ψ : prop → prop → prop
augur> ok?
augur> [redmathead]: does this make sense?