3 lines
272 B
Plaintext
3 lines
272 B
Plaintext
|
eager = (\f x : triage (f t) (\u f : (t u)) (\u v : f (t u v)) x)
|
||
|
|
eagerEval = y (\self : triage (\u : t u) (\u v : t u v) (triage (\u2 v : u2) (\u1 u2 v : eager (self (self u1 v)) (self u2 v)) (\u0 u1 u2 v : triage u0 (\v : self u1 v) (\v1 v2 : self (self u2 v1) v2) v)))
|