git.iko.soy/Idris-dev
on master help sign in
Fix Vect arguments in samples/
commitd6f785e763a17abec2d6cdacab38dd39e519d20c authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 28 Jul 2013, 14:03 (13 years ago) parent1862197
2 files changed+10−10
compare with master
unifiedsplit
samples/interp-alt.idr+6−6 samples/interp.idr+4−4
samples/interp-alt.idr+6−6
@@ -7,22 +7,22 @@ interpTy TyInt = Int
77interpTy TyBool = Bool
88interpTy (TyFun s t) = interpTy s -> interpTy t
99
10−using (G : Vect Ty n)
10+using (G : Vect n Ty)
1111
12− data Env : Vect Ty n -> Type where
12+ data Env : Vect n Ty -> Type where
1313 Nil : Env Nil
1414 (::) : interpTy a -> Env G -> Env (a :: G)
1515
16−-- data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where
16+-- data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
1717-- stop : HasType fZ (t :: G) t
1818-- pop : HasType k G t -> HasType (fS k) (u :: G) t
1919
20− lookup : (i:Fin n) -> Env G -> interpTy (lookup i G)
20+ lookup : (i:Fin n) -> Env G -> interpTy (index i G)
2121 lookup fZ (x :: xs) = x
2222 lookup (fS i) (x :: xs) = lookup i xs
2323
24− data Expr : Vect Ty n -> Ty -> Type where
25− Var : (i : Fin n) -> Expr G (lookup i G)
24+ data Expr : Vect n Ty -> Ty -> Type where
25+ Var : (i : Fin n) -> Expr G (index i G)
2626 Val : (x : Int) -> Expr G TyInt
2727 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
2828 App : Expr G (TyFun a t) -> Expr G a -> Expr G t
samples/interp.idr+4−4
@@ -7,13 +7,13 @@ interpTy TyInt = Int
77interpTy TyBool = Bool
88interpTy (TyFun s t) = interpTy s -> interpTy t
99
10−using (G : Vect Ty n)
10+using (G : Vect n Ty)
1111
12− data Env : Vect Ty n -> Type where
12+ data Env : Vect n Ty -> Type where
1313 Nil : Env Nil
1414 (::) : interpTy a -> Env G -> Env (a :: G)
1515
16− data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where
16+ data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
1717 stop : HasType fZ (t :: G) t
1818 pop : HasType k G t -> HasType (fS k) (u :: G) t
1919
@@ -21,7 +21,7 @@ using (G : Vect Ty n)
2121 lookup stop (x :: xs) = x
2222 lookup (pop k) (x :: xs) = lookup k xs
2323
24− data Expr : Vect Ty n -> Ty -> Type where
24+ data Expr : Vect n Ty -> Ty -> Type where
2525 Var : HasType i G t -> Expr G t
2626 Val : (x : Int) -> Expr G TyInt
2727 Lam : Expr (a :: G) t -> Expr G (TyFun a t)