From 431a5de2b043a9d2b28428942cf1e92bec0ddfed Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 1 Nov 2019 09:55:08 -0700
Subject: [PATCH] chore: add helper functions

---
 library/Init/Lean/Expr.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/library/Init/Lean/Expr.lean b/library/Init/Lean/Expr.lean
index b07c38ef8c..badfd40cc9 100644
--- a/library/Init/Lean/Expr.lean
+++ b/library/Init/Lean/Expr.lean
@@ -246,6 +246,14 @@ def isAppOfArity : Expr → Name → Nat → Bool
 | app f _,   n, a+1 => isAppOfArity f n a
 | _,         _, _   => false
 
+def appFn! : Expr → Expr
+| app f _ => f
+| _       => panic! "application expected"
+
+def appArg! : Expr → Expr
+| app _ a => a
+| _       => panic! "application expected"
+
 def constName! : Expr → Name
 | const n _ => n
 | _         => panic! "constant expected"