diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 46d114f3dc77c1d88703c21e19a00ed876e53141..7dfb82ff1f3c4ea144636706e391560bc554ed16 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -149,7 +149,7 @@ object Expressions {
     }
   }
 
-  /** $encodingof `def ... = ...; ...` (lazy evaluation)
+  /** $encodingof `def ... = ...; ...` (local function definition)
     * 
     * @param id The function definition.
     * @param body The body of the expression after the function
@@ -190,9 +190,9 @@ object Expressions {
   }
 
 
-  /* HOFs (Higher-order Formulas) */
+  /* HOFs (Higher-order Functions) */
   
-  /** $encodingof `callee.apply(args...)`
+  /** $encodingof `callee(args...)`
     *
     * If you are not sure about the requirement you should use
     * [[purescala.Constructors#application purescala's constructor application]]
@@ -290,7 +290,7 @@ object Expressions {
     val subPatterns = Seq()    
   }
 
-  /** Any pattern having an `unapply` function */
+  /** A custom pattern defined through an object's `unapply` function */
   case class UnapplyPattern(binder: Option[Identifier], unapplyFun: TypedFunDef, subPatterns: Seq[Pattern]) extends Pattern {
     // Hacky, but ok
     lazy val optionType = unapplyFun.returnType.asInstanceOf[AbstractClassType]
@@ -377,14 +377,14 @@ object Expressions {
   }
 
 
-  /* Generic values. Represent values of the generic type tp */
+  /** Generic values. Represent values of the generic type `tp` */
   // TODO: Is it valid that GenericValue(tp, 0) != GenericValue(tp, 1)?
   case class GenericValue(tp: TypeParameter, id: Int) extends Expr with Terminal {
     val getType = tp
   }
 
 
-  /** $encodingof `case class ...(...)`
+  /** $encodingof `CaseClass(args...)`
     * @param ct The case class name and inherited attributes
     * @param args The arguments of the case class
     */
@@ -397,7 +397,7 @@ object Expressions {
     val getType = BooleanType
   }
 
-  /** $encodingof `value.selector` where value is a case class 
+  /** $encodingof `value.selector` where value is of a case class type
     *
     * If you are not sure about the requirement you should use
     * [[purescala.Constructors#caseClassSelector purescala's constructor caseClassSelector]]
@@ -417,11 +417,7 @@ object Expressions {
   }
 
 
-  /** $encodingof `... == ...`
-    *
-    * If you are not sure about the requirement you should use
-    * [[purescala.Constructors#equality purescala's constructor equality]]
-    */
+  /** $encodingof `... == ...` */
   case class Equals(lhs: Expr, rhs: Expr) extends Expr {
     val getType = {
       if (typesCompatible(lhs.getType, rhs.getType)) BooleanType
@@ -467,11 +463,7 @@ object Expressions {
     def apply(a: Expr, b: Expr): Expr = Or(Seq(a, b))
   }
 
-  /** Implication.
-    * 
-    * If you are not sure about the requirement you should use
-    * [[purescala.Constructors#implies purescala's constructor implies]]
-    */
+  /** Locical Implication */
   case class Implies(lhs: Expr, rhs: Expr) extends Expr {
     val getType = {
       if(lhs.getType == BooleanType && rhs.getType == BooleanType) BooleanType
@@ -479,11 +471,7 @@ object Expressions {
     }
   }
 
-  /** $encodingof `!...`
-    *  
-    * If you are not sure about the requirement you should use
-    * [[purescala.Constructors#not purescala's constructor not]]
-    */
+  /** $encodingof `!...` */
   case class Not(expr: Expr) extends Expr {
     val getType = {
       if (expr.getType == BooleanType) BooleanType
@@ -494,40 +482,28 @@ object Expressions {
 
   /* Integer arithmetic */
 
-  /** $encodingof `... +  ...`
-    *  
-    * If you are not sure about the requirement you should use
-    * [[purescala.Constructors#plus purescala's constructor plus]]
-    */
+  /** $encodingof `... +  ...` for BigInts */
   case class Plus(lhs: Expr, rhs: Expr) extends Expr {
     val getType = {
       if (lhs.getType == IntegerType && rhs.getType == IntegerType) IntegerType
       else untyped
     }
   }
-  /** $encodingof `... -  ...`
-    *  
-    * If you are not sure about the requirement you should use
-    * [[purescala.Constructors#matchExpr purescala's constructor matchExpr]]
-    */
+  /** $encodingof `... -  ...` */
   case class Minus(lhs: Expr, rhs: Expr) extends Expr {
     val getType = {
       if (lhs.getType == IntegerType && rhs.getType == IntegerType) IntegerType
       else untyped
     }
   }
-  /** $encodingof `- ...`*/
+  /** $encodingof `- ... for BigInts`*/
   case class UMinus(expr: Expr) extends Expr {
     val getType = {
       if (expr.getType == IntegerType) IntegerType
       else untyped
     }
   }
-  /** $encodingof `... *  ...`
-    *  
-    * If you are not sure about the requirement you should use
-    * [[purescala.Constructors#times purescala's constructor times]]
-    */
+  /** $encodingof `... * ...` */
   case class Times(lhs: Expr, rhs: Expr) extends Expr {
     val getType = {
       if (lhs.getType == IntegerType && rhs.getType == IntegerType) IntegerType
diff --git a/src/main/scala/leon/purescala/Types.scala b/src/main/scala/leon/purescala/Types.scala
index 3754b85342f48b6b8411ae3961b5c6597dbd2c81..775a82c19e7fadbec3e681f83d730d2e915a4702 100644
--- a/src/main/scala/leon/purescala/Types.scala
+++ b/src/main/scala/leon/purescala/Types.scala
@@ -32,7 +32,7 @@ object Types {
   abstract class TypeTree extends Tree with Typed {
     val getType = this
 
-    // Checks wether the subtypes of this type contain Untyped,
+    // Checks whether the subtypes of this type contain Untyped,
     // and if so sets this to Untyped.
     // Assumes the subtypes are correctly formed, so it does not descend 
     // deep into the TypeTree.
@@ -49,8 +49,8 @@ object Types {
   case object IntegerType extends TypeTree
   case object RealType extends TypeTree
 
-  case class BitVectorType(size: Int) extends TypeTree
-  case object Int32Type extends TypeTree
+  abstract class BitVectorType(val size: Int) extends TypeTree
+  case object Int32Type extends BitVectorType(32)
 
   class TypeParameter private (name: String) extends TypeTree {
     val id = FreshIdentifier(name, this)
@@ -74,7 +74,7 @@ object Types {
    * you should use tupleTypeWrap in purescala.Constructors
    */
   case class TupleType (bases: Seq[TypeTree]) extends TypeTree {
-    lazy val dimension: Int = bases.length
+    val dimension: Int = bases.length
     require(dimension >= 2)
   }