git.iko.soy/Idris-dev
on master help sign in
Add goalType tactic
30585fcDavid Raymond Christiansen
libs/prelude/Language/Reflection/Elab.idr+7
compare with master
unifiedsplit
@@ -7,6 +7,7 @@ module Language.Reflection.Elab
7
7
8import Builtins
8import Builtins
9import Prelude.Applicative
9import Prelude.Applicative
10+import Prelude.Basics
10import Prelude.Bool
11import Prelude.Bool
11import Prelude.Functor
12import Prelude.Functor
12import Prelude.List
13import Prelude.List
@@ -224,6 +225,12 @@ namespace Tactics
224 forgetTypes : TT -> Elab Raw
225 forgetTypes : TT -> Elab Raw
225 forgetTypes tt = prim__Forget tt
226 forgetTypes tt = prim__Forget tt
226
227
228+ ||| Get the goal type as a Raw term
229+ goalType : Elab Raw
230+ goalType = do g <- getGoal
231+ forgetTypes (snd g)
232+
233+
227 ||| Generate a unique name based on some hint.
234 ||| Generate a unique name based on some hint.
228 |||
235 |||
229 ||| **NB**: the generated name is unique _for this run of the
236 ||| **NB**: the generated name is unique _for this run of the