diff --git a/library/Init/Lean/Meta.lean b/library/Init/Lean/Meta.lean
index de50afa0e3..7e841ed269 100644
--- a/library/Init/Lean/Meta.lean
+++ b/library/Init/Lean/Meta.lean
@@ -31,15 +31,15 @@ private def boolToExpr : Bool → Expr
 | true  => mkBVar 0
 private partial def auxFixpoint : MetaOp → Expr → Expr → MetaM Expr
 | op, e₁, e₂ =>
-  let whnf         := fun e => auxFixpoint whnfOp e e;
-  let inferType    := fun e => auxFixpoint inferTypeOp e e;
-  let isDefEq      := fun e₁ e₂ => pure false; -- TODO
-  let synthPending := fun e => pure false;     -- TODO
+  let whnf         := fun e     => auxFixpoint whnfOp e e;
+  let inferType    := fun e     => auxFixpoint inferTypeOp e e;
+  let isDefEq      := fun e₁ e₂ => exprToBool <$> auxFixpoint isDefEqOp e₁ e₂;
+  let synthPending := fun e     => exprToBool <$> auxFixpoint synthPendingOp e e;
   match op with
   | whnfOp         => whnfAux inferType isDefEq synthPending e₁
   | inferTypeOp    => inferTypeAux whnf e₁
-  | synthPendingOp => boolToExpr <$> pure false
-  | isDefEqOp      => boolToExpr <$> pure false
+  | synthPendingOp => boolToExpr <$> pure false -- TODO
+  | isDefEqOp      => boolToExpr <$> pure false -- TODO
 
 def whnf (e : Expr) : MetaM Expr :=
 auxFixpoint whnfOp e e