git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of github.com:idris-lang/Idris-dev
64b44f2Edwin Brady
test/pruviloj001/pruviloj001.idr+4−2
compare with master
unifiedsplit
@@ -12,7 +12,7 @@ partial
12auto : Elab ()
12auto : Elab ()
13auto = do compute
13auto = do compute
14 attack
14 attack
15− try $ repeatUntilFail intro'
15+ try intros
16 hs <- map fst <$> getEnv
16 hs <- map fst <$> getEnv
17 for_ hs $
17 for_ hs $
18 \ih => try (rewriteWith (Var ih))
18 \ih => try (rewriteWith (Var ih))
@@ -23,10 +23,12 @@ auto = do compute
23partial
23partial
24mush : Elab ()
24mush : Elab ()
25mush =
25mush =
26+ do attack
26− do n <- gensym "j"
27+ n <- gensym "j"
27 intro n
28 intro n
28 try intros
29 try intros
29 ignore $ induction (Var n) `andThen` auto
30 ignore $ induction (Var n) `andThen` auto
31+ solve
30
32
31plusAssoc : (j, k, l : Nat) -> plus (plus j k) l = plus j (plus k l)
33plusAssoc : (j, k, l : Nat) -> plus (plus j k) l = plus j (plus k l)
32plusAssoc = %runElab mush
34plusAssoc = %runElab mush