git.iko.soy/Idris-dev
on master help sign in
Merge pull request #170 from frytvm/master
73ec76fEdwin Brady
samples/binary.idr+2−2
compare with master
unifiedsplit
@@ -1,6 +1,6 @@
1module main
1module main
2
2
3−data Bit : Nat -> Set where
3+data Bit : Nat -> Type where
4 b0 : Bit 0
4 b0 : Bit 0
5 b1 : Bit 1
5 b1 : Bit 1
6
6
@@ -10,7 +10,7 @@ instance Show (Bit n) where
10
10
11infixl 5 #
11infixl 5 #
12
12
13−data Binary : (width : Nat) -> (value : Nat) -> Set where
13+data Binary : (width : Nat) -> (value : Nat) -> Type where
14 zero : Binary O O
14 zero : Binary O O
15 (#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)
15 (#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)
16
16
samples/interp-alt.idr+4−4
@@ -2,18 +2,18 @@ module main
2
2
3data Ty = TyInt | TyBool| TyFun Ty Ty
3data Ty = TyInt | TyBool| TyFun Ty Ty
4
4
5−interpTy : Ty -> Set
5+interpTy : Ty -> Type
6interpTy TyInt = Int
6interpTy 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
10using (G : Vect Ty n)
10using (G : Vect Ty n)
11
11
12− data Env : Vect Ty n -> Set where
12+ data Env : Vect Ty n -> 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 -> Set where
16+-- data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where
17-- stop : HasType fO (t :: G) t
17-- stop : HasType fO (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 fO (x :: xs) = x
21 lookup fO (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 -> Set where
24+ data Expr : Vect Ty n -> Ty -> Type where
25 Var : (i : Fin n) -> Expr G (lookup i G)
25 Var : (i : Fin n) -> Expr G (lookup 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)
samples/interp.idr+4−4
@@ -2,18 +2,18 @@ module main
2
2
3data Ty = TyInt | TyBool | TyFun Ty Ty
3data Ty = TyInt | TyBool | TyFun Ty Ty
4
4
5−interpTy : Ty -> Set
5+interpTy : Ty -> Type
6interpTy TyInt = Int
6interpTy 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
10using (G : Vect Ty n)
10using (G : Vect Ty n)
11
11
12− data Env : Vect Ty n -> Set where
12+ data Env : Vect Ty n -> 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 -> Set where
16+ data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where
17 stop : HasType fO (t :: G) t
17 stop : HasType fO (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 -> Set where
24+ data Expr : Vect Ty n -> 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)