Idris Tactics

Question

So, I read this article on the thinking of developers ( https://eb.host.cs.st-andrews.ac.uk/drafts/elab-reflection.pdf ) and decided that I want to try this tactic (see section 5.2) :

mush : Elab ()
mush =
   do attack
      x <- gensym "x"
      intro x
      try intros
      induction (Var x) `andThen` auto
      solve

Presumably, this tactic can prove the associativity of addition:

plusAssoc : (j, k, l : Nat) -> plus (plus j k) l = plus j (plus k l)
plusAssoc = %runElab mush

however, trying to call typecheck mush, I get the following error:

error: not a terminator, expected: "$", "&", ")", ","> "," + "," ++ "," - "," → ",". "," / "," / = "," :: ","; "," lt; "," "," <"," <> "," <+> ", <", "<=", "<|>", "=", "==", ">", "> = "," → "," → = "," \\ "," `", "in", "||", "~ = ~", the ambiguous use of the left-associative operator, the ambiguous use of the non-associative operator, the ambiguous use of the right -associative operator, completion of input, matching of application expression, where block x <- gensym "x" ^

, , -, ?

Answer 1

, :

import Language.Reflection
import Pruviloj.Core
import Pruviloj.Induction

auto : Elab ()
auto =
  do compute
     attack
     try intros
     hs <- map fst <$> getEnv
     for_ hs $
       \ih => try (rewriteWith (Var ih))
     hypothesis <|> search
     solve

mush : Elab ()
mush =
   do attack
      x <- gensym "x"
      intro x
      try intros
      induction (Var x) `andThen` auto
      solve

plusAssoc : (j, k, l : Nat) -> plus (plus j k) l = plus j (plus k l)
plusAssoc = %runElab mush

Idris, Pruviloj:

idris -p pruviloj <fileName.idr>

typechecks , .