@@ -69,11 +69,14 @@ eDouble' : {G : Vect Ty n} ->
6969 Expr G (TyFun TyNat TyNat);
7070eDouble' = Lam (App (App eAdd (Var fO)) (Var fO));
7171
72−eProg : {G : Vect Ty n} -> Expr G (TyFun TyNat TyNat);
73−eProg = Lam (Bind (App eDouble (Var fO))
72+-- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2
73+
74+eProg : {G : Vect Ty n} -> Expr G (TyFun TyNat (TyFun TyNat TyNat));
75+eProg = Lam (Lam
76+ (Bind (App eDouble (Var (fS fO)))
7477 (\x => Bind (App eDouble (Var fO))
7578 (\y => Bind (App eDouble (Val x))
76− (\z => App (App eAdd (Val y)) (Val z)))));
79+ (\z => App (App eAdd (Val y)) (Val z))))));
7780
7881test : Nat;
7982test = interp Empty eAdd (S (S O)) (S (S O));