From 9cdaf79cfc5f00e765538f11c1bb511c7cdd22dc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 11 Nov 2019 12:19:07 -0800
Subject: [PATCH] feat: extend public Meta API

---
 library/Init/Lean/Meta/Default.lean | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/library/Init/Lean/Meta/Default.lean b/library/Init/Lean/Meta/Default.lean
index 57b0b6c9ad..4fb581bbf7 100644
--- a/library/Init/Lean/Meta/Default.lean
+++ b/library/Init/Lean/Meta/Default.lean
@@ -53,5 +53,14 @@ exprToBool <$> auxFixpoint isDefEqOp e₁ e₂
 /-          END OF BIG HACK                    -/
 /- =========================================== -/
 
+def isProp (e : Expr) : MetaM Bool :=
+isPropAux whnf e
+
+def getFunInfo (fn : Expr) : MetaM FunInfo :=
+getFunInfoAux whnf fn
+
+def getFunInfoNArgs (fn : Expr) (nargs : Nat) : MetaM FunInfo :=
+getFunInfoNArgsAux whnf fn nargs
+
 end Meta
 end Lean