2d22462 · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

@@ -238,6 +238,9 @@ Extra-source-files:

238 test/reg042/expected

239 test/reg043/run

240 test/reg043/expected

241+ test/reg044/run

242+ test/reg044/*.idr

243+ test/reg044/expected

241

244

242 test/basic001/run

245 test/basic001/run

243 test/basic001/*.idr

246 test/basic001/*.idr

src/Idris/Prover.hs+7−4

@@ -91,10 +91,13 @@ elabStep st e = case runStateT eCheck st of

91 OK (a, st') -> return (a, st')

92 Error a -> ierror a

93 where eCheck = do res <- e

94+ probs' <- get_probs

95+ case probs' of

94− tm <- get_term

96+ [] -> do tm <- get_term

95− ctxt <- get_context

97+ ctxt <- get_context

96− lift $ check ctxt [] (forget tm)

98+ lift $ check ctxt [] (forget tm)

97− return res

99+ return res

100+ ((_,_,_,e,_,_):_) -> lift $ Error e

98

101

99dumpState :: IState -> ProofState -> Idris ()

102dumpState :: IState -> ProofState -> Idris ()

100dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) =

103dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) =

test/reg044/expectednew file+11

@@ -0,0 +1,11 @@

1+reg044.idr:4:4:When elaborating right hand side of Main.pf:

2+Can't unify

3+ [95mb[0m [94m=[0m [95mb[0m

4+with

5+ [95ma[0m [94m=[0m [95mb[0m

6+

7+Specifically:

8+ Can't unify

9+ [95mb[0m

10+ with

11+ [95ma[0m

test/reg044/reg044.idrnew file+6

@@ -0,0 +1,6 @@

1+exjection : S a = S b -> a = b

2+exjection = ?pf

3+

4+pf = proof

5+ intros

6+ refine refl

test/reg044/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris reg044.idr --check

3+rm -f *.ibc