diff --git a/library/Init/Lean/WHNFUtil.lean b/library/Init/Lean/WHNFUtil.lean
index adafac3a2e..683b2282d6 100644
--- a/library/Init/Lean/WHNFUtil.lean
+++ b/library/Init/Lean/WHNFUtil.lean
@@ -360,4 +360,26 @@ match e with
   deltaDefinition cinfo lvls failK successK
 | _ => failK ()
 
+/- Reference implementation for `whnf`. It does not cache any results.
+
+   How to use:
+   - `getConst constName` retrieves `constName` from environment. Caller may make definitions opaque by returning `none`.
+   - `isAuxDef? constName` returns `true` is `constName` is an auxiliary declaration automatically generated by Lean and
+     used by equation compiler, and must be eagerly reduced by `whnfCore`. This method is usually implemented using `isAuxRecursor`.
+   - `synthesizePending` is used to (try to) synthesize synthetic metavariables that may be blocking reduction.
+
+   The other parameters should be self explanatory.  -/
+@[specialize] partial def whnfMain {m : Type → Type} [Monad m]
+    (getConst          : Name → m (Option ConstantInfo))
+    (isAuxDef?         : Name → m Bool)
+    (inferType         : Expr → m Expr)
+    (isDefEq           : Expr → Expr → m Bool)
+    (synthesizePending : Expr → m Bool)
+    (getLocalDecl      : Name → m LocalDecl)
+    (getMVarAssignment : Name → m (Option Expr))
+    : Expr → m Expr
+| e => do
+  e ← whnfCore getConst isAuxDef? whnfMain inferType isDefEq getLocalDecl getMVarAssignment e;
+  unfoldDefinition getConst isAuxDef? whnfMain inferType isDefEq synthesizePending getLocalDecl getMVarAssignment e (fun _ => pure e) whnfMain
+
 end Lean