Compute before proof search
Needed to establish the type in more complex cases
commit48715b78021c99f96d728826b33436a5c6c190d2
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateTue 6 Jan 2015, 11:27 (12 years ago)
parent9aea863
src/Idris/ProofSearch.hs+2−1
@@ -85,7 +85,8 @@ proofSearch False fromProver ambigok deferonfail depth elab _ nroot [fn] ist
8585 isImp (PImp p _ _ _ _) = (True, p)
8686 isImp arg = (True, priority arg) -- try to get all of them by unification
8787proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
88− = do ty <- goal
88+ = do compute
89+ ty <- goal
8990 argsok <- conArgsOK ty
9091 if ambigok || argsok then
9192 case lookupCtxt nroot (idris_tyinfodata ist) of