on master help sign in
Expand ! binds in tactics
2a1de7aDavid Raymond Christiansen
src/Idris/DSL.hs+1
@@ -162,6 +162,7 @@ debind b tm = let (tm', (bs, _)) = runState (db' tm) ([], 0) in
162 db' (PDPair fc p l t r) = do l' <- db' l
162 db' (PDPair fc p l t r) = do l' <- db' l
163 r' <- db' r
163 r' <- db' r
164 return (PDPair fc p l' t r')
164 return (PDPair fc p l' t r')
165+ db' (PRunTactics fc t) = fmap (PRunTactics fc) (db' t)
165 db' t = return t
166 db' t = return t
166
167
167 dbArg a = do t' <- db' (getTm a)
168 dbArg a = do t' <- db' (getTm a)