@@ -7,6 +7,7 @@ module Language.Reflection.Elab
77
88import Builtins
99import Prelude.Applicative
10+import Prelude.Basics
1011import Prelude.Bool
1112import Prelude.Functor
1213import Prelude.List
@@ -224,6 +225,12 @@ namespace Tactics
224225 forgetTypes : TT -> Elab Raw
225226 forgetTypes tt = prim__Forget tt
226227
228+ ||| Get the goal type as a Raw term
229+ goalType : Elab Raw
230+ goalType = do g <- getGoal
231+ forgetTypes (snd g)
232+
233+
227234 ||| Generate a unique name based on some hint.
228235 |||
229236 ||| **NB**: the generated name is unique _for this run of the