From 0da83dc4ae290ebcc7d77b4980f4df4d113465c7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 25 Jan 2021 17:03:53 -0800
Subject: [PATCH] feat: add `unfoldDefinition`

---
 src/Lean/Meta/WHNF.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index 03390e1786..c5ed7dc24f 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -421,6 +421,10 @@ mutual
     | _ => return none
 end
 
+def unfoldDefinition (e : Expr) : MetaM Expr := do
+  let some e ← unfoldDefinition? e | throwError! "failed to unfold definition{indentExpr e}"
+  return e
+
 @[specialize] partial def whnfHeadPred (e : Expr) (pred : Expr → MetaM Bool) : MetaM Expr :=
   whnfEasyCases e fun e => do
     let e ← whnfCore e