@@ -57,5 +57,13 @@ eAdd : {G : Vect Ty n} ->
5757 Expr G (TyFun TyNat (TyFun TyNat TyNat));
5858eAdd = Lam (Lam (Add (Var fO) (Var (fS fO))));
5959
60+eDouble : {G : Vect Ty n} ->
61+ Expr G (TyFun TyNat TyNat);
62+eDouble = Lam (App (App (Lam (Lam (Add (Var fO) (Var (fS fO))))) (Var fO)) (Var fO));
63+
64+eDouble' : {G : Vect Ty n} ->
65+ Expr G (TyFun TyNat TyNat);
66+eDouble' = Lam (App (App eAdd (Var fO)) (Var fO));
67+
6068test : Nat;
6169test = interp Empty eAdd (S (S O)) (S (S O));