7bde028 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Use subst for intro, rather than updsubst

This is because we are introducing things that aren't holes, and the application status being "complete" might block for substitution of an introduction. This fixes a bug in the interactive prover and the interactive elaborator where introduction only worked when precisely the same name was provided, becuase it was incompletely substituted.

commit7bde028b12b4e8134746c3e6370c1193b5722298 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateTue 25 Aug 2015, 15:49 (11 years ago) parent29e29c2

1 file changed+5−2

compare with master

unifiedsplit

src/Idris/Core/ProofState.hs+5−2

src/Idris/Core/ProofState.hs+5−2

@@ -627,8 +627,11 @@ intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

627627 x@(Bind y (Pi _ s _) _) -> x

628628 _ -> hnf ctxt env t

629629 case t' of

630− Bind y (Pi _ s _) t -> -- trace ("in type " ++ show t') $

631− let t' = updsubst y (P Bound n s) t in

630+ Bind y (Pi _ s _) t ->

631+ -- It's important that this be subst and not updsubst,

632+ -- because we want to substitute even in portions of

633+ -- terms that we know do not contain holes.

634+ let t' = subst y (P Bound n s) t in

632635 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))

633636 _ -> lift $ tfail $ CantIntroduce t'

634637intro n ctxt env _ = fail "Can't introduce here."