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

Fix samples to use Type instead of Set

Browse Source
This commit is contained in:
Frederic Koehler 2013-01-29 01:47:02 -05:00
parent 95607a59c7
commit 4a15c64812
3 changed files with 10 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
samples/binary.idr
View File

@ -1,6 +1,6 @@
module main
data Bit : Nat -> Set where
data Bit : Nat -> Type where
b0 : Bit 0
b1 : Bit 1
@ -10,7 +10,7 @@ instance Show (Bit n) where
infixl 5 #
data Binary : (width : Nat) -> (value : Nat) -> Set where
data Binary : (width : Nat) -> (value : Nat) -> Type where
zero : Binary O O
(#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)

8
samples/interp-alt.idr
View File

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

8
samples/interp.idr
View File

@ -2,18 +2,18 @@ module main
data Ty = TyInt | TyBool | TyFun Ty Ty
interpTy : Ty -> Set
interpTy : Ty -> Type
interpTy TyInt = Int
interpTy TyBool = Bool
interpTy (TyFun s t) = interpTy s -> interpTy t
using (G : Vect Ty n)
data Env : Vect Ty n -> Set where
data Env : Vect Ty n -> Type where
Nil : Env Nil
(::) : interpTy a -> Env G -> Env (a :: G)
data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where
data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where
stop : HasType fO (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 -> Set where
data Expr : Vect Ty n -> 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)