ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-22 14:38:20 +03:00
Code Issues Projects Releases Wiki Activity

Add goalType tactic

Browse Source 
This is a derived tactic that I've defined in every non-trivial use of
Elab. Better put it in the library.
This commit is contained in:
David Raymond Christiansen 2015-08-12 10:38:28 -07:00
parent 763ac00bfd
commit 30585fcddd
1 changed files with 7 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
libs/prelude/Language/Reflection/Elab.idr
View File

@ -7,6 +7,7 @@ module Language.Reflection.Elab
import Builtins
import Prelude.Applicative
import Prelude.Basics
import Prelude.Bool
import Prelude.Functor
import Prelude.List
@ -224,6 +225,12 @@ namespace Tactics
forgetTypes : TT -> Elab Raw
forgetTypes tt = prim__Forget tt
||| Get the goal type as a Raw term
goalType : Elab Raw
goalType = do g <- getGoal
forgetTypes (snd g)
||| Generate a unique name based on some hint.
|||
||| **NB**: the generated name is unique _for this run of the