[Haskell-cafe] function terms

[Henning Thielemann]

On Wed, 6 Jul 2011, Ian Childs wrote:

> Term a is meant to be the simply-typed lambda-calculus as a GADT. Then given 
> two terms App (App "=" l1) r1, and App (App "=" l2) r2, I want to form App 
> (App "=" (App l1 l2)) (App r1 r2), but as you can see this will only work if 
> the types of l1 and l2, and r1 and r2, match as detailed previously. does 
> that make sense?

What is App? It looks like you apply it once to a string ("=") and also to 
terms(?) like l1, r1. How is the GADT defined?