@@ -62,7 +62,7 @@ The full representation of expressions is:
6262
6363 data Expr : Vect n Ty -> Ty -> Type where
6464 Var : HasType i G t -> Expr G t
65− Val : (x : Int) -> Expr G TyInt
65+ Val : (x : Integer) -> Expr G TyInt
6666 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
6767 App : Expr G (TyFun a t) -> Expr G a -> Expr G t
6868 Op : (interpTy a -> interpTy b -> interpTy c) ->
@@ -115,7 +115,7 @@ A value carries a concrete representation of an integer:
115115
116116.. code-block:: idris
117117
118− Val : (x : Int) -> Expr G TyInt
118+ Val : (x : Integer) -> Expr G TyInt
119119
120120A lambda creates a function. In the scope of a function of type ``a ->
121121t``, there is a new local variable of type ``a``, which is expressed