6 Jul
2011
6 Jul
'11
6:16 a.m.
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?