git.iko.soy/Idris-dev
on master help sign in
Change forall tactic to use unify rather than isType
35034dbEdwin Brady
CHANGELOG+1
compare with master
unifiedsplit
@@ -3,6 +3,7 @@ New in 0.9.8:
3
3
4User visible changes:
4User visible changes:
5
5
6+* Added "rewrite ... in ..." construct
6* Renamed EFF to EFFECT in Effect package
7* Renamed EFF to EFFECT in Effect package
7* Experimental Java backend
8* Experimental Java backend
8* Tab completion in REPL
9* Tab completion in REPL
src/Core/ProofState.hs+1−2
@@ -444,8 +444,7 @@ intro n ctxt env _ = fail "Can't introduce here."
444forall :: Name -> Raw -> RunTactic
444forall :: Name -> Raw -> RunTactic
445forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
445forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
446 do (tyv, tyt) <- lift $ check ctxt env ty
446 do (tyv, tyt) <- lift $ check ctxt env ty
447− lift $ isType ctxt env tyt
447+ unify' ctxt env tyt (TType (UVar 0))
448− lift $ isType ctxt env t
449 return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))
448 return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))
450forall n ty ctxt env _ = fail "Can't pi bind here"
449forall n ty ctxt env _ = fail "Can't pi bind here"
451
450