Update test for new API
commita953ba2762b33ca8ccb8ffc45f035df6e15aa3ef
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateTue 25 Aug 2015, 17:38 (11 years ago)
parent6432db2
test/meta002/Tacs.idr+2−2
@@ -24,11 +24,11 @@ import Language.Reflection.Utils
2424intros : Elab ()
2525intros = do g <- getGoal
2626 case snd g of
27− `(~_ -> ~_) => intro Nothing
27+ `(~_ -> ~_) => intro'
2828 _ => return ()
2929
3030foo : Nat -> Nat
31−foo = %runElab (do intro (Just (UN "fnord"))
31+foo = %runElab (do intro (UN "fnord")
3232 fill `(plus ~(Var (UN "fnord")) ~(Var (UN "fnord")))
3333 solve)
3434