git.iko.soy/Idris-dev
on master help sign in
Merge pull request #170 from frytvm/master

Fix samples to use Type instead of Set

commit73ec76f71a5f42c2e87d0a86d6db8365a48a0881 authorEdwin Brady <edwin.brady@gmail.com> dateFri 8 Feb 2013, 02:20 (14 years ago) parentf8683904a15c64
3 files changed+10−10
compare with master
unifiedsplit
samples/binary.idr+2−2 samples/interp-alt.idr+4−4 samples/interp.idr+4−4
samples/binary.idr+2−2
@@ -1,6 +1,6 @@
11module main
22
3−data Bit : Nat -> Set where
3+data Bit : Nat -> Type where
44 b0 : Bit 0
55 b1 : Bit 1
66
@@ -10,7 +10,7 @@ instance Show (Bit n) where
1010
1111infixl 5 #
1212
13−data Binary : (width : Nat) -> (value : Nat) -> Set where
13+data Binary : (width : Nat) -> (value : Nat) -> Type where
1414 zero : Binary O O
1515 (#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)
1616
samples/interp-alt.idr+4−4
@@ -2,18 +2,18 @@ module main
22
33data Ty = TyInt | TyBool| TyFun Ty Ty
44
5−interpTy : Ty -> Set
5+interpTy : Ty -> Type
66interpTy TyInt = Int
77interpTy TyBool = Bool
88interpTy (TyFun s t) = interpTy s -> interpTy t
99
1010using (G : Vect Ty n)
1111
12− data Env : Vect Ty n -> Set where
12+ data Env : Vect Ty n -> 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 -> Set where
16+-- data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where
1717-- stop : HasType fO (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 fO (x :: xs) = x
2222 lookup (fS i) (x :: xs) = lookup i xs
2323
24− data Expr : Vect Ty n -> Ty -> Set where
24+ data Expr : Vect Ty n -> Ty -> Type where
2525 Var : (i : Fin n) -> Expr G (lookup i G)
2626 Val : (x : Int) -> Expr G TyInt
2727 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
samples/interp.idr+4−4
@@ -2,18 +2,18 @@ module main
22
33data Ty = TyInt | TyBool | TyFun Ty Ty
44
5−interpTy : Ty -> Set
5+interpTy : Ty -> Type
66interpTy TyInt = Int
77interpTy TyBool = Bool
88interpTy (TyFun s t) = interpTy s -> interpTy t
99
1010using (G : Vect Ty n)
1111
12− data Env : Vect Ty n -> Set where
12+ data Env : Vect Ty n -> 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 -> Set where
16+ data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where
1717 stop : HasType fO (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 -> Set where
24+ data Expr : Vect Ty n -> 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)