git.iko.soy/Idris-dev
on master help sign in
Fix Vect arguments in samples/
d6f785eEdwin Brady
samples/interp-alt.idr+6−6
compare with master
unifiedsplit
@@ -7,22 +7,22 @@ interpTy TyInt = Int
7interpTy TyBool = Bool
7interpTy TyBool = Bool
8interpTy (TyFun s t) = interpTy s -> interpTy t
8interpTy (TyFun s t) = interpTy s -> interpTy t
9
9
10−using (G : Vect Ty n)
10+using (G : Vect n Ty)
11
11
12− data Env : Vect Ty n -> Type where
12+ data Env : Vect n Ty -> Type where
13 Nil : Env Nil
13 Nil : Env Nil
14 (::) : interpTy a -> Env G -> Env (a :: G)
14 (::) : interpTy a -> Env G -> Env (a :: G)
15
15
16−-- data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where
16+-- data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
17-- stop : HasType fZ (t :: G) t
17-- stop : HasType fZ (t :: G) t
18-- pop : HasType k G t -> HasType (fS k) (u :: G) t
18-- pop : HasType k G t -> HasType (fS k) (u :: G) t
19
19
20− lookup : (i:Fin n) -> Env G -> interpTy (lookup i G)
20+ lookup : (i:Fin n) -> Env G -> interpTy (index i G)
21 lookup fZ (x :: xs) = x
21 lookup fZ (x :: xs) = x
22 lookup (fS i) (x :: xs) = lookup i xs
22 lookup (fS i) (x :: xs) = lookup i xs
23
23
24− data Expr : Vect Ty n -> Ty -> Type where
24+ data Expr : Vect n Ty -> Ty -> Type where
25− Var : (i : Fin n) -> Expr G (lookup i G)
25+ Var : (i : Fin n) -> Expr G (index i G)
26 Val : (x : Int) -> Expr G TyInt
26 Val : (x : Int) -> Expr G TyInt
27 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
27 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
28 App : Expr G (TyFun a t) -> Expr G a -> Expr G t
28 App : Expr G (TyFun a t) -> Expr G a -> Expr G t
samples/interp.idr+4−4
@@ -7,13 +7,13 @@ interpTy TyInt = Int
7interpTy TyBool = Bool
7interpTy TyBool = Bool
8interpTy (TyFun s t) = interpTy s -> interpTy t
8interpTy (TyFun s t) = interpTy s -> interpTy t
9
9
10−using (G : Vect Ty n)
10+using (G : Vect n Ty)
11
11
12− data Env : Vect Ty n -> Type where
12+ data Env : Vect n Ty -> Type where
13 Nil : Env Nil
13 Nil : Env Nil
14 (::) : interpTy a -> Env G -> Env (a :: G)
14 (::) : interpTy a -> Env G -> Env (a :: G)
15
15
16− data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where
16+ data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
17 stop : HasType fZ (t :: G) t
17 stop : HasType fZ (t :: G) t
18 pop : HasType k G t -> HasType (fS k) (u :: G) t
18 pop : HasType k G t -> HasType (fS k) (u :: G) t
19
19
@@ -21,7 +21,7 @@ using (G : Vect Ty n)
21 lookup stop (x :: xs) = x
21 lookup stop (x :: xs) = x
22 lookup (pop k) (x :: xs) = lookup k xs
22 lookup (pop k) (x :: xs) = lookup k xs
23
23
24− data Expr : Vect Ty n -> Ty -> Type where
24+ data Expr : Vect n Ty -> Ty -> Type where
25 Var : HasType i G t -> Expr G t
25 Var : HasType i G t -> Expr G t
26 Val : (x : Int) -> Expr G TyInt
26 Val : (x : Int) -> Expr G TyInt
27 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
27 Lam : Expr (a :: G) t -> Expr G (TyFun a t)