(i) What is the order of calls to TmApp within evall? (ii) How values are distinguished from non-values? (iii) What is the role of contexts? let rec eval 1 ctx t = match t with TmApp (fi, TmAbs C,x,t12), v2) when isval ctx v2 - termSubstTop v2 t12 | TmApp (fi,v1,t2) when isval ctx vl let t2' -evall ctx t2 in TmApp (fi, vl, t2') TmApp (fi,t1,t2) - let tl' - eval1 ctx tl in TmApp (fi, tl', t2) raise NoRuleApplies (i) What is the order of calls to TmApp within evall? (ii) How values are distinguished from non-values? (iii) What is the role of contexts? let rec eval 1 ctx t = match t with TmApp (fi, TmAbs C,x,t12), v2) when isval ctx v2 - termSubstTop v2 t12 | TmApp (fi,v1,t2) when isval ctx vl let t2' -evall ctx t2 in TmApp (fi, vl, t2') TmApp (fi,t1,t2) - let tl' - eval1 ctx tl in TmApp (fi, tl', t2) raise NoRuleApplies