git.iko.soy/Idris-dev
on master help sign in
Fix sample code
e51954fMarkus Klink
docs/tutorial/interp.rst+1−1
compare with master
unifiedsplit
@@ -30,7 +30,7 @@ calculated just like any other value:
30 interpTy : Ty -> Type
30 interpTy : Ty -> Type
31 interpTy TyInt = Integer
31 interpTy TyInt = Integer
32 interpTy TyBool = Bool
32 interpTy TyBool = Bool
33− interpTy (TyFun A T) = interpTy A -> interpTy T
33+ interpTy (TyFun a t) = interpTy a -> interpTy t
34
34
35We're going to define a representation of our language in such a way
35We're going to define a representation of our language in such a way
36that only well-typed programs can be represented. We'll index the
36that only well-typed programs can be represented. We'll index the