@@ -42,12 +42,18 @@ elabRewrite elab ist fc Nothing rule sc newg
4242 -}
4343elabRewrite elab ist fc Nothing rule sc newg
4444 = elabRewrite elab ist fc (Just (sUN "rewrite__impl")) rule sc newg
45−elabRewrite elab ist fc (Just substfn_in) rule sc newg
45+elabRewrite elab ist fc (Just substfn_in) rule sc_in newg
4646 = do substfn <- case lookupTyName substfn_in (tt_ctxt ist) of
4747 [(n, t)] -> return n
4848 [] -> lift . tfail . NoSuchVariable $ substfn_in
4949 more -> lift . tfail . CantResolveAlts $ map fst more
5050 attack
51+ sc <- case newg of
52+ Nothing -> return sc_in
53+ Just t -> do
54+ letn <- getNameFrom (sMN 0 "rewrite_result")
55+ return $ PLet fc letn fc t sc_in
56+ (PRef fc [] letn)
5157 tyn <- getNameFrom (sMN 0 "rty")
5258 claim tyn RType
5359 valn <- getNameFrom (sMN 0 "rval")
@@ -115,19 +121,3 @@ elabRewrite elab ist fc (Just substfn_in) rule sc newg
115121 removeImp t = t
116122 phApps tm = tm
117123
118−doEquiv elab fc t sc
119− = do attack
120− tyn <- getNameFrom (sMN 0 "ety")
121− claim tyn RType
122− valn <- getNameFrom (sMN 0 "eqval")
123− claim valn (Var tyn)
124− letn <- getNameFrom (sMN 0 "equiv_val")
125− letbind letn (Var tyn) (Var valn)
126− focus tyn
127− elab t
128− focus valn
129− elab sc
130− elab (PRef fc [] letn)
131− solve
132−
133−