da25e42 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Tweak proof search metavariable update

da25e42Edwin Brady13 years ago

libs/neweffects/Effects.idr−3

@@ -253,9 +253,6 @@ runEnv env prog = eff env prog (\r, env => pure (r ** env))

253runPure : Env id xs -> Eff id a xs xs' -> a

254runPure env prog = eff env prog (\r, env => r)

255

256−-- runPureEnv : Env id xs -> Eff id a xs xs' -> (x : a ** Env id (xs' x))

257−-- runPureEnv env prog = eff env prog (%unifyLog (\r, env => id (r ** env)))

258−

259runWith : (a -> m a) -> Env m xs -> Eff m a xs xs' -> m a

256runWith : (a -> m a) -> Env m xs -> Eff m a xs xs' -> m a

260runWith inj env prog = eff env prog (\r, env => inj r)

257runWith inj env prog = eff env prog (\r, env => inj r)

261

258

src/Idris/REPL.hs+1−1

@@ -744,7 +744,7 @@ process h fn (DoProofSearch updatefile l n hints)

744 | length cs >= length n

745 = case splitAt (length n) cs of

746 (mv, c:cs) ->

747− if (isSpace c && mv == n)

747+ if ((isSpace c || c == ')' || c == '}') && mv == n)

748 then addBracket brack new ++ (c : cs)

749 else '?' : mv ++ c : updateMeta True cs n new

750 (mv, []) -> if (mv == n) then addBracket brack new else '?' : mv