@@ -12,6 +12,7 @@ import Idris.Delaborate
12import Idris.Compiler
12import Idris.Compiler
13import Idris.Prover
13import Idris.Prover
14import Idris.Parser
14import Idris.Parser
15import Paths_idris
16import Paths_idris
17import Core.Evaluate
18import Core.Evaluate
@@ -194,7 +195,12 @@ process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t
194 ist <- get
195 ist <- get
195 let tm' = specialise ctxt (idris_statics ist) tm
196 let tm' = specialise ctxt (idris_statics ist) tm
196 iputStrLn (show (delab ist tm'))
197 iputStrLn (show (delab ist tm'))
197−process fn (Prove n) = prover (lit fn) n
198+process fn (Prove n) = do prover (lit fn) n
201+ totcheck (FC "(input)" 0, n)
202+ mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)
203+ mapM_ checkDeclTotality (idris_totcheck i)
198process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t
204process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t
199 ctxt <- getContext
205 ctxt <- getContext
200 ist <- get
206 ist <- get