git.iko.soy/Idris-dev
on master help sign in
Fixed types in tutorial for Well-Typed Interpreter.
eddea6fJan de Muijnck-Hughes
docs/tutorial/interp.rst+2−2
compare with master
unifiedsplit
@@ -62,7 +62,7 @@ The full representation of expressions is:
62
62
63 data Expr : Vect n Ty -> Ty -> Type where
63 data Expr : Vect n Ty -> Ty -> Type where
64 Var : HasType i G t -> Expr G t
64 Var : HasType i G t -> Expr G t
65− Val : (x : Int) -> Expr G TyInt
65+ Val : (x : Integer) -> Expr G TyInt
66 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
66 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
67 App : Expr G (TyFun a t) -> Expr G a -> Expr G t
67 App : Expr G (TyFun a t) -> Expr G a -> Expr G t
68 Op : (interpTy a -> interpTy b -> interpTy c) ->
68 Op : (interpTy a -> interpTy b -> interpTy c) ->
@@ -115,7 +115,7 @@ A value carries a concrete representation of an integer:
115
115
116.. code-block:: idris
116.. code-block:: idris
117
117
118− Val : (x : Int) -> Expr G TyInt
118+ Val : (x : Integer) -> Expr G TyInt
119
119
120A lambda creates a function. In the scope of a function of type ``a ->
120A lambda creates a function. In the scope of a function of type ``a ->
121t``, there is a new local variable of type ``a``, which is expressed
121t``, there is a new local variable of type ``a``, which is expressed