git.iko.soy/Idris-dev
on master help sign in
need to import Data.Vect and Data.Fin for interp.idr to compile
8518aa3anthony cantor
samples/tutorial/interp.idr+3
compare with master
unifiedsplit
@@ -1,5 +1,8 @@
1module Main
1module Main
2
2
3+import Data.Vect
4+import Data.Fin
5+
3data Ty = TyInt | TyBool| TyFun Ty Ty
6data Ty = TyInt | TyBool| TyFun Ty Ty
4
7
5interpTy : Ty -> Type
8interpTy : Ty -> Type