イドリスのマッシュ戦術

Question

だから私はエラボレータ反射（https://eb.host.cs.st-andrews.ac.uk/drafts/elab-reflection.pdf）にこの論文を読んで、私は（セクション5.2で見つかった）この戦術アウトこれを試してみたかったことを決めた。

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

たぶんこの戦術は、追加の関連性を証明することができ：

エラー：期待できないターミネータ、 "$"、 "ドロドロのです。TypeCheckしようとしたとき

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

は、しかし、私は次のエラーを取得します「+」、「++」、「 - 」、「 - 」、「/」、「/ =」、「：」、「：」、「：」、「：」、「： ：」、 ";"、 "<"、 ""、 "< "、 "<>"、 "< +>"、 "< <"、 "< ="、 "< |>"、 "=" 「=」、「=」、「=」、「=」、「>> =」、「>> =」、「>>」、非連想演算子のあいまいな使用、非連想演算子のあいまいな使用、右結合演算子のあいまいな使用、入力の終わり、アプリケーション式の一致など、ブロック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 

は、その後、あなたはパッケージPruviloj使用するイドリスを指示する必要があります：

idris -p pruviloj <fileName.idr> 

それtypechecksと作品を、私は「wasnエラーメッセージを再現できません。