930f16a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

"auto" now does proof search

Instead of just the "trivial" tactic, it now searches through possible constructors.

commit930f16a5adc3b4a5068fa85c723e787eb5b4ca7e authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 12 Jun 2014, 21:27 (12 years ago) parent8a8faa8

2 files changed+3−5

unifiedsplit

libs/effects/Effects.idr+2−4

@@ -249,15 +249,13 @@ syntax MkDefaultEnv = with Env

249249

250250call : {a, b: _} -> {e : Effect} ->

251251 (eff : e t a b) ->

252− {default tactics { search 100; }

253− prf : EffElem e a xs} ->

252+ {auto prf : EffElem e a xs} ->

254253 Eff m t xs (\v => updateResTy v xs prf eff)

255254call e {prf} = callP prf e

256255

257256implicit

258257lift : Eff m t ys ys' ->

259− {default tactics { search 100; }

260− prf : SubList ys xs} ->

258+ {auto prf : SubList ys xs} ->

261259 Eff m t xs (\v => updateWith (ys' v) xs prf)

262260lift e {prf} = liftP prf e

263261

src/Idris/ParseExpr.hs+1−1

@@ -816,7 +816,7 @@ pi syn =

816816 symbol "->"

817817 sc <- expr syn

818818 return (bindList (PPi

819− (TacImp [] Dynamic (PTactics [Trivial]))) xt sc)) <|> (do

819+ (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing []]))) xt sc)) <|> (do

820820 try (lchar '{' *> reserved "default")

821821 when (st == Static) $ fail "default tactic constraints can not be lazy or static"

822822 script <- simpleExpr syn