Fixed reflection induction tactic
commit5bc16ae672c62ae29eec0cf5abc1628d1486217c
authorAhmad Salim Al-Sibahi <asal@itu.dk>
dateTue 10 Dec 2013, 13:06 (13 years ago)
parent1e93672
libs/base/Language/Reflection.idr+1−1
@@ -177,7 +177,7 @@ data Tactic = Try Tactic Tactic
177177 -- ^ focus a named hole
178178 | Rewrite TT
179179 -- ^ rewrite using the reflected rep. of a equality proof
180− | Induction TT
180+ | Induction TTName
181181 -- ^ do induction on the particular expression
182182 | LetTac TTName TT
183183 -- ^ name a reflected term