@@ -12,7 +12,7 @@ partial
1212auto : Elab ()
1313auto = do compute
1414 attack
15− try $ repeatUntilFail intro'
15+ try intros
1616 hs <- map fst <$> getEnv
1717 for_ hs $
1818 \ih => try (rewriteWith (Var ih))
@@ -23,10 +23,12 @@ auto = do compute
2323partial
2424mush : Elab ()
2525mush =
26− do n <- gensym "j"
26+ do attack
27+ n <- gensym "j"
2728 intro n
2829 try intros
2930 ignore $ induction (Var n) `andThen` auto
31+ solve
3032
3133plusAssoc : (j, k, l : Nat) -> plus (plus j k) l = plus j (plus k l)
3234plusAssoc = %runElab mush