ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-21 22:17:19 +03:00
Code Issues Projects Releases Wiki Activity

Fix Vect arguments in samples/

Browse Source
This commit is contained in:
Edwin Brady 2013-07-28 14:03:52 +01:00
parent 18621973c3
commit d6f785e763
2 changed files with 10 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
samples/interp-alt.idr
View File

@ -7,22 +7,22 @@ interpTy TyInt = Int
interpTy TyBool = Bool
interpTy (TyFun s t) = interpTy s -> interpTy t
using (G : Vect Ty n)
using (G : Vect n Ty)
data Env : Vect Ty n -> Type where
data Env : Vect n Ty -> Type where
Nil : Env Nil
(::) : interpTy a -> Env G -> Env (a :: G)
-- data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where
-- data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
-- stop : HasType fZ (t :: G) t
-- pop : HasType k G t -> HasType (fS k) (u :: G) t
lookup : (i:Fin n) -> Env G -> interpTy (lookup i G)
lookup : (i:Fin n) -> Env G -> interpTy (index i G)
lookup fZ (x :: xs) = x
lookup (fS i) (x :: xs) = lookup i xs
data Expr : Vect Ty n -> Ty -> Type where
Var : (i : Fin n) -> Expr G (lookup i G)
data Expr : Vect n Ty -> Ty -> Type where
Var : (i : Fin n) -> Expr G (index i G)
Val : (x : Int) -> Expr G TyInt
Lam : Expr (a :: G) t -> Expr G (TyFun a t)
App : Expr G (TyFun a t) -> Expr G a -> Expr G t

8
samples/interp.idr
View File

@ -7,13 +7,13 @@ interpTy TyInt = Int
interpTy TyBool = Bool
interpTy (TyFun s t) = interpTy s -> interpTy t
using (G : Vect Ty n)
using (G : Vect n Ty)
data Env : Vect Ty n -> Type where
data Env : Vect n Ty -> Type where
Nil : Env Nil
(::) : interpTy a -> Env G -> Env (a :: G)
data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where
data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
stop : HasType fZ (t :: G) t
pop : HasType k G t -> HasType (fS k) (u :: G) t
@ -21,7 +21,7 @@ using (G : Vect Ty n)
lookup stop (x :: xs) = x
lookup (pop k) (x :: xs) = lookup k xs
data Expr : Vect Ty n -> Ty -> Type where
data Expr : Vect n Ty -> Ty -> Type where
Var : HasType i G t -> Expr G t
Val : (x : Int) -> Expr G TyInt
Lam : Expr (a :: G) t -> Expr G (TyFun a t)