git.iko.soy/Idris-dev
on master help sign in
more interpreter testing
f97602bEdwin Brady
interp.mi+8
compare with master
unifiedsplit
@@ -57,5 +57,13 @@ eAdd : {G : Vect Ty n} ->
57 Expr G (TyFun TyNat (TyFun TyNat TyNat));
57 Expr G (TyFun TyNat (TyFun TyNat TyNat));
58eAdd = Lam (Lam (Add (Var fO) (Var (fS fO))));
58eAdd = Lam (Lam (Add (Var fO) (Var (fS fO))));
59
59
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+
60test : Nat;
68test : Nat;
61test = interp Empty eAdd (S (S O)) (S (S O));
69test = interp Empty eAdd (S (S O)) (S (S O));