이드리스 썰매의 전술

Question

그래서 elaborator 반사에이 논문 (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 

기발한 추가의 연관성을 입증 할 수있는이 전술을

오류 :하지 터미네이터, 예상 : 나는 다음과 같은 오류 얻을 썰매의 유형 체킹을 시도하지만

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

"$"를, ",557 ",""," ","+ ","++ ","- ","- ",". ","/ ",": " : ","; ","< "," ","< ","<> ","< +> ","< < ","< = ","< |> ","= " , "==", "> =", ">>", ">> =", " 왼쪽 연상 연산자의 모호한 사용, 비 연관 연산자의 모호한 사용, 오른쪽 연상 연산자의 모호한 사용, 입력 끝, 일치하는 응용 프로그램 표현식, 여기서 블록 x < - gensym "x"^

무엇이 잘못 되었는가를 이해하지 못한다. 진부한 전술이 정확하지 않거나 내가 뭔가있다. 내 파일에 추가해야합니까? 모든

Answer 1

첫째, 당신은 약간의 수입을 추가해야

idris -p pruviloj <fileName.idr> 

typechecks와 작품,하지만 난 '년후 그건 :

이

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를 사용하는 이드리스 말할 필요 오류 메시지를 재현 할 수 없습니다.